e_030232
plain-language theorem explainer
For the six-index slot (0,3,0,2,3,2) on Fin 4, the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic decide-cell in the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,0,2,3,2)$ in $\{0,1,2,3\}$, the folded coupling numerator $N_2(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 256-cell kernel certification that the midpoint numerator of a 4D Regge-calculus mass-squared identity equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. the four spacetime directions.
The numerator $N_2$ (Lean m2Num) is defined by folding a fixed coupling list: start at 0 and add each term's contribution at the six indices. The explicit kernel $Z$ (Lean explicitZ) is a pattern-matched integer table on those same six indices (typical values $\pm 2,\pm 4$, etc.).
The local goal is pointwise equality $N_2=8Z$ at every hex-tuple, proved by exhaustive decide rather than symbolic algebra on the fold.
proof idea
One-line decide proof. Both sides are closed integer expressions once the six concrete Fin 4 arguments are substituted: the left side evaluates the fold of couplingZList contributions; the right side is eight times the matching clause of the explicitZ table. Lean’s kernel decision procedure checks the resulting integer equality.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N_2=8Z$ by fin_cases on all six indices and dispatch to these chunk cells. That global identity is the algebraic core of the exact midpoint M2/TT relation in the 4D Regge gravity analysis.
In the Recognition Science gravity stack this certifies that the discrete curvature/mass-squared numerator matches the closed-form kernel used downstream, so continuum or continuum-limit claims can quote a fully checked finite table rather than an unexpanded fold. It is pure bookkeeping scaffolding inside the gravity domain, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.