e_222011
plain-language theorem explainer
For the six-index slot (2,2,2,0,1,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these pointwise identities when assembling the global Regge midpoint M2=8Z certificate. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(2,2,2,0,1,1)$ equals eight times the explicit integer kernel at the same slot: $N(2,2,2,0,1,1)=8\,Z(2,2,2,0,1,1)$.
background
This module is one chunk of the 4D Regge exact-midpoint identity that asserts the folded numerator equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels ${0,1,2,3}$.
The numerator $N=m2Num$ is defined by folding a fixed coupling list: start at $0$ and add a contribution for each coupling triple at the six indices. The closed form $Z=explicitZ$ is a sparse integer table on those same six indices (typical nonzero entries are $\pm 2,\pm 4$).
The local goal, stated in the module header, is the pointwise identity $N=8Z$ discharged by kernel decides, split across chunks so each file stays small. Downstream assembly recombines every slot into a single $\forall$ statement.
proof idea
One-line proof by decide. Both sides are closed integer expressions once the six concrete Fin 4 arguments are substituted: the left folds a finite coupling list of contributions, the right looks up the matching clause of the explicit table (or defaults). Lean’s kernel decision procedure compares the two evaluated integers and closes the goal.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ by exhaustive fin_cases on all six indices and dispatch to these chunk lemmas. That global equality is the algebraic core of the Regge exact-midpoint M2–TT identity in 4D: the continuum-side numerator matches eight copies of the discrete kernel table.
In the Recognition gravity stack this is bookkeeping, not a new physical law. It certifies that the discrete curvature/coupling combinatorics used in the midpoint scheme agree with the explicit integer kernel before continuum or phenomenological limits are taken. No forcing-chain landmark (T5–T8) is at stake here; the result is pure finite arithmetic supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.