e_312223
plain-language theorem explainer
Case check that the folded coupling numerator m2Num equals eight times the explicit integer table explicitZ on the multi-index (3,1,2,2,2,3) in (Fin 4)^6. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite it as one kernel cell. The proof is a single decide on two concrete integers.
Claim. For indices $a=3$, $b=1$, $c=2$, $d=2$, $i=2$, $j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit table value: $\mathrm{m2Num}(3,1,2,2,2,3)=8\cdot\mathrm{explicitZ}(3,1,2,2,2,3)$.
background
This module is chunk 13 of a brute-force certification that the 4D Regge-midpoint M2 numerator agrees with an explicit closed form. The ambient setting is discrete gravity analysis: couplings on a 4-index simplex lattice are summed, then matched against a sparse integer table.
The numerator m2Num 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 pattern-matched integer table on six Fin 4 arguments (typical nonzero entries are $\pm 2$ or $4$). The claimed relation on every cell is m2Num = 8 · explicitZ.
Upstream, both sides are pure definitions in the kernel certificate module; no analytic lemma is required beyond evaluating those definitions at a concrete multi-index.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the fixed indices $(3,1,2,2,2,3)$ to concrete integers (the fold for the numerator, the match for the table) and checks equality in Int. No lemmas are invoked beyond the decidable equality instance.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the identity for all six Fin 4 indices and proves it by exhaustive fin_cases. Each leaf such as this one discharges a single cell; without the chunk theorems the assembly cannot close.
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint M2–TT relation in 4D Regge calculus, not a forcing-chain landmark (T5–T8) by itself. It removes a sorry-shaped gap in the discrete curvature algebra so later continuum or continuum-limit arguments can quote a fully certified numerator. Open analytic content (why the factor 8 appears, continuum meaning) lives above this kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.