e_011213
plain-language theorem explainer
For the six Fin-4 indices (0,1,1,2,1,3), the midpoint Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one cell of the 4D M2TT identity table. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}1$, $d{=}2$, $i{=}1$, $j{=}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 1 of a 256-cell decide table establishing the algebraic identity $m_2^{\mathrm{num}}=8\cdot Z$ on all sextuples of $\mathrm{Fin},4$ indices. The setting is the exact midpoint analysis of the 4D Regge M2TT kernel used in the Recognition gravity stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term $\mathrm{contrib},t,a,b,c,d,i,j$. The comparison value $\mathrm{explicitZ}$ is a piecewise integer table on the same six indices (typical entries $4$, $-2$, and so on for the nonzero patterns).
The full quantified statement is assembled downstream by exhaustive fin_cases over all six arguments; each chunk theorem such as this one discharges one concrete cell.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side by evaluating the fold of contrib over couplingZList at the fixed indices $(0,1,1,2,1,3)$, the right-hand side by looking up explicitZ at those same indices and multiplying by $8$. Lean’s kernel decision procedure checks integer equality.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which asserts the identity for every sextuple in $\mathrm{Fin},4$ by casing on each coordinate and invoking the matching chunk. That global equality is the certified algebraic core of the 4D Regge exact-midpoint M2TT identity used in the gravity analysis path.
Within Recognition Science this sits in the gravity domain rather than the T0–T8 forcing chain: it is bookkeeping that makes the discrete curvature/coupling kernel match its closed form, so later continuum or phenomenological claims can quote a fully decided integer identity instead of an unexpanded sum. No scaffolding remains on this cell; the open work, if any, is only assembly and use of the parent forall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.