ExactHessianSymbolStatus
plain-language theorem explainer
Status record for the exact flat 4D Regge Hessian Bloch-symbol program: seven boolean flags tracking oracle validation, gauge battery, same-shell isotropy, algebraic m² table presence, edge-origin m² banking, SRS inhabitation, and gap-action recovery. Gravity analysts cite it as the honest checklist for what is closed versus still open on the flat Hessian. It is a plain structure definition with no proof content.
Claim. A status package is a 7-tuple of booleans: (oracle validated, gauge battery pass, same-shell isotropy, algebraic $m^2$ table present, edge-origin $m^2$ banked, $S_{RS}$ inhabited, gap-action recovery). Each flag records whether the corresponding certificate or construction for the exact flat Regge Hessian symbol in 4D is presently closed.
background
The module studies the second variation of the 4D Regge action $S=\sum_h A_h\delta_h$ at a flat background. Every deficit vanishes, so Schläfli reduces $S''$ to the cross term $\sum_h (dA_h)(d\delta_h)$ in squared-length coordinates; no off-flat Schläfli primitive is required.
Stage-1 algebraic work produces an $m^2$ density on TT polarizations that is isotropic, $Q_{m^2}(H,k)=(-1/8)|H|_F^2|k|^2$, hence $-1/4$ on the banked axis-TT-plus face and $0$ on pure gauge. Edge-origin certificates (from the sibling edge-origins evaluator) close four named modes on symbolDir: TT plus/cross at $-1/4$, decoy and counterexample gauges at $0$.
The structure is the §5 "honest status package": a single place to record which of those certificates (and which larger ledger claims) are actually banked, without pretending a general $\mathbb{Q}(\sqrt{\cdot})$ coupling table or full gap-action recovery exists yet.
proof idea
No proof: this is a structure declaration. Seven named Bool fields package the checklist. Downstream, a single definition inhabits the structure by assigning concrete booleans (oracle, gauge battery, isotropy, and edge-origin banking true; algebraic $m^2$ table false; SRS and gap-action recovery left unset in the visible inhabitant snippet).
why it matters
In the Regge exact-flat-Hessian line, this structure is the audit surface for what Lean actually owns. The inhabitant exactHessianSymbolStatus sets oracle validation, gauge battery, same-shell isotropy, and edge-origin $m^2$ banking to true, while keeping algebraicM2Table false, matching the module claim that decide-certs on named modes are not a general algebraic $C_{abcdij}$ table.
That honesty matters for Recognition gravity: the flat Hessian symbol is the bridge from discrete hinge geometry to continuum TT kinetics (Einstein–Hilbert coefficient comparisons live as siblings). Banking TT $\to -1/4$ and gauge $\to 0$ without flipping gap-action recovery or inhabiting the full recognition ledger $S_{RS}$ keeps the forcing chain clean: local symbol facts do not silently claim global action recovery.
Downstream consumers read one record instead of hunting scattered theorems when asking whether the 4D flat symbol is ready for continuum matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.