e_220022
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,2,0,0,2,2) equals eight times the explicit integer kernel at that same index. Gravity analysts cite it as one cell of the 256-case kernel table for the 4D Regge midpoint M2–TT identity. The proof is a single kernel decision (`decide`).
Claim. For indices $(a,b,c,d,i,j)=(2,2,0,0,2,2)$ in $(\mathbb{F}_4)^6$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 10 of a 256-case kernel certification that the folded numerator of the 4D Regge exact-midpoint M2–TT identity agrees with eight times a closed-form integer table. Indices run over $\mathbb{F}_4$ (four discrete directions).
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution contrib t a b c d i j. The comparison target explicitZ is a pattern-matched integer table on six $\mathrm{Fin},4$ arguments (sample entries $4$, $-2$, etc.).
The local claim is only the single multi-index $(2,2,0,0,2,2)$. Sibling theorems in the same chunk cover the neighboring index tuples; the assembly theorem quantifies over all six indices.
proof idea
One-line computational proof: by decide. Lean reduces both sides (the fold defining the numerator, and eight times the table lookup) to concrete integers and checks equality in the kernel. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and is proved by exhaustive fin_cases on all six $\mathrm{Fin},4$ indices, discharging each cell by a chunk theorem such as this one.
In the Recognition gravity stack this closes a finite algebraic identity in the 4D Regge midpoint analysis: the summed coupling numerator is exactly eight copies of the explicit kernel. It is bookkeeping for a certified discrete curvature/TT identity, not a continuum GR derivation. Landmark contact is indirect (discrete 4D structure supporting the gravity side of the RS program); it does not itself invoke T5–T8, RCL, or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.