e_023002
plain-language theorem explainer
Single kernel identity: the folded M2 numerator at multi-index (0,2,3,0,0,2) equals eight times the explicit integer coupling Z at those same indices. Gravity analysts assembling the 4D Regge midpoint M2=8Z certificate cite this as one of the 256 decided cases. Proof is a pure `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,3,0,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-way kernel certification that the Regge exact-midpoint M2 numerator equals eight times an explicit integer table Z on all 4D multi-indices. The ambient setting is discrete gravity analysis: couplings on $\mathrm{Fin},4$ edges/faces are reduced to integer arithmetic so the identity can be machine-checked.
Upstream, m2Num is the fold of a contribution function over a fixed coupling list: it accumulates every term that can feed the midpoint numerator at a given six-tuple of $\mathrm{Fin},4$ indices. explicitZ is the closed-form integer table for the same indices (sample clauses include values $4$, $-2$, and so on). The claim is the pointwise equality of those two integers at one concrete tuple.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values (left via the fold definition of the numerator, right via the pattern-match table for explicit Z), and Lean’s decision procedure discharges the equality. No lemmas are invoked beyond the definitions of the two sides.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhaustive fin_cases and consumes each chunk theorem such as this one. That global equality is the certified algebraic core of the 4D Regge exact-midpoint M2–TT identity in the Gravity analysis stack. Within Recognition Science it is infrastructure for the discrete curvature/coupling side of the gravity sector, not a forcing-chain (T0–T8) step; it closes a finite integer kernel so later continuum or phenomenological claims can quote a fully decided numerator identity rather than an open computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.