e_202302
plain-language theorem explainer
For the six-index tuple (2,0,2,3,0,2) 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–TT identity in 4D. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=0$, $c=2$, $d=3$, $i=0$, $j=2$ in $\mathrm{Fin}\,4$, the summed coupling numerator equals eight times the explicit integer kernel: $N(2,0,2,3,0,2)=8\,Z(2,0,2,3,0,2)$.
background
This module is one chunk of a 256-case kernel certification that the Regge midpoint mass-squared numerator in 4D equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, matching the four spacetime directions of the discrete geometry.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing local contributions at those six indices. The comparison table $Z$ is an explicit pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (typical nonzero values $\pm 2,,4$). The local claim is the equality $N=8Z$ at one concrete sextuple.
The surrounding analysis sits in the gravity layer of Recognition Science, where discrete Regge-type curvature and midpoint identities are certified before continuum limits.
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 $(2,0,2,3,0,2)$, the right-hand side multiplies the pattern-matched kernel entry by eight. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases over all $4^6$ index tuples and dispatches each case to a chunk theorem of this form. Without the pointwise decides, the global identity does not close.
In the gravity analysis stack this identity is the algebraic backbone of the exact midpoint M2–TT relation in 4D discrete geometry. It is bookkeeping rather than a new physical law, but it is required scaffolding before continuum or continuum-limit statements can be trusted. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; those enter only at higher layers that consume the certified kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.