symFull_explicit_eq_symFull_closed
plain-language theorem explainer
Full symmetrization of the explicit midpoint m² coefficient table agrees pointwise with full symmetrization of the closed-form coefficient table, for every six-tuple of indices in Fin 4. Cited when swapping the assembled Regge m² table for the closed rational bi-quadratic in the 4D exact midpoint Bloch identity. Proof pushes a uniform 1/32 scaling out of both sides and invokes the certified integer-table identity.
Claim. For all indices $a,b,c,d,i,j \in \{0,1,2,3\}$, the fully symmetrized six-index coefficient built from the explicit midpoint $m^2$ table equals the fully symmetrized coefficient built from the closed-form table (Frobenius, load, trace-squared, and trace-quadratic pieces).
background
This module closes the exact midpoint $m^2$ TT identity in 4D Regge analysis (scripted kernel certs and numerical assembly). The ambient object is a bi-quadratic form in a $4\times 4$ matrix field and a 4-wavevector, built from edge TT decompositions and the flat Hessian Bloch symbol.
The explicit midpoint $m^2$ coefficients are the assembled rational table of that second variation. The closed-form coefficient table packages four gated rational pieces: Frobenius diagonal $(-1/8)$, load $(1/4)$, trace-squared $(1/8)$, and trace-quadratic $(-1/4)$. Full symmetrization averages a six-index rational table over the index permutations that match the bi-quadratic contraction.
Upstream, each closed coefficient equals an integer table entry over 32, and the explicit $m^2$ coefficients admit the same $1/32$ presentation. A prior pointwise certificate identifies the closed table with its integer form; a parallel integer certificate equates the two fully symmetrized integer tables.
proof idea
Fix the six Fin-4 indices. Record two scaling identities: the explicit $m^2$ coefficient is definitionally the corresponding integer entry over 32, and the closed coefficient equals its integer entry over 32 by the pointwise closed-coefficient certificate.
Apply the generic rewrite that factors a uniform $1/32$ out of full symmetrization on each side. The claim reduces to equality of the two fully symmetrized integer tables, which is the certified rational identity between those tables. Three rewrites finish the proof; no case split on indices is needed at this layer.
why it matters
This is the table-level bridge used by the parent result that, for every symmetric $4\times 4$ matrix, the exact midpoint Bloch $m^2$ equals the closed bi-quadratic form. That parent chains: midpoint $m^2$ equals the bi-quadratic in the assembled coefficients; after full symmetrization those coefficients match the closed table; the closed table reproduces the closed form for every matrix (symmetry used only to reach the midpoint side).
In the Recognition gravity stack it discharges the computational half of exact_midpoint_m2_tt_identity, turning a 4096-entry rational certificate into an analytic identity for the 4D Regge Hessian at the midpoint stencil. It sits downstream of the kernel-cert and M2-assembly modules and unlocks the real bi-quadratic bridge section that follows in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.