status_flags_grounded
plain-language theorem explainer
Each Boolean in the Regge TT symbol preflight status record is paired with its mathematical content at lattice size N=3: flat deficits and action vanish, the frozen conformal identification holds, the TT second-difference is even, a concrete TT polarization exists, and the continuum-symbol flag is false. Stage-1 auditors and anyone citing the protocol record use this grounding. The proof is a pure term pairing of rfl on the Bools with the named kernel lemmas.
Claim. At $N=3$ on the canonical periodic Freudenthal torus: the flat-deficit flag is true and every edge deficit of the flat squared-length field is zero; the flat-action flag is true and the true nonlinear Regge action at flat is zero; the frozen-identification flag is true and for every vertex potential $u$, the concrete Regge action on the conformal edge field equals the true action on the typed conformal edge field; the symbol-symmetry flag is true and the TT second difference is even in the amplitude $t$; the TT-constraint flag is true and the axis wave vector with the plus polarization is a valid TT polarization (symmetric, traceless, transverse, unit Frobenius norm); and the continuum-symbol-value flag is false.
background
This module is Stage 1 of the QG full-theory campaign on the Regge TT continuum symbol. It defines the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus as a function of an arbitrary edge squared-length field: $S(\ell)=\sum_e\sqrt{\ell_e},(2\pi-\sum\theta)$, with dihedral angles from Cayley-Menger. The deficit and action machinery is reused, not re-derived.
The ambient lattice is the periodic cubic Freudenthal triangulation: vertices are $\mathrm{Fin},N^3$, edges are positive-displacement periodic edges, and incidence comes from the canonical periodic triangulation with a consistency certificate. The flat edge field is the unit squared-length assignment; conformal fields are those pulled back from a vertex potential via the stencil map toPotential.
A TT polarization for an integer wave vector $m$ is a symmetric, traceless, $m$-transverse, Frobenius-normalized $3\times 3$ matrix. The continuum isotropy claim (symbol equal to $-(1/4)$ times the TT projector on all preregistered directions) is numerical evidence only and remains OPEN.
proof idea
Pure term-mode conjunction. Each true flag is rfl on the status Bool, paired with the corresponding kernel lemma instantiated at $N=3$:
- flat deficits:
deficitOfField_flatEdgeField 3; - flat action:
trueReggeAction_flatEdgeField 3; - frozen identification:
reggeAction_conformal_eq 3 ufor arbitrary vertex potential $u$; - symbol evenness:
ttSecondDifference_even 3 E k t; - non-vacuous TT set:
axisTTPolarizationPlus_isTT.
The final conjunct is rfl pinning the continuum-symbol flag to false. No tactics, no new reasoning.
why it matters
This is the honesty certificate for the Stage-1 protocol record ReggeTTSymbolPreflightStatus. Downstream, the status structure and axisWaveVector_ne_zero rely on these grounded flags so that OPEN-target hypotheses are instantiated non-vacuously rather than by bare Booleans.
In the campaign hierarchy it closes the preflight tier: true-action definition, kernel-checked flat point, exact frozen-model identification along the conformal family, well-formedness of the TT Bloch symbol object, and non-vacuity of the TT constraint set. It deliberately leaves ReggeTTContinuumIsotropyTarget open (flag false), matching the module rule that C10 continuum isotropy with value $K(0)=-(1/4),I_{TT}$ is numerical evidence, not a theorem.
No Recognition forcing-chain landmark (T5-T8, RCL, phi) is directly invoked; the result is lattice gravity infrastructure feeding the continuum TT symbol program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.