e_112112
plain-language theorem explainer
One of 256 kernel cases: the midpoint mass-squared numerator at discrete indices (1,1,2,1,1,2) equals eight times the explicit integer Z-coupling at those same indices. Gravity analysts assembling the full 4D Regge midpoint identity cite it as a discharged case. The proof is a single kernel decide on concrete Fin 4 values.
Claim. For indices $a=1$, $b=1$, $c=2$, $d=1$, $i=1$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge midpoint analysis for the mass-squared TT identity. The local goal, stated in the module header, is to show $m_2^{\mathrm{num}} = 8\cdot Z$ by exhausting a 256-case kernel on $\mathrm{Fin},4^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums a contribution function over that list at the six discrete indices. The explicit kernel $Z$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern of integer values (for example $4$, $-2$, and related entries on selected index patterns).
Chunk 5 is one block of those decides. Each sibling theorem pins one concrete sextuple; together they feed the universal statement.
proof idea
One-line computational proof: decide evaluates both sides at the concrete $\mathrm{Fin},4$ sextuple $(1,1,2,1,1,2)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of the folded numerator and the explicit kernel table.
why it matters
The parent theorem is the assembled identity: for all $a,b,c,d,i,j:\mathrm{Fin},4$, the numerator equals eight times the explicit kernel. That proof introduces the six indices and runs nested fin_cases, so each leaf such as this one must already hold.
In the gravity track this identity is bookkeeping for the exact midpoint mass-squared TT structure in 4D Regge-type analysis. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is a discrete algebraic certificate inside the gravity analysis layer that those continuum claims later rely on for clean numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.