e_022023
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at multi-index (0,2,2,0,2,3) equals eight times the explicit integer kernel Z at those same Fin 4 indices. Gravity analysts cite it when assembling the global m2Num = 8·explicitZ identity over all 4^6 slots. Proof is a single kernel decide on concrete integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,0,2,3)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-way case split verifying $m_2^{\mathrm{num}}=8\cdot Z$ on the 4D Regge midpoint TT kernel. Indices run over $\mathrm{Fin},4$, labelling discrete edge/face slots in the midpoint stencil.
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 closed-form integer table on six $\mathrm{Fin},4$ arguments (sample entries: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$).
The local claim is one concrete cell of that table equality, needed before the assembler can quantify over all index tuples.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left by evaluating the fold of contrib over couplingZList at the fixed indices $(0,2,2,0,2,3)$, the right by looking up explicitZ and multiplying by 8. Lean’s kernel decision procedure discharges the resulting integer equality with no lemmas or case splits.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and is proved by exhaustive fin_cases on all six indices. Each chunk theorem such as this one pins a single cell so the global identity is a pure assembly of decided equalities rather than a symbolic expansion of the fold.
In the Recognition gravity stack this identity is part of the exact midpoint M2 TT analysis in 4D: it certifies that the discrete curvature/mass-squared numerator matches the closed kernel used downstream in Regge-type continuum limits. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure discrete linear-algebra bookkeeping inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.