ExactMidpointM2TTIdentityProved
plain-language theorem explainer
Boolean certificate that the exact midpoint Bloch m² transverse-traceless identity in 4D Regge analysis is closed. Gravity auditors and the m²-TT audit package cite it as the machine-checkable “proved” bit. The body is the constant true; the real work lives in the imported kernel, glue, and numerator-assembly modules.
Claim. The certificate flag for the exact midpoint $m^2$ transverse-traceless identity in four-dimensional Regge analysis is defined to be true.
background
This module sits in the 4D Regge gravity analysis stack. The local goal is the exact midpoint Bloch $m^2$ TT identity: a relation among the quadratic mass-coefficient of Bloch modes, the transverse-traceless edge decomposition, and the flat Hessian data at the midpoint configuration.
Sibling material in the same file introduces the 4×4 matrix and wave types, Frobenius and wave norms, the coupling $S$, the defect $\delta Q$, and the $m^2$ coefficient (with equalities to an explicit sum and to a numerator over a fixed denominator). Imports bring the flat Hessian Bloch data and symbol, the edge TT decomposition, kernel certificates, numerator assembly, and kernel glue.
The module doc states that this file closes exact_midpoint_m2_tt_identity, backed by the Python scripts that generated the kernel certificates and the identity check.
proof idea
Definitional certificate only: the flag is bound to the Boolean constant true. No tactics, no lemmas. The companion theorem exactMidpointM2TTIdentityProved_true discharges equality to true by rfl. Substantive content is assumed already assembled in the imported kernel-cert, numerator-assembly, and glue modules.
why it matters
Gives the audit layer a single named Boolean that the midpoint $m^2$ TT identity is closed. Downstream, exactMidpointM2TTIdentityProved_true re-exports the equality by reflexivity, and m2_tt_identity_audit_package packages that fact (with an axioms print) for the gravity analysis audit trail.
In the broader Recognition gravity program this is bookkeeping for the 4D Regge quadratic sector: once the midpoint Bloch $m^2$ TT identity is certified, Hessian and mode analyses can treat that algebraic relation as settled rather than open scaffolding. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is a local closure flag inside the discrete gravity analysis path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.