e_301232
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (3,0,1,2,3,2) equals eight times the explicit integer table value. Gravity analysts cite it as one of the 256 kernel cells that assemble the global m2Num = 8·explicitZ statement. Proof is a single decide on concrete Int arithmetic.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,0,1,2,3,2)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit table entry: $m_2^{\mathrm{num}}(3,0,1,2,3,2)=8\,Z_{\mathrm{expl}}(3,0,1,2,3,2)$.
background
This module is chunk 12 of a 256-cell kernel certifying that the folded numerator of a 4D Regge midpoint mass-squared identity equals eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, i.e. discrete edge/vertex labels in the 4-simplex combinatorics.
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 term at those six indices. The explicit table $Z_{\mathrm{expl}}$ is a pattern-matched $\mathrm{Int}$-valued function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for the listed patterns).
Local goal of the chunk family: discharge every concrete sextuple so the assembly theorem can reassemble the universal equality by exhaustive fin_cases.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed literals, so Lean’s decision procedure evaluates the fold that defines the numerator and the pattern match that defines the explicit table, then checks integer equality. No lemmas are invoked beyond the two definitions.
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}}$ and proves it by six nested fin_cases over $\mathrm{Fin},4$, hitting this cell (among the other 255). That global identity is the algebraic core of the Regge exact midpoint $M_2$ TT identity in 4D gravity analysis inside the monolith.
In the Recognition framework this sits in the gravity sector (discrete curvature / Regge calculus bookkeeping), not in the T0–T8 forcing chain itself. It closes a pure computational obligation: every kernel cell must match so the continuum-facing midpoint identity inherits an exact integer factor of 8 rather than a residual defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.