e_302311
plain-language theorem explainer
For the single index tuple (3,0,2,3,1,1) in (Fin 4)^6, the folded M2 coupling numerator equals eight times the explicit Z kernel entry. Gravity analysts cite it when assembling the full pointwise identity m2Num = 8·explicitZ over the 4D Regge midpoint TT kernel. The proof is a pure `decide` on concrete integer arithmetic.
Claim. At discrete indices $(a,b,c,d,i,j)=(3,0,2,3,1,1)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 256-case kernel certification that the midpoint M2 numerator matches eight times an explicit integer kernel on every 4-index pattern. The ambient setting is 4D Regge-exact midpoint analysis for the TT sector of the discrete gravity operator.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each local contribution contrib at the six Fin-4 slots. The comparison target explicitZ is a hand-written total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ that tabulates the expected kernel values (examples in the cert module include $4$, $-2$, and other small integers on distinguished patterns).
Chunk 12 isolates a block of those patterns so each equality can be discharged by kernel decision rather than by a single giant tactic.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are fixed at 3,0,2,3,1,1, so the decision procedure checks integer equality with no further lemmas.
why it matters
Feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is a leaf of that case split.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint TT kernel in 4D Regge analysis: once numerator and explicit kernel agree pointwise up to the factor 8, downstream curvature and continuum-limit arguments can quote a closed algebraic form instead of a folded sum. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure discrete-kernel algebra supporting the gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.