e_310321
plain-language theorem explainer
Pointwise identity: the midpoint numerator m2Num at Fin-4 indices (3,1,0,3,2,1) equals eight times the explicit integer kernel explicitZ at the same indices. Gravity analysts assembling the full 4D Regge midpoint M2TT identity cite this as one of 256 kernel cells. The proof is a single decide on concrete integers.
Claim. For the index sextuple $(a,b,c,d,i,j)=(3,1,0,3,2,1)$ with each index in $\{0,1,2,3\}$, the folded midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-cell kernel certification that the 4D Regge exact-midpoint numerator equals eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$ (labels $0..3$ for discrete directions or simplex legs).
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling entry at the six indices. The explicit kernel $Z$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on the matched patterns).
The local claim is the equality at one concrete sextuple inside that table, not the universal statement.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values (the fold for the numerator versus the pattern match for $Z$, scaled by $8$), and the kernel decides equality of those integers. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall$ six $\mathrm{Fin},4$ indices the same equality and discharges the universal goal by exhaustive fin_cases on each coordinate, invoking one cell theorem per sextuple. This cell is the $(3,1,0,3,2,1)$ branch of that case tree.
In the Recognition gravity stack these kernel identities underwrite the exact midpoint M2TT algebraic identity in 4D Regge calculus, a discrete curvature/mass bookkeeping step on the phi-ladder side of the forcing chain. The chunk exists so the 256 decides stay modular rather than one giant tactic block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.