Lane R Phase 0：exact affine edge-root kernel

状态：exact-root kernel + bundle checker complete；rounding isotopy blocker remains open

kernel merge：f3a70c7；bundle 分支：codex/lane-r-exact-root-bundle

日期：2026-08-31

1. 本批目标

本批只建立后续 certificate/checker 可复用的精确根边界，不声称完整修复 current freudenthal-linear-normal-surface@0.1.0：

finite binary64 endpoints and values
    -> exact reduced dyadic rationals
    -> canonical shared grid edge
    -> exact rational root parameter
    -> exact affine point and exact zero cancellation

浮点 mesh position 继续存在，但明确标记为 approximatePoint，不再作为精确根 witness 的组成部分。

2. TypeScript kernel

smooth-implicit-exact-edge-root.ts 实现：

按 IEEE-754 bit pattern 无损解码 finite binary64；
BigInt rational 的加、减、乘、除、约分和比较；
以较小 grid vertex id 作为共享边起点；
生成 canonical parameter 和 exact rational 3D point；
重算 (1-t)F(left)+tF(right)=0；
对非有限、退化、零端点和非 sign-changing 输入 fail closed；
使用 scale-safe binary64 parameter 生成兼容输出位置，但不把该位置放进 exact witness。

为保持 v0.1 sealed evidence 不变，新建的 smooth-implicit-certified-pl-exact-root-projection.ts 在旧 constructor 之外额外返回：

readonly exactEdgeRoots: readonly CertifiedPlExactEdgeRootBinding[];

每个 binding 把一个规范 exact shared root 对应到原 mesh vertex index。现有 constructor 源码、positions、 triangles 与 v0.1 sealed evidence 均保持不变。

3. Lean kernel

ExactRoot.lean 定义：

affineInterpolate；
edgeRootParameter；
ExactAffineEdgeRoot；
exactAffineEdgeRootOfSignChange。

已证明：

edgeRootParameter_mem_openUnitInterval；
edgeRootParameter_cancels；
exactAffineEdgeRoot_point_on_segment。

#print axioms 只报告 mathlib 当前使用的 propext、Classical.choice 和 Quot.sound；没有 custom axiom 或 sorryAx。

4. 验证

pnpm --filter @aira/field-spike typecheck
pnpm --filter @aira/field-spike exec vitest run \
  src/smooth-implicit-exact-edge-root.test.ts \
  src/smooth-implicit-certified-pl-exact-root-projection.test.ts \
  src/smooth-implicit-certified-pl.test.ts

cd formal/aira-lane-r
lake build

确定性审计反例现在同时保留两种对象：

exact root：严格位于 affine edge 上；
binary64 approximation：仍可偏离 affine edge，因而不能被当作 exact root。

5. Exact-root bundle checker

第二批已完成独立 schema、canonical ordering、root hash 和 checker 重建：

schema： lane-r-exact-edge-roots-v0.1.schema.json；
checker： smooth-implicit-certified-pl-exact-root-certificate.ts；
tests：pnpm --filter @aira/lane-r test。

真实 depth-4 fixture 当前确定性输出：

certificateId = lane-r-exact-edge-roots:sha256:bd533a4f47a1d6375418a254dcf781f159d6a7cc6fa0c77c50136673516d9312
exactEdgeRootHash = sha256:d2a37537c98d515255a0a6c1d76c454b16a007dafc60b3064d3f0e75532ff90b
rootCount = 908

checker 会验证：

一根对应一个连续 meshVertex；
grid edge 严格递增且不重复；
rational lexical form、正 denominator、约分和 open-unit parameter；
provided roots 与独立重建 roots 的 canonical hash 完全一致；
field、prerequisite、domain、grid values、position buffer、triangle buffer 全部绑定；
删除、重复、parameter 篡改和 certificate 篡改 fail closed。

证书不包含 claims、proofObligations 或 status，并固定：

positionSemantics = binary64-output-unproved-perturbation

5.1 当前 TCB

TypeScript finite-number/DataView bit decoding；
JavaScript BigInt 算术；
canonical semantic-ref hashing 与 WebCrypto SHA-256；
AJV JSON Schema validator；
checker 与 producer 共用的 exact-rational primitive。

Lean 已独立证明 exact real algebra，但 JSON/BigInt witness 到 Lean ExactAffineEdgeRoot 的 parser theorem 尚未建立，所以 TypeScript checker 结果不能直接称为 kernel-checked。

6. 未关闭项与下一批

将 exact roots 接入 formal certificate parser bridge；
形式化一个 tetrahedron 内 exact normal triangle/quad；
对 binary64 output 给出 displacement enclosure 和保持嵌入的扰动定理；在此之前不得用 exact-root theorem 推出 binary64 output 的 actualIsotopy=pass。