Regge4DContinuumPreflightStatus
plain-language theorem explainer
Status record for the 4D Regge continuum preflight: nine Booleans tracking which frozen contracts are closed and which continuum closers remain open. Gravity analysts cite it to read campaign state without opening the ledger Props. Pure structure definition; the concrete assignment lives in the sibling value of the same name.
Claim. A record type with Boolean fields reporting whether the Frobenius pin, the independently frozen Einstein-Hilbert coefficient, the honesty decoys, and the concrete continuum-symbol binding are closed, and whether the continuum EH target, gauge-zero target, named $S_{\mathrm{RS}}\to\mathrm{EH}$ convergence, named edge-TT split, and gap-action recovery remain open.
background
This module is the first binding increment of the 4D continuum closure plan in the QG full-theory campaign. It freezes the independent continuum target, canonical mesh carrier, normalized TT data, pure-gauge family, and honesty decoys before further computation. Nothing in the module proves continuum recovery.
The continuum symbol is the $|k|^2$-normalized concrete exact-action finite Hessian along the Freudenthal 4-torus family $N=j+3$: the sequence is definitionally the exact midpoint Bloch symbol, not a constant face and not an existential witness. The packaged ledger closer is the conjunction of the continuum EH target and the gauge-zero target (weak-field quadratic action only).
Decoy D4 excludes arbitrary test-variation pullbacks: only a Recognition-native mesh bridge may inhabit the action theorem. Banked algebraic identities (discrete bookkeeping $2\cdot(-1/8)=-1/4$, gauge face $0$) do not inhabit the geometric Tendsto Props.
proof idea
No proof: this is a structure declaration. Nine Boolean fields name the closed/open axes of the preflight. The sibling value assigns concrete flags (Frobenius pin, EH coefficient, decoys, and continuum-symbol binding closed; continuum EH target and related ledger Props left open).
why it matters
Gives a single typed snapshot of what the continuum preflight has frozen versus what remains open, so later modules cannot silently treat open Tendsto Props as closed. The sole direct consumer is the concrete status value in this module, which sets frobenius pin, EH coefficient, decoys, and continuum-symbol binding to closed and leaves continuum EH target, gauge zero, named SRS convergence, edge-TT, and gap-action recovery open.
That split matches the module contract: THEOREM tier for pins, decoys, and symbol uniqueness; OPEN for continuum Tendsto value Props and the uninhabited packaged closer. It enforces the honesty rule that the EH quadratic is frozen independently of the lattice symbol, so a later algebraic closer must observe equality rather than fit a scale. No T0-T8 forcing step is discharged here; this is campaign bookkeeping for 4D Regge continuum recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.