e_023233
plain-language theorem explainer
For the six-index slot (0,2,3,2,3,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity in 4D cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(0,2,3,2,3,3)$ equals $8$ times the explicit integer kernel entry at the same indices: $N(0,2,3,2,3,3)=8\,Z(0,2,3,2,3,3)$.
background
This module is chunk 2 of a 256-cell case split proving that the Regge midpoint M2 numerator equals eight times an explicit integer kernel on all 4D index sextuples. The ambient setting is exact algebraic identities for discrete gravity (Regge-type) midpoint operators in four dimensions.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing local contributions at those six Fin-4 indices. The companion kernel $Z$ is an explicit piecewise integer function of the same six indices (sample values include $4$, $-2$, and so on on the diagonal and off-diagonal patterns).
The global claim is $\forall a,b,c,d,i,j,; N=8Z$. Each chunk theorem discharges one concrete sextuple so the assembler can finish by exhaustive fin_cases.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold that defines the numerator at $(0,2,3,2,3,3)$, the right-hand side multiplies the matching explicit kernel clause by 8. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for every Fin-4 sextuple by casing on all six indices and invoking the corresponding chunk cells. That global equality is the algebraic backbone of the exact midpoint M2 TT identity certificate in 4D discrete gravity analysis inside the Recognition Science gravity stack.
In the broader framework this is bookkeeping infrastructure rather than a forcing-chain landmark (T5–T8, RCL, phi). It closes one of 256 finite cases so the midpoint operator identity can be cited as fully machine-checked rather than schematic. No open physical hypothesis is at stake here; the work is pure finite verification of the numerator–kernel relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.