e_022301
plain-language theorem explainer
For the six-index slot (0,2,2,3,0,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over the 4D Regge midpoint kernel. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}2$, $d{=}3$, $i{=}0$, $j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,2,2,3,0,1)=8\,Z(0,2,2,3,0,1)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $N=m2Num$ is obtained by folding a fixed coupling list and summing a local contribution at each tuple. The comparison target $Z=explicitZ$ is a sparse closed-form table of small integers (entries such as $4$, $-2$, and defaults).
This module is chunk 2 of a 256-way case split that discharges $N=8Z$ pointwise by kernel computation. The ambient goal is the exact midpoint mass-squared identity in the Recognition gravity stack, where discrete curvature couplings must match an explicit algebraic form before continuum limits are taken.
Upstream, $m2Num$ and $explicitZ$ are pure definitions in the kernel certificate module; no analytic hypotheses are attached to this pointwise equality.
proof idea
One-line decide proof. Both sides reduce to concrete Int values once the six indices are substituted into the fold definition of $m2Num$ and the pattern table of $explicitZ$; the kernel checks integer equality. No lemmas beyond evaluation of those two definitions are required.
why it matters
Feeds the assembler theorem $m2Num_eq_eight_explicitZ$, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m2Num=8\cdot explicitZ$ by exhaustive fin_cases over the six indices and invocation of the chunk equalities. That global identity is the algebraic backbone of the Regge exact midpoint $M^2$ TT certificate in 4D.
Within Recognition Science gravity work, matching the folded coupling numerator to eight times the explicit kernel is a discrete consistency check on the curvature/mass-squared side before continuum or continuum-limit claims. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is infrastructure inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.