regge4DAlgebraicCloserStatus
plain-language theorem explainer
Status ledger for the 4D Regge algebraic closer: four banked algebraic witnesses are marked closed and five continuum targets stay open. Gravity analysts cite it when auditing what the campaign has actually proved versus what remains named but unproved. The body is a pure structure literal of boolean constants.
Claim. The 4D Regge algebraic-closer status record sets decoy one-orbit closed, plus/cross TT witnesses closed, gauge $m^2$ symbol closed, and full zero-momentum moment closed to true, while full TT isotropy, pure-gauge vanishing, plus/cross continuum agreement, $S_{\mathrm{RS}}\to\mathrm{EH}$ convergence in 4D, and gap-action recovery remain false (open).
background
This module is the 4D counterpart of the Regge TT algebraic closer in the quantum-gravity full-theory campaign. It consumes the frozen continuum preflight target and the geometry-derived hinge-orbit / $(1,1)$-symbol stack, then banks every immediately available algebraic identity while naming the remaining continuum targets as open propositions with status flags set to false.
Banked content (already proved upstream) includes: the decoy one-orbit $(1,1)$ $m^2$ symbol equals $-3$, not the Einstein–Hilbert TT coefficient $-1/4$; Frobenius-normalized plus and cross tensors inhabit the 4D TT-polarization predicate; the gauge decoy has vanishing $(1,1)$-orbit $m^2$ symbol; and the full zero-momentum moment, summed over hinge-orbit types, matches the true-weight quadratic and vanishes on axis TT-plus and decoy gauge.
Open named targets include full TT isotropy at the EH coefficient for every nonzero direction and every normalized TT polarization, pure-gauge vanishing for every direction, and plus/cross continuum agreement. The status structure is the single place those open/closed bits are recorded.
proof idea
Definitional structure literal: each field of Regge4DAlgebraicCloserStatus is assigned a boolean constant. The four banked algebraic identities receive true; full TT isotropy, pure-gauge vanishing, plus/cross agreement, SRS-to-EH convergence, and gap-action recovery receive false. No tactics, no lemmas, no computation.
why it matters
Gives the campaign an auditable ledger so downstream honesty theorems can quote the flags rather than restate prose. Used by regge4DAlgebraicCloserStatus_flags, which packages the eight boolean equalities, and by banked_does_not_flip_gap_or_isotropy, whose doc-comment states that banked one-orbit identities do not inhabit the open isotropy target and that the ledger flag stays false (also that the axis TT-plus $m^2$ symbol is not the EH coefficient $-1/4$).
Module disclosures bind the record: it does not prove $S_{\mathrm{RS}}$ converges to EH in 4D, does not flip gap-action recovery, and treats zero-momentum full-moment identities as banked witnesses only; finite-momentum EH Tendsto lives in the transported closer as open. In the broader Recognition gravity stack this is bookkeeping for the 4D Regge continuum limit, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.