e_000313
plain-language theorem explainer
Pointwise certificate that the midpoint numerator m2Num equals eight times the explicit kernel Z at index sextuple (0,0,0,3,1,3). One of 256 decide-kernel facts assembled into the full Fin-4 identity. Proof is a single kernel decision; no algebraic rewriting.
Claim. At indices $(a,b,c,d,i,j)=(0,0,0,3,1,3)$ in $(\mathrm{Fin}\,4)^6$, the midpoint 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 sits in the 4D Regge exact-midpoint analysis for the M2 TT identity. The numerator m2Num is the fold of coupling contributions over a fixed list: it sums contrib t a b c d i j for each term t in couplingZList. The comparison target explicitZ is a closed-form integer table on six Fin 4 indices (sample clauses include values 4, -2, and so on for particular patterns).
The local setting is chunk 0 of a 256-way kernel split: each chunk discharges a block of concrete sextuples by decide, so the later universal statement can be assembled by exhaustive fin_cases rather than by a single huge decision problem.
Upstream, only the two definitions matter: the fold that builds the numerator and the pattern-matching table that defines the explicit kernel.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the concrete sextuple (0,0,0,3,1,3) in the integer ring and checks equality. No lemmas are invoked; the kernel reduces the fold defining the numerator and the matching clause of the explicit table to numerals and compares them.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in (Fin 4)^6 by nested fin_cases and discharge of each point by a chunk certificate of this form. That universal equality is the algebraic core of the Regge exact-midpoint M2 TT identity in four dimensions: it replaces a summed coupling expression by eight times a sparse explicit kernel, which is what later gravity-analysis steps consume.
In the broader Recognition gravity stack this is bookkeeping infrastructure, not a forcing-chain landmark (T0–T8). It closes a finite computational obligation so the continuum-facing midpoint identity can cite a proved discrete equality rather than an unchecked table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.