e_032303
plain-language theorem explainer
Pointwise check that the Regge midpoint mass-squared numerator equals eight times the explicit Z coupling at multi-index (0,3,2,3,0,3) in Fin 4. Gravity analysts cite it as one cell of the 256-kernel case split proving the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,2,3,0,3)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
This module is chunk 3 of a brute-force verification that the 4D Regge midpoint mass-squared numerator agrees with eight times a closed-form coupling table. The ambient setting is discrete gravity analysis: curvature and mass terms are assembled from finite-index couplings on $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed list of coupling contributions over six $\mathrm{Fin},4$ indices and summing integer increments. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on the same six indices (sample clauses include values $4$, $-2$, and so on for distinguished index patterns).
The local claim is one concrete cell of that table equality. Upstream, both sides are pure definitions; no analytic lemma is required beyond evaluating the fold and the match.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,3,2,3,0,3)$. The left side reduces by unfolding the fold over couplingZList and summing contrib terms; the right side reduces by matching explicitZ and multiplying by 8. Equality of the resulting integers is discharged by the kernel decision procedure.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $\mathrm{Fin},4$ by exhaustive fin_cases. That global equality is the certified algebraic core of the Regge exact midpoint $M_2$–TT identity in 4D: it replaces a summed contribution list by a sparse explicit coupling, which is what later gravity lemmas quote.
Within Recognition Science gravity analysis this is scaffolding for the discrete curvature/mass bookkeeping, not a forcing-chain (T0–T8) step. It closes one of the 256 kernel cells named in the module doc so the assemble proof can finish without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.