LaneRFormalCertificate v0.1

状态：Phase 1 design frozen / parser bridge not yet implemented

日期：2026-08-31

Schema： lane-r-formal-certificate-v0.1.schema.json

Lean representation： Certificate.lean

1. Scope

v0.1 的唯一 theorem scope 是：

homotopy-transversality-no-critical-zero

它是现有 Lane R certificate 的 formal projection，不是 replacement，也不是完整 mesh certificate。v0.1 不携带：

• actualIsotopy；
• globalRegularIsotopy；
• globalSelfIntersection；
• proof-obligation pass；
• ambient-isotopy map；
• Hausdorff claim；
• binary64 mesh root 正确性。

这些只能成为 Lean theorem 的输出，不能成为 Lean 的可信输入。

2. Data model

2.1 Source bindings

字段	作用
fieldId	绑定 Typed Field IR
prerequisiteAnalysisId	绑定 GeneralImplicit prerequisite
domainBoundsHash	绑定 domain
gridValueHash	绑定完整 vertex sample ordering/values
candidateTetrahedronHash	绑定 candidate band
uniformDepth	允许 Lean 重建 resolution/grid cardinality
tetrahedralization	固定 0→6 six-tet Freudenthal convention

hash 只提供 artifact identity；它们不证明 Field denotation或数学 theorem。parser/binding 在 Level 3 前仍需单独审计。

2.2 Exact scalar model

所有 proof-relevant 数使用 canonical reduced rational：

{ "numerator": "-3", "denominator": "7" }

JSON Schema 检查基本 lexical shape；Lean parser还必须检查：

• denominator > 0；
• gcd(|numerator|, denominator)=1；
• zero 必须写成 0/1；
• integer/string resource limits；
• interval lower ≤ upper；
• positive margin numerator > 0。

不把 binary64 decimal 直接解释成抽象 real。若从现有 binary64 checker迁移，bridge 必须用每个 finite float 的精确 dyadic value生成 rational，不能重新做 decimal近似。

2.3 Vertex-star witness

每个 relevant grid vertex 携带：

• grid vertex index；
• exact rational 3-vector separator；
• smooth gradient interval box；
• 每个 incident tetrahedron 的 index 与 PL gradient interval box。

全 certificate 携带两个正的 global minimum margins。Lean 对每个 star 重算 sign-aware dotLower，验证：

minimumSmoothMargin ≤ dotLower(separator, smoothGradientBox)
minimumPlMargin     ≤ dotLower(separator, each incident PL gradient box)

producer 提供的 per-star smoothMargin/plMargin summary 不需要进入 formal certificate；Lean 直接重算。

2.4 Barycentric weights 不在 certificate 中

F_t regularity theorem 对 simplex 内所有点量化。一个点的 barycentric weights 是 theorem variable，应由 simplex-membership lemma推出 nonnegative 与 sum-to-one，而不是为有限采样点逐一证书化。因此 Lean BarycentricWeights 是 proof object，不是 serialized witness 字段。

3. Producer / checker / certificate / Lean split

信息或动作	Producer	Current TS checker	v0.1 carries	Lean v0.1 rechecks
separator 搜索	计算候选	验证	exact separator	dot lower bounds
uniform grid/Freudenthal	可缓存	重建	version/depth/hashes	Phase 1只绑定；L2重建
vertex samples	计算	重算	hash；bridge可另带 exact trace	Phase 1未重算 Field denotation
smooth interval box	计算	从 Field重算	exact rational box	box order、dot bound；Field inclusion待 L1.5/L2
PL gradients	计算	从 samples重算	incident exact boxes	dot bound；PL derivative correspondence待 L2
star coverage	生成	重建并检查 exact set	vertex/tet indices	parser完成后重建 coverage
margin	候选 summary	重算	global positive threshold	exact positivity和每项 lower bound
homotopy transversality	不得输入	由人工 theorem解释	不携带	formally derives
no-critical-zero	不得输入	由人工 theorem解释	不携带	formally derives
ambient isotopy	不得输入	current schema固定 pass	不携带	v0.1不推出
mesh correctness	constructor生成	独立重建	不携带	v0.1不推出

4. Lean representation

Lean 内明确分离 raw data 与 validity proposition：

VertexStarCertificate
  separator
  smoothMargin
  plMargin

VertexStarCertificate.ValidFor
  smoothMargin_pos
  plMargin_pos
  smoothLowerBound
  plLowerBound

serialized certificate 经 parser 得到 raw data；独立 executable checks构造 ValidFor。v0.1 prototype当前已经证明 “一旦 ValidFor 与 gradient box membership成立，就推出 homotopy transversality/no-critical-zero”，但 production JSON→Lean parser和 concrete fixture replay是下一阶段，不能把设计状态写成已实现。

5. Kernel verdict

formal verdict应由运行器从成功 theorem check产生，并与输入分离，例如：

{
  "theorem": "intervalVertexStarWitness_implies_noCriticalZero",
  "certificateHash": "sha256:...",
  "status": "kernel-checked",
  "scope": "homotopy-transversality-no-critical-zero"
}

status 是 verifier 输出，不得出现在 proof input 中。它也不得自动映射成 current Lane R actualIsotopy=pass。

6. Version evolution

• v0.1：exact star separator + interval algebra + no-critical-zero（当前）；
• v0.2 candidate：Lean 重建 uniform grid/Freudenthal/PL gradients/candidate confinement；
• v0.3 candidate：exact affine edge roots、normal disks、mesh buffer binding。独立 exact-root bundle schema/checker 已完成，但 JSON→Lean parser、normal disks 与 binary64 rounding isotopy 仍需关闭；
• v1.0 / Level 3：smooth→PL relative ambient isotopy、PL→mesh ambient isotopy、composition theorem。

任何版本升级都必须保持旧 schema 与 sealed evidence不可变；不能通过给 v0.1 增加 final claim常量来伪装 Level 3。