Lane R → Lean proof obligation mapping

状态：Phase 1 mapping complete

日期：2026-08-31

规则：formally proved 只表示当前 Lean project 内存在可编译、无 sorry theorem；TS Gate 的 satisfied 不自动等于 Lean proved。

1. 目标分解

最终 theorem 按两个中间对象拆解：

F⁻¹(0)
  -- smooth/PL homotopy regularity + relative ambient isotopy -->
F_PL⁻¹(0)
  -- exact normal disks + shared roots + stitching isotopy -->
M

Phase 1 只关闭第一条箭头中的 pointwise algebra：separator certificate 推出 local homotopy gradient 非零。

2. Requested obligations

#	Obligation	Existing Lane R asset	Lean Phase 1	仍缺
1	smooth implicit field 与 zero set	Typed Field IR evaluator、GeneralImplicit prerequisite、smooth-op allowlist	Vec/gradient 作为抽象 exact-real 输入；NoCriticalZero predicate	Field IR denotation、ContDiff、derivative correctness、zero-set subtype/manifold theorem
2	simplex、tetrahedron、simplicial complex	fixed grid/tet index arrays；mathlib 有 geometric/abstract complex	theorem 对任意 m-vertex simplex 的 barycentric weights 泛化	具体 tetra realization、nondegeneracy、face intersection、finite complex
3	Freudenthal tetrahedralization	0→6 main diagonal、每 cube 六 tet、checker 重建	未形式化	grid-to-complex 构造、六 tet 覆盖 cube、interiors disjoint、邻 cube conforming
4	PL scalar field F_PL	vertex samples、per-tet outward PL gradient	plGradient 为 abstract exact vector；homotopy algebra已证明	barycentric definition、shared-face continuity、gradient theorem、exact sampling semantics
5	vertex-star transverse witness	per relevant vertex separator、full-star smooth/PL margins	VertexStarCertificate.ValidFor；interval→dot 与 interpolated margin formally proved	global star incidence、AABB coverage、certificate parser/binding
6	smooth / PL gradient separation	TS outward interval dot checker	dotLower_le_dot、separator_margin_of_interval formally proved	binary64→exact interval soundness、Field derivative/PL derivative connection
7	F_t regularity / no-critical-zero	validation §3.2 mathematical argument	intervalVertexStarWitness_implies_homotopyTransverse、gradient_ne_zero、noCriticalZero formally proved	across-face generalized derivative、zero-set total space、projection regularity/properness
8	relative-boundary / ambient isotopy	candidate band interior + prose invocation of flow/isotopy extension	未形式化	compact-support flow、existence/uniqueness、boundary-fixed theorem、Palais/extension layer
9	tetrahedron 内 PL zero set / normal disk	checker rebuilds 3/4 edge roots and triangulates	未形式化	affine hyperplane∩tet classification、triangle/quad uniqueness、quad diagonal isotopy
10	sign-changing edge root 共享一致性	独立 projection + bundle checker 已 canonicalize、重建并 hash-bind exact roots；binary64 root 仍只作输出	exact affine root existence/open-interior/zero cancellation/on-segment 已形式化；JSON→Lean binding 与 rounding theorem 未完成	formal parser、exact normal disks、rounding isotopy
11	normal-surface mesh stitching	shared root map、topology checker、buffer identity	未形式化	face segment equality、disk interior disjointness、global embeddedness、orientation/link theorem
12	F⁻¹(0) ≃ F_PL⁻¹(0) ≃ M	current TS Gate claims pass	只证明第一箭头的 local no-critical algebra	两个 ambient isotopy theorem 与 composition

3. Existing PV3D matrix → formal status

PV3D	Existing Gate status	Formal status	Formal theorem / next object
01 theorem domain	satisfied	unfinished	bounded zero set、domain boundary separation、candidate confinement
02 interval arithmetic	satisfied	partial formally proved	exact interval dot sound；binary64 outward evaluator仍在 TS TCB
03 local parametrization	satisfied	partial formally proved	positive separator dot implies gradient nonzero；axis-specific IFT未接入
04 exact-zero policy	satisfied	unfinished	current certified path rejects zero grid vertices；Lean representation待建
05 deterministic edge vertex	satisfied	partial：exact shared-root kernel 与 TS bundle binding 已完成，binary64 output 仍被 audit finding 阻塞	JSON→Lean binding + exact-to-output perturbation theorem
06 face compatibility	satisfied	unfinished	conforming tet shared-face theorem
07 cube case partition	satisfied	not needed by new formal target	Formal Lane 复用 Freudenthal path，不重证 legacy cube corpus
08 accepted subset	satisfied	not needed by new formal target	同上
09 output combinatorics	satisfied	unfinished	finite triangle complex / closed oriented manifold theorem
10 face-bubble normalization	satisfied by stronger Gate	unfinished	smooth→PL ambient isotopy would subsume it
11 repeated-edge normalization	satisfied by stronger Gate	unfinished	smooth→PL ambient isotopy would subsume it
12 legacy local fan geometry	satisfied	not reimplemented	不是 certified Freudenthal constructor 的 formal target
13 local isotopy	satisfied	partial formally proved	local homotopy transverse/no-critical；local isotopy/relative boundary未证
14 global stitching	satisfied	unfinished	global continuous PL separator field + isotopy stitching
15 global mesh geometry	satisfied	unfinished / soundness blocker	exact normal surface embeddedness；binary64 diagonal-root finding先关闭
16 theorem conclusion	satisfied	unfinished	composed ambient isotopy
17 Hausdorff	satisfied by certified-adaptive companion	unfinished	工程 checker 已给出数值 displacement bound；Lean 尚未形式化 interpolation-error、flow length 与双向 Hausdorff theorem
18 adaptive octree	satisfied by certified-adaptive companion	unfinished	工程 checker 已重放 2:1 balance 与 zero-free transition annulus；Lean 尚未形式化 octree coverage、balance、transition exclusion 与 fine-band conformity

4. Theorem dependency graph

binary64/rational interval reconstruction
          │
          ▼
dotLower_le_dot ──► separator_margin_of_interval
                              │
barycentric nonnegative/sum=1 │
                              ▼
               interpolated_dot_ge_margin
                              │
        0 ≤ t ≤ 1 + positive endpoint margins
                              ▼
 intervalVertexStarWitness_implies_homotopyTransverse
                              │
                              ▼
             gradient_ne_zero / NoCriticalZero       [Phase 1 complete]
                              │
        generalized IFT + compact support + flow
                              ▼
              F⁻¹(0) ambient-isotopic F_PL⁻¹(0)
                              │
 exact Freudenthal normal disks + shared-root stitching
                              ▼
              F_PL⁻¹(0) ambient-isotopic M
                              │
                              ▼
          LaneRCertificate(F,M,C) → AmbientIsotopic(F⁻¹(0),M)

5. Claim vocabulary

• formally proved：Lean theorem 已编译，且 axiom audit 不含 sorryAx；
• imported theorem：mathlib theorem，proof term 仍由 Lean kernel 检查；
• axiom：本项目当前只接受 propext、Classical.choice、Quot.sound；
• conditional theorem：theorem 对 exact interval membership 等 premise 成立；如果这些 premise 仍由 TS 提供， end-to-end claim 还没有脱离 TS TCB；
• unfinished：没有 Lean proof；
• soundness blocker：现有 checker premise 不足以支持目标 theorem，不能靠增加测试改名为 proved；
• out-of-scope：Level 3 也不自动包含的 Hausdorff/adaptive claim。