e_030122
plain-language theorem explainer
One concrete index sextuple of the 4D midpoint Regge identity: the mass-squared numerator at (0,3,0,1,2,2) equals eight times the explicit Z kernel there. Gravity analysts cite it only as a discharged case inside the full assembly over Fin 4^6. The proof is a single kernel `decide` on two closed integer expressions.
Claim. For the index tuple $(a,b,c,d,i,j)=(0,3,0,1,2,2)$ in $(\mathrm{Fin}\,4)^6$, the folded mass-squared 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 3 of a case-split certification that the 4D midpoint Regge mass-squared numerator equals eight times an explicit integer kernel on every sextuple of indices in $\mathrm{Fin},4$. The ambient setting is discrete gravity analysis: couplings are summed into a numerator m2Num, defined by folding a contribution function over a fixed coupling list.
The comparison target explicitZ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite pattern of integer values (for example $4$, $-2$, and other small entries on selected index patterns). The identity $m_2^{\mathrm{num}}=8\cdot Z$ is the algebraic content being certified pointwise before assembly.
Upstream, both sides are pure definitions in the kernel-cert module; no analytic hypotheses remain once the six indices are fixed.
proof idea
Both sides specialize to closed integer terms once the six Fin 4 arguments are the literals 0,3,0,1,2,2. The proof is the single tactic decide, which evaluates the fold defining the numerator and the matching clause of explicitZ, then checks integer equality in the kernel. No lemmas are invoked beyond that evaluation.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ and discharges the universal quantifier by exhaustive fin_cases. Each chunk lemma such as this one closes one concrete goal in that $4^6$-way split (module doc: "256 kernel decides" per chunk family).
In the Recognition gravity stack this is bookkeeping infrastructure for the exact midpoint Regge $M^2$ identity in 4D, not a new physical law. It does not itself invoke the forcing chain (T0–T8), RCL, or $\phi$-ladder mass formulae; those sit upstream of why a 4D Regge kernel is the right object. Its value is that the assembled equality becomes a zero-sorry theorem once every index cell is decided.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.