Lean-checked root-cone core
This release adds a reproducible Lean 4 formalization of the conceptual core of
the graviton root-cone result, pinned to Lean and mathlib v4.32.2.
The checked declarations cover:
- the spinor cut identity and zero-sum projected vector;
- directed cut/divergence cancellation;
- uniqueness of tree flow with prescribed divergence;
- strict tree-cut inequalities, positive flows, and open-root-cone membership;
- both retarded-orientation sign cases for
-cutBracket/pairBracket > 0.
All 17 principal theorems are guarded by assert_no_sorry, and their axiom
reports contain only Lean/mathlib's standard propext, Classical.choice, and
Quot.sound. GitHub Actions rebuilds with warnings treated as errors and runs
leanchecker. The existing exact-arithmetic and independent referee suites
also pass unchanged.
Verification status: Lean-checked, statement unaudited. The formalized core
has not yet received an independent informal-to-formal correspondence audit.
The chamber counts, determinant identities, realizability count, and five-point
formula remain outside Lean.
- Passing verification run for the immutable v0.3.0 tag
- See
FORMALIZATION.mdfor the manuscript-to-Lean map and audit checklist.