e_033302
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (0,3,3,3,0,2) equals eight times the explicit integer table at that same index. Gravity analysts cite it when assembling the global 4D midpoint M2–TT numerator identity. The proof is a single kernel `decide` on concrete `Int` values.
Claim. For the multi-index $(0,3,3,3,0,2)\in(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(0,3,3,3,0,2)=8\,Z_{\mathrm{expl}}(0,3,3,3,0,2)$.
background
This module is chunk 3 of a 256-case kernel certification that the 4D Regge exact-midpoint M2–TT numerator matches an explicit integer table. Indices run over $\mathbb{F}_4$ (four discrete labels), six of them: four simplex/edge slots and two free tensor indices.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ 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 $Z_{\mathrm{expl}}$ is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by an exhaustive pattern table (sample entries include $4$, $-2$, and so on).
Local goal of the chunk: discharge one concrete sextuple so the assembler can conclude $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ for every index.
proof idea
One-line kernel proof: decide. Both sides reduce to closed Int expressions once the six Fin 4 arguments are literals. Lean evaluates the fold that defines the numerator and the matching clause of the explicit table, then checks integer equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is one leaf of that case tree (256 kernel decides total).
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge calculus in four dimensions: it certifies that the discrete M2–TT numerator is exactly eight times a sparse explicit integer kernel, so later continuum or continuum-limit arguments can quote a closed form rather than a fold. It does not itself invoke the forcing chain (T0–T8), $\phi$, or the eight-tick octave; those enter only at higher layers that consume the assembled identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.