e_120133
plain-language theorem explainer
For the six-index slot $(1,2,0,1,3,3)$ on $\mathrm{Fin}\,4$, the folded Regge coupling numerator equals eight times the explicit integer table. Gravity analysts cite it only as one cell of the $m_2$ numerator identity. The proof is a single kernel `decide` on concrete integers.
Claim. Let $m_2$ be the integer obtained by folding the coupling contribution list at multi-index $(a,b,c,d,i,j)=(1,2,0,1,3,3)\in(\mathrm{Fin}\,4)^6$, and let $Z$ be the explicit integer lookup at the same multi-index. Then $m_2(1,2,0,1,3,3)=8\,Z(1,2,0,1,3,3)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local goal, stated in the module header, is to discharge $m_2\mathrm{Num}=8\cdot\mathrm{explicit}Z$ on a block of kernel cases by pure decision.
Upstream, $m_2\mathrm{Num}(a,b,c,d,i,j)$ is defined as the fold of couplingZList, accumulating each term's contribution at the six $\mathrm{Fin},4$ indices. The companion table explicitZ is a closed-form integer pattern on the same six indices (sample clauses give values such as $4$, $-2$, etc.). The identity asserts that the folded sum is exactly eight times that table entry, pointwise.
The ambient setting is discrete gravity analysis: certifying an algebraic numerator identity that appears in the midpoint Regge calculus expansion in four dimensions, before any continuum or continuum-limit claim.
proof idea
One-line computational proof: by decide. Both sides are closed integer expressions once the six concrete Fin 4 arguments are substituted, so the kernel reduces the equality to true with no lemmas, rewrites, or case splits inside this declaration.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every multi-index by nested fin_cases and invokes these chunk lemmas cellwise; without the cell equalities the universal statement does not close. The module frames the work as chunk 6 of the 256-kernel-decide split of that identity.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact midpoint $M_2$ TT identity in 4D Regge analysis, not a forcing-chain (T0–T8) step. It does not itself touch $\phi$, the eight-tick octave, or the $\alpha$ band; it only clears one integer cell so the assembled numerator identity can be cited downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.