e_310221
plain-language theorem explainer
For the six-index tuple (3,1,0,2,2,1) on Fin 4, the folded coupling numerator equals eight times the explicit closed-form integer Z. Analysts assembling the exact four-dimensional midpoint M2 TT identity cite this atomic cell check. The proof is a single native decide on the two concrete integers.
Claim. At multi-index $(3,1,0,2,2,1)$, the folded coupling numerator equals eight times the explicit integer table value: $m_2^{\mathrm{num}}(3,1,0,2,2,1)=8\,Z_{\mathrm{exp}}(3,1,0,2,2,1)$.
background
In the four-dimensional Regge midpoint analysis, the M2 TT identity is certified by matching a folded coupling numerator against an explicit integer table Z on $(Fin 4)^6$. The numerator is the fold of a contribution map over a fixed coupling list, yielding one integer per six-tuple. The explicit table assigns a small integer (for example $4$ or $-2$) by pattern match on the six indices.
This module is chunk 13 of a 256-cell kernel partition. Each cell discharges one concrete equality numerator $= 8\cdot Z$ by decision procedure. The local setting is pure finite enumeration: no continuum limit and no physical units enter the chunk.
Upstream definitions live in the kernel certificate module: the fold that builds the numerator, and the pattern-matched explicit Z table.
proof idea
One-line native decision. Both sides are closed integer terms at the concrete $Fin 4$ values $3,1,0,2,2,1$: the left-hand side evaluates the coupling-list fold; the right-hand side evaluates the pattern match for explicit Z and multiplies by eight. decide checks the resulting integer equality. No intermediate lemmas are applied.
why it matters
The assembly theorem states numerator $= 8\cdot Z$ for every six-tuple in $(Fin 4)^6$ and proves it by exhaustive fin_cases, each case landing on one chunk cell such as this one. This declaration is the witness for the single multi-index $(3,1,0,2,2,1)$.
Inside the Recognition Science gravity stack, the exact midpoint M2 TT identity is discrete curvature bookkeeping on the Regge side. Filling every kernel cell removes scaffolding from that identity. The result stays combinatorial: it does not invoke the forcing chain T0-T8, the Recognition Composition Law, or the phi ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.