e_213133
plain-language theorem explainer
For the fixed multi-index (2,1,3,1,3,3) on Fin 4, the summed Regge coupling numerator equals eight times the explicit integer kernel value. Gravity analysts cite this as one atomic cell in the 4D midpoint M2–TT identity. The proof is a pure kernel decision: both sides evaluate to the same integer.
Claim. For indices $a{=}2,\,b{=}1,\,c{=}3,\,d{=}1,\,i{=}3,\,j{=}3$ in $\{0,1,2,3\}$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $N$ is defined by folding a fixed coupling list: each term contributes an integer depending on the six indices, and the fold starts at zero. The explicit kernel $Z$ is a closed case table on the same six indices, returning small integers such as $4$, $-2$, and so on.
The local module is chunk 9 of a 256-cell partition of the full index space. Each cell asserts $N=8Z$ at one concrete sextuple. The parent assembly theorem then recombines all cells by exhaustive fin_cases on every coordinate.
Upstream, $Z$ and $N$ live in the kernel certificate module; this chunk only evaluates them at one point.
proof idea
One-line computational proof: decide evaluates both the folded numerator and $8$ times the explicit table entry at the concrete indices $(2,1,3,1,3,3)$ and checks integer equality. No lemmas are invoked beyond the definitions of the two kernels; the kernel closes the goal.
why it matters
This cell is consumed by m2Num_eq_eight_explicitZ, which states $\forall$ six Fin-4 indices, $N=8Z$. That universal identity is the algebraic core of the Regge exact midpoint M2–TT certificate in four dimensions: it converts a summed coupling expression into an explicit sparse integer table, making subsequent curvature and deficit identities purely combinatorial.
Within Recognition gravity, such exact midpoint identities constrain discrete curvature bookkeeping before continuum limits or phenomenological fits. The chunking into 256 decide goals is an engineering partition of the same identity, not a new physical claim. No forcing-chain landmark (T5–T8) is touched directly; the result is infrastructure for the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.