exactActionSymbolStatus
plain-language theorem explainer
Boolean status package recording how far the exact flat Regge cross-term continuum symbol has been rebound on the Freudenthal torus. Continuum rebind, legacy fold retention, t11/t12 star offsets, and banked edge-origin m² certs are marked done; other-orbit incompleteness is cleared; ledger inhabit of S_RS and gap-action recovery stay false. Downstream flag theorems cite it by decide. The body is a pure structure literal of seven Bools.
Claim. The exact-action continuum-symbol status record is the 7-tuple of Booleans: continuum rebound to the exact flat cross-term is true; the distinct-hinge fold is retained as legacy true; $t_{11}$/$t_{12}$ star-member cube offsets are defined true; other-orbit offsets incomplete is false; edge-origin $m^2$ certificates are banked true; the Recognition ledger action $S_{RS}$ is inhabited false; gap-action recovery is false.
background
This module treats the exact flat cross-term continuum symbol for 4D Regge calculus on the Freudenthal torus. At flat background, deficits vanish, so Schläfli reduces the Hessian cross term to $S''=\sum_h (dA_h)(d\delta_h)$ on plane-wave class strains with position-resolved deficit phasing. The oracle target $H_{\mathrm{fold}}$ annihilates vertex-gauge modes and sends normalized TT on axisTTPlus/symbolDir to $-1/4$; the older distinct-hinge transported fold mis-transports (t12/t13 gauge residue) and is kept only as legacy.
The structure ExactActionSymbolStatus is a pure status package: seven Booleans that snapshot which pieces of that rebind are closed versus open. Sibling work defines t11 star-member cube offsets and t12/t13/t22 per-edge transported origins from the star-edge-origins analysis; edge-origin $m^2$ certificates for the banked gauge suite live in a companion module and are re-banked by the exact flat Hessian symbol assembly.
Module tags mark continuum Tendsto for all modes, ledger $S_{RS}$ inhabit, and gap-action recovery as still open. This definition does not itself prove any of those geometric claims; it only freezes the present flag vector.
proof idea
No proof. The declaration is a structure instance: seven field assignments of concrete Booleans. Downstream theorems exactActionSymbolStatus_flags and exact_action_srs_still_open recover those values by decide.
why it matters
Gives a single named snapshot of the exact-action continuum rebind so Preflight and local status lemmas can quote closed versus open work without re-deriving geometry. Downstream, exactActionSymbolStatus_flags packages the five true/false closed flags, and exact_action_srs_still_open records that $S_{RS}$ inhabit and gap-action recovery remain false: edge-origin $m^2$ decide-certs are banked elsewhere and do not inhabit the Recognition ledger action.
In the gravity analysis stack this sits under the $H_{\mathrm{fold}}$ pivot: the true flat Regge Hessian symbol on TT modes, distinct from the legacy mis-transported fold. It does not close ContinuumSymbolIs Tendsto, e0 isotropy, or Schläfli elevation of the nonlinear action for every orbit; those stay OPEN in the module doc. Framework-wise it is bookkeeping for the discrete gravity side (Regge Hessian assembly toward continuum symbols), not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.