e_200323
plain-language theorem explainer
For the six-index slot (2,0,0,3,2,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the exact midpoint M2 TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2,b=0,c=0,d=3,i=2,j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2 TT identity certification. The local goal, stated in the module header, is to prove $m_2^{\mathrm{num}}=8\cdot Z$ on a block of the $4^6$ index space by kernel decides (256 decides per chunk).
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $Z$ is an explicit integer table on six $\mathrm{Fin},4$ arguments (sample entries include $4$, $-2$, and other small integers on diagonal and off-diagonal patterns).
Both definitions live in the kernel certificate module imported here. The present declaration fixes one concrete sextuple rather than quantifying over all indices.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side by evaluating the fold of contributions at $(2,0,0,3,2,3)$, the right-hand side by looking up or computing $8\cdot Z(2,0,0,3,2,3)$. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and discharges the claim by exhaustive fin_cases on all six indices, each case pointing at a chunk equality such as this one.
In the gravity analysis stack this identity is the algebraic core of the exact midpoint M2 TT relation in 4D Regge calculus: once the folded numerator matches the closed kernel everywhere, midpoint curvature bookkeeping becomes an equality of integers rather than a floating approximation. It is pure discrete GR bookkeeping inside Recognition Science gravity, not a forcing-chain (T0–T8) step, but it underwrites exact discrete curvature identities used downstream of the continuum limit story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.