e_112110
plain-language theorem explainer
Pointwise identity: the Regge midpoint $m_2$ numerator at multi-index $(1,1,2,1,1,0)$ equals eight times the explicit $Z$ table entry there. Gravity analysts cite it when assembling the full 4D kernel identity $m_2=8Z$ over $(\mathbb{F}_4)^6$. Proof is a single kernel `decide` on concrete integers.
Claim. For indices $a=1,b=1,c=2,d=1,i=1,j=0$ in $\mathbb{F}_4$, the folded coupling numerator $m_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 5 of a 256-case kernel certification that the midpoint Regge $m_2$ numerator coincides with eight times a closed-form integer table on every sextuple of indices in $\mathbb{F}_4$.
The numerator $m_2$ is defined by folding a fixed coupling list: start at $0$ and add each contribution contrib evaluated at the six indices. The comparison target explicitZ is a pattern-matched integer table on $(\mathrm{Fin},4)^6$ (sample entries include $4$, $-2$, and so on for distinguished index patterns).
Local setting is pure integer arithmetic on a finite discrete index set; no continuum limit or physical units enter these chunk lemmas.
proof idea
One-line proof: by decide. Lean evaluates both sides as concrete Int values (the fold that defines the numerator versus eight times the table lookup) and discharges equality by computation. No lemmas are invoked beyond the definitions of the numerator and the explicit table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2=8Z$ and proves it by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments, routing each concrete sextuple to a chunk identity of this form.
In the gravity analysis stack this closes the algebraic identity between the summed coupling numerator and the explicit $Z$ kernel used in the 4D Regge midpoint $TT$ identity. It is bookkeeping, not a new physical law: once every chunk holds, the global equality is unconditional on the finite index set.
No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is directly at stake; the lemma is infrastructure inside the discrete gravity kernel certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.