e_320332
plain-language theorem explainer
Pointwise identity: the folded M2 numerator at multi-index (3,2,0,3,3,2) equals eight times the explicit Z-table entry there. Gravity analysts cite it as one cell of the 256-case kernel that certifies the Regge midpoint M2–TT numerator identity in 4D. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,0,3,3,2)$ in $(\mathbb{F}_4)^6$, 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 14 of a 256-case kernel certifying $m_2^{\mathrm{num}}=8\cdot Z$ for the Regge exact-midpoint M2–TT identity in four dimensions. Indices run over $\mathbb{F}_4$ (four discrete labels), matching the 4D simplex/edge bookkeeping of the discrete gravity kernel.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contribution of each coupling term at the six indices. The comparison object $Z$ is an explicit integer-valued table on $(\mathbb{F}_4)^6$, hard-coded by cases (typical nonzero values $\pm 2,,4$).
The parent assembly theorem states the identity for every index tuple by exhaustive fin_cases. Each chunk theorem such as this one discharges one concrete cell so the assembly step is pure case split, not arithmetic.
proof idea
One-line proof: decide. Both sides are closed integer expressions once the six Fin 4 arguments are literals. Lean reduces the fold that defines the numerator and the matching clause of the explicit $Z$ table, then checks equality of the resulting integers in the kernel. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by six nested fin_cases over $\mathbb{F}_4$. That global identity is the algebraic backbone of the Regge exact-midpoint M2–TT certification in the Gravity analysis stack: it replaces a symbolic fold by a sparse explicit table, enabling later exact midpoint and continuum-limit arguments.
Within Recognition Science gravity work, this is bookkeeping infrastructure rather than a forcing-chain landmark (not T5–T8). It closes one of the 256 decide cells so the numerator identity is machine-checked with no sorry. Downstream consumers can quote the universal statement instead of re-deriving the fold at each index.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.