e_113232
plain-language theorem explainer
For the six Fin-4 indices (1,1,3,2,3,2), the midpoint m2 numerator equals eight times the explicit Z kernel value. Gravity analysts cite it when assembling the full pointwise identity m2Num = 8·explicitZ over the 4D index cube. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded midpoint numerator $m_2^{\mathrm{num}}(1,1,3,2,3,2)$ equals $8$ times the explicit integer kernel $Z(1,1,3,2,3,2)$.
background
This module is chunk 5 of a 256-case kernel certification that the Regge midpoint $m_2$ numerator equals eight times an explicit integer table $Z$ on every 4D multi-index. The ambient setting is discrete gravity analysis: couplings are summed over a fixed list, and the resulting integer is compared to a closed-form case table.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a contribution function over couplingZList, starting from zero. The comparison target explicitZ is a total function on six Fin 4 arguments that returns a small integer (typical values $\pm 2,,4$, and zero off the listed patterns).
Only the single sextuple $(1,1,3,2,3,2)$ is treated here; sibling lemmas cover the other points of the cube.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six indices are substituted into the fold definition of the numerator and the pattern-matching definition of the explicit kernel, so the kernel closes the equality with no further lemmas.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases. Each chunk lemma such as this one discharges one concrete cell, so the assemble proof is only case splitting plus these decides.
In the Recognition gravity stack this underwrites the exact midpoint $m_2$ identity used in 4D Regge analysis. It is bookkeeping rather than a forcing-chain step (T0–T8), but it is required before continuum or continuum-limit claims that quote the normalized kernel can be trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.