exactMidpointM2TTIdentityProved_true
plain-language theorem explainer
Certifies that the exact midpoint Bloch m² transverse-traceless identity in 4D Regge analysis is marked proved. Gravity auditors and the m²-TT audit package cite it as the closed boolean gate for that identity. The proof is reflexivity: the certificate definition is the constant true.
Claim. The boolean certificate that the exact midpoint Bloch $m^2$ transverse-traceless identity holds in four-dimensional Regge analysis equals $\mathrm{true}$.
background
This module sits in the 4D Regge gravity analysis stack. It closes the exact midpoint Bloch $m^2$ TT identity: a discrete-curvature identity relating the midpoint-evaluated mass-squared coefficient for transverse-traceless wave modes to the TT edge decomposition of the flat Hessian.
Sibling material defines 4×4 matrices and wave data, Frobenius and wave norms, a coupling $S$, a defect $\Delta Q$, and the $m^2$ coefficient (assembled numerically and matched to an explicit form). Upstream imports supply the flat Hessian Bloch data and symbol, the edge TT decomposition, kernel certificates, numerical assembly of the $m^2$ numerator, and kernel glue.
The local setting is a machine-checked closure of a Python-scripted identity (regge_4d_m2_tt_identity and kernel certs). The named certificate is a Bool definition fixed to true once those pieces are in place.
proof idea
One-line term proof by reflexivity. The certificate definition is literally the constant true, so equality to true is rfl. No lemmas are applied; the mathematical work lives in the imported kernel certs, numerator assembly, and glue modules that justify setting the flag.
why it matters
Gives the audit layer a zero-axiom gate that the midpoint $m^2$ TT identity is closed. Downstream, m2_tt_identity_audit_package is exactly this equality and prints its axioms, so CI and paper appendices can treat the identity as discharged.
In the Recognition gravity program this is discrete-geometry bookkeeping for spin-2 / TT sector mass structure on the Regge complex, not a T0–T8 forcing step. It finishes the scripted 4D midpoint identity so later continuum or continuum-limit claims can assume the discrete TT $m^2$ match without reopening the kernel algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.