e_123003
plain-language theorem explainer
Pointwise kernel identity: for the Fin-4 sextuple (1,2,3,0,0,3), the folded numerator m2Num equals eight times the closed-form integer explicitZ. Gravity analysts cite it as one cell of the 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,3,0,0,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(1,2,3,0,0,3)=8\,Z_{\mathrm{expl}}(1,2,3,0,0,3)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on sextuples of $\mathbb{F}4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums a local contribution at each coupling term for the six indices. The companion $Z{\mathrm{expl}}$ is an explicit pattern-matched integer table on the same domain (sample clauses send $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local module is chunk 6 of a 256-way kernel split whose sole job is to discharge $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ at concrete index points by decision procedure. The ambient claim is the exact midpoint M2–TT identity in four dimensions.
proof idea
One-line computational proof: decide evaluates both sides at the fixed sextuple $(1,2,3,0,0,3)$. The left side reduces by unfolding the fold over couplingZList; the right side multiplies the matched explicitZ clause by eight. No lemmas beyond the two definitions are invoked.
why it matters
This cell is consumed by the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathbb{F}_4)^6$ and proves it by exhaustive fin_cases on the six indices. The chunk decomposition keeps each kernel goal inside the decide budget while the assembler rebuilds the full $\forall$-statement.
In the Recognition gravity stack, the exact M2–TT midpoint identity is bookkeeping for the discrete curvature/coupling side of the Regge calculus layer. It does not itself invoke the forcing chain (T5–T8) or the RCL, but it is part of the certified numeric skeleton those continuum limits sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.