e_100323
plain-language theorem explainer
Pointwise kernel check: the Regge midpoint numerator at multi-index (1,0,0,3,2,3) equals eight times the explicit integer table value at that index. Gravity analysts cite it only as one cell of the 4^6 case split that assembles the global identity. The proof is a single native decide on concrete integers.
Claim. For indices $a{=}1,b{=}0,c{=}0,d{=}3,i{=}2,j{=}3$ in $\mathbb{F}_4$, the folded coupling 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 4 of a brute-force certification that the 4D Regge midpoint $m_2$ numerator agrees with an explicit closed-form integer table. Indices run over $\mathrm{Fin},4$ (four discrete directions), so there are $4^6$ cells; each chunk discharges a block of them by kernel decide.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums a local contribution at each coupling triple for the six indices. The comparison target $Z$ is an explicit pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and so on for the listed patterns).
The local claim is only the equality at one concrete multi-index. Upstream, both sides are pure definitions in the kernel certificate module; no analytic lemma is required beyond evaluating those definitions.
proof idea
One-line computational proof: decide. Lean reduces both sides of
$m_2^{\mathrm{num}}(1,0,0,3,2,3)=8\cdot Z(1,0,0,3,2,3)$
to concrete integers (fold of the coupling list versus the pattern match on $Z$) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the two sides.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all six $\mathrm{Fin},4$ indices. That parent introduces the six variables and splits by fin_cases on each; each leaf is one of these chunk theorems (here the cell $(1,0,0,3,2,3)$).
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge $m_2$ tensor structure in 4D, not a new dynamical law. It does not itself touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder mass formula; it only certifies a discrete algebraic identity used downstream in the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.