e_030233
plain-language theorem explainer
For the six-index slot (0,3,0,2,3,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these micro-identities when assembling the exact midpoint Regge M2 TT identity in 4D. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,0,2,3,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 a 256-case kernel certification that the discrete numerator of the midpoint Regge second-moment tensor equals eight times a tabulated integer kernel on six Fin-4 indices.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The comparison target explicitZ is a total function Fin 4^6 → ℤ given by an exhaustive pattern match (e.g. (0,0,1,1,2,2) ↦ 4, (0,0,1,2,1,2) ↦ −2, and so on).
Local setting (module doc): prove $m_2^{\mathrm{num}}=8\cdot Z$ case-by-case so a later assembler can discharge the universal statement by fin_cases.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are fixed: the left side evaluates the fold of contrib over couplingZList, the right side is 8 times the matching clause of explicitZ. Lean’s kernel decision procedure checks integer equality; no lemmas are invoked.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states ∀ a b c d i j, m2Num = 8 · explicitZ and proves it by exhaustive fin_cases on all six indices, each leaf pointing at a chunk identity such as this one.
In the gravity analysis stack these equalities certify the exact midpoint Regge M2 TT identity in 4D: the discrete second-moment numerator is completely determined by the explicit integer kernel Z. That identity is infrastructure for Recognition Science continuum limits of Regge calculus (spatial dimension D=3 forced upstream at T8; here the combinatorial 4D index set is Fin 4). No open scaffold remains on this leaf; it is a closed decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.