e_232133
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,3,2,1,3,3) equals eight times the explicit integer table at those same indices. Gravity analysts cite it when assembling the full 4D Regge midpoint M2TT numerator identity over (F_4)^6. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,b{=}3,c{=}2,d{=}1,i{=}3,j{=}3$ in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 11 of a 256-way case split proving that the 4D Regge midpoint M2TT numerator equals eight times a closed-form integer table. The ambient setting is discrete gravity analysis: index sextuples range over $\mathbb{F}_4$, and the numerator is obtained by folding a fixed coupling list.
Upstream, m2Num is defined as the fold of contrib over couplingZList, yielding an integer for each sextuple. explicitZ is a pattern-matched integer table on the same domain (sample clauses give values such as $4$, $-2$, etc.). The local claim is one concrete instance of $m_2^{\mathrm{num}}=8Z$.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(2,3,2,1,3,3)$ and checks integer equality. No lemmas are invoked beyond the kernel definitions of the numerator fold and the explicit table.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathbb{F}_4$, $m_2^{\mathrm{num}}=8Z$, by exhaustive fin_cases over the six indices. Each chunk theorem such as this one discharges one leaf of that case tree. In the broader Recognition gravity stack this closes the algebraic identity between the summed coupling numerator and the explicit midpoint table used in the 4D Regge M2TT analysis. It is pure discrete bookkeeping, not a continuum GR claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.