Lane R：证明携带的隐式曲面规范与研究状态

状态：维护中的研究能力；窄接受域实现已保留；不阻塞 CAD V1 论文草稿：Lane R 论文草稿 形式化证明：formal/aira-lane-r

Lane R 研究隐式曲面网格的可检查拓扑保证（Proof-Carrying Isotopy）。它与 Exact 产品建模路径保持分离，作为前瞻研究和未来认证需求的基础，不属于当前 CAD V1 上线前置工作。只有当产品出现明确的几何认证需求时才扩大接受域。

1. 保留范围

当前源码保留了 Publication profile 的构造、独立检查、规范化字节和固定球体工件：

• packages/aira-lane-r/src/：构造器、独立检查器和规范化字节实现。
• packages/aira-lane-r/schema/：实际数据交换所需的 prior-art 与 publication artifact schema。
• formal/aira-lane-r/：Lean 4 源码与锁定工具链。
• packages/aira-lane-r/artifacts/publication-v0.2/：可复现的数值工件与第三方声明。

2. 维护与构建入口

根据仓库精简与开发约定，测试与验证通过构建及类型检查完成：

pnpm --filter @aira/lane-r build
pnpm --filter @aira/lane-r typecheck
cd formal/aira-lane-r
lake build

3. 开发规则与纪律

• 遵循实现优先原则，仓库不维护冗余的发布 attestation、closeout、人工复核模板或历史报告回放；历史阶段报告已退出工作树，必要时通过 Git 历史追溯。
• Lean 证明在 formal/aira-lane-r 中直接使用 lake build 验证。
• 新的 profile 或算子必须由真实产品需求驱动，并直接在现有实现中扩展。