Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D

show as:
view Lean formalization →

Packages the exact midpoint m² transverse-traceless identity for the 4D flat Regge Hessian Bloch symbol: unit-Frobenius TT modes give normalized quadratic form -1/8, pure gauge gives 0. Gravity analysts cite it when matching continuum TT second variation and closing weak-field quadratic recovery. The argument glues kernel-decide scale-32 Int certificates through algebraic lifts onto the rational coupling tables.

claimFor the exact midpoint Bloch symbol of the 4D flat Regge Hessian, the quadratic $m^{2}$ coefficient on a transverse-traceless symmetric $4\times 4$ polarization $H$ at wave covector $k\neq 0$ satisfies $m^{2}(H,k)/|k|^{2}=-1/8$ when $\|H\|_{F}=1$, and $m^{2}=0$ on pure-gauge polarizations. Certificates are realized by scale-32 integer tables and kernel-checkable fold identities equating packed rational $m^{2}$ coeffs to an explicit numerator.

background

In the QG full-theory campaign, the Stage-1 unit-cell exact flat Hessian is named as a finite trig polynomial over a 1208-row rational coupling table (each row: coupling $s=p/q$, edge displacements in ${0,1}^{4}$, doubled midpoint offset). The edge TT decomposition supplies the linear-algebra transverse-traceless split of symmetric $4\times 4$ real matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$.

Upstream kernel certificates are generated Int List.foldl facts on scale-32 tables, discharged by kernel decide only (no native_decide). Algebraic glue lifts Array-sum $m^{2}$ coefficients through those Int folds onto the $\mathbb{Q}$ tables used here. An assembly layer builds the numerator $m_{2}^{\mathrm{Num}}=8\cdot\mathrm{explicit}Z$ over all 4096 index tuples.

Local siblings name $4\times 4$ matrices and waves, Frobenius and wave norms, the coupling $s$, $\delta Q$, and equalities identifying the packed $m^{2}$ coefficient with its explicit rational form.

proof idea

Definition-and-certificate assembly rather than a single one-line wrapper. KernelCert supplies the decide-only Int certificates for the scale-32 tables. KernelGlue lifts Array-sum $m^{2}$ coeffs through Int folds to the rational coefficient tables. M2NumAssemble constructs $m_{2}^{\mathrm{Num}}=8\cdot\mathrm{explicit}Z$ over the full index set. This module casts those tables and proves the packed rational $m^{2}$ coefficient equals the explicit form, exposing the TT and pure-gauge evaluations that the Rayleigh faces consume.

why it matters in Recognition Science

Inhabits the certificate behind the typed residual exact_midpoint_m2_tt_identity used by the midpoint Bloch $m^{2}$ Rayleigh module: unit-Frobenius TT face $-1/8$, pure gauge $0$. RecognitionMeshExactJBridge4D attaches the Option-C midpoint Bloch symbol as the amplitude Hessian of the Recognition mesh action on the periodic Freudenthal 4-torus. ReggeNormalizationDerived4D compares against the continuum EH face $-(1/4)|k|^{2}|H|_{F}^{2}$ (derived from the Levi-Civita connection alone) to fix Regge's normalization constant. SRSConvergesEH4D exports the ledger-facing closer for weak-field quadratic action recovery. The companion audit module checks the axiom surface stays at propext, Classical.choice, Quot.sound.

scope and limits

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (47)