v0.3.0 — Lean-checked root-cone core

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.md for the manuscript-to-Lean map and audit checklist.

v0.2.0 — reviewed working preprint

Working preprint release

This release publishes the revised working paper, exact-arithmetic verification programs, machine-readable chamber certificates, and an adversarial review package.

Principal result

The retarded half-collinear graviton multipoint vertex is identified with a weighted enumerator of directed spanning-tree root cones containing a kinematic netflow vector. This converts the global cut tests of arXiv:2603.04330 into root-cone membership conditions and gives directed Matrix-Tree Theorem formulas in arborescent chambers.

Verification included

• Direct checks of the published three-, four-, and decay-chamber formulas.
• Root-cone equivalence through valency six.
• Exhaustive four- and five-block resonance-chamber classification.
• 67 exact directed-Laplacian determinant checks.
• 22,102 exact checks of a non-decay five-graviton identity.
• Two independently written referee programs and a public response to the report.

Review status

The result has passed adversarial independent LLM review but has not yet been endorsed by an unaffiliated human expert. It is released for open checking and should not yet be treated as established literature.