Eigenius 理论：基于构造性机构的类型化知识存储

论文提出 Eigenius 理论，定义了一种在构造性机构上进行类型化知识存储的形式系统。 核心内核为累积宇宙依赖类型论，将证明无关性设为公理而非转换规则，利用正交重写系统保证定义等价的判定性。 配套 Lean 4 形式化验证了系统一致性，通过子判断处理宇宙累积性与类包含，支持证据追踪与类型化知识图谱构建。