regge4DAlgebraicCloserStatus_flags
plain-language theorem explainer
The 4D Regge algebraic-closer status record is frozen with four banked flags true and five open flags false. Anyone auditing the QG full-theory campaign cites this to confirm the ledger matches the module header: one-orbit decoy, plus/cross TT witnesses, gauge m² vanishing, and full zero-momentum moment are closed; full TT isotropy, pure-gauge vanishing, plus-cross agreement, SRS→EH convergence, and gap action recovery remain open. Proof is a single decidability check on the concrete Boolean fields.
Claim. The status record of the 4D Regge algebraic closer satisfies: decoy one-orbit identity closed $=\mathrm{true}$, plus/cross TT witnesses closed $=\mathrm{true}$, gauge $m^2$ symbol closed $=\mathrm{true}$, full zero-momentum moment closed $=\mathrm{true}$, while full TT isotropy closed $=\mathrm{false}$, pure-gauge vanishing closed $=\mathrm{false}$, plus-cross agreement closed $=\mathrm{false}$, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence $=\mathrm{false}$, and gap action recovery $=\mathrm{false}$.
background
This module is the 4D counterpart of the Regge TT algebraic closer in the QG full-theory campaign. It consumes the frozen continuum preflight target and the geometry-derived orbit / (1,1)-symbol stack, banks every immediately available algebraic identity, and names the remaining full TT isotropy, pure-gauge, and plus-cross agreement goals as open propositions with status flags set to false.
Banked content (per the module header) includes: the decoy one-orbit $(1,1)$ $m^2$ symbol equals $-3$, not the frozen Einstein-Hilbert TT coefficient $-1/4$; plus and cross Frobenius-normalized TT witnesses inhabit the 4D TT-polarization predicate; the gauge $(1,1)$-orbit $m^2$ symbol on the decoy gauge vanishes; and the full zero-momentum moment, summed over hinge-orbit types, matches the true-weight zero-momentum quadratic and vanishes on axis TT plus and decoy gauge.
The status structure is a concrete Boolean ledger. This theorem only asserts that the ledger values match the intended closed/open partition; it does not itself prove the underlying geometric identities.
proof idea
One-line decidability proof. The status definition hard-codes nine Boolean fields; decide evaluates the nine equalities and the nested conjunction, which holds by construction of that record. No geometric lemmas are invoked at this step.
why it matters
In the Recognition Science gravity stack this is the honesty seal for the 4D Regge algebraic closer: it locks the campaign ledger so banked one-orbit and zero-momentum witnesses cannot be silently reclassified as the open full TT isotropy or continuum EH targets. Downstream consumers (none yet wired in the graph) and human auditors rely on these flags to separate what is proved from what remains named-open.
The module header is explicit: this does not prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, does not flip gap action recovery, and does not inhabit the open isotropy target with the banked zero-momentum identities. Continuum symbol work and finite-momentum EH Tendsto live in the transported closer as open. The theorem therefore enforces the disclosure boundary of the 4D campaign rather than advancing a new physical identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.