e_032302
plain-language theorem explainer
Pointwise identity: the Regge midpoint m2 numerator at multi-index (0,3,2,3,0,2) equals eight times the explicit integer kernel Z at those indices. Gravity analysts cite it only as one cell of the 4D kernel table. The proof is a single kernel decide on concrete Int values.
Claim. For indices $(a,b,c,d,i,j)=(0,3,2,3,0,2)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 3 of a 256-way split of the 4D Regge midpoint identity $m_2^{\mathrm{num}}=8\cdot Z$. Each chunk discharges a block of concrete multi-indices by kernel decision.
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 $\mathbb{F}_4$ indices. The explicit table $Z$ is a pattern-matched integer function on the same six indices (sample clauses give values such as $4$, $-2$, and so on).
The local goal is only the single equality at $(0,3,2,3,0,2)$, not the universal statement.
proof idea
One-line computational proof: decide evaluates both sides as concrete integers (the fold that defines the numerator versus eight times the matched table entry) and closes the propositional equality. No lemmas are invoked beyond the definitions of the numerator and the explicit table.
why it matters
Feeds the assemble theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six $\mathbb{F}_4$ arguments. Each chunk theorem such as this one is the discharged cell for one case branch. In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge kernel in 4D, not a new physical law; it certifies that the folded coupling form agrees with the closed-form integer table used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.