regge4DContinuumPreflightStatus_flags
plain-language theorem explainer
The 4D Regge continuum preflight status is locked to a fixed honesty ledger: Frobenius pin, EH coefficient freeze, decoys, and continuum-symbol bound are closed; continuum EH target, gauge-zero target, named SRS convergence, and named edge-TT remain open; gap-action recovery is false. Auditors of the QG continuum closure plan cite this instead of reading fields by hand. Proof is a single decidability check on the concrete status record.
Claim. The continuum preflight status satisfies: Frobenius pin closed, Einstein-Hilbert coefficient frozen, decoys frozen, and continuum-symbol bound closed are all true; continuum EH target open, gauge-zero target open, named $S_{RS}$ convergence open, and named edge-TT open are all true; and gap-action recovery equals false.
background
This module is the first binding increment of the 4D Regge continuum closure plan in the QG full-theory campaign. It freezes the independent continuum target, canonical mesh carrier, normalized transverse-traceless (TT) data, pure-gauge family, and honesty decoys before further computation. The module header is explicit: nothing here proves continuum recovery.
Frozen contracts include a canonical periodic Freudenthal 4-torus of side $N \ge 3$, Frobenius-normalized Euclidean TT polarizations, and an independently defined linearized Einstein-Hilbert quadratic using $\kappa_{\mathrm{einstein}}$ (not a free lattice scale). The named open continuum target asks that the exact flat cross-term symbol, $|k|^2$-normalized, match the EH coefficient on TT and vanish on pure gauge.
The status record is a boolean ledger of which of those contracts are already closed versus still open. Closed items are algebraic or definitional freezes; open items are geometric Tendsto-style continuum claims and named recovery goals still uninhabited.
proof idea
One-line wrapper: decide on the concrete value of the preflight status definition. That definition hard-codes each boolean field, so the long conjunction of equalities is a decidable closed term and reduces by reflection with no lemmas.
why it matters
In the module's tier tags this sits under THEOREM: status flags are binding honesty infrastructure for the continuum campaign. It records, in machine-checkable form, that Frobenius pin, EH coefficient freeze, decoys, and continuum-symbol bound are closed, while continuum EH target, gauge-zero target, named $S_{RS}$ convergence, and named edge-TT stay open, and gapActionRecovery is false.
That false gap-action flag and the open Tendsto targets match the module contract: banked algebraic face identities (for example discrete bookkeeping $2\cdot(-1/8)=-1/4$) must not be mistaken for geometric continuum recovery. The EH quadratic is frozen independently of the lattice symbol so later closers must observe equality, never fit a scale.
No downstream consumers are wired yet; the declaration is the audit snapshot for the preflight layer itself, not a step in a forcing chain (T0-T8) or mass-ladder argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.