e_313113
plain-language theorem explainer
Pointwise identity: the midpoint Regge m₂ numerator at multi-index (3,1,3,1,1,3) equals eight times the explicit kernel value Z at that index. Gravity analysts cite it as one cell of the 256-case kernel table. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,1,1,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel table.
background
This module is chunk 13 of a 256-cell decide table establishing $m_2^{\mathrm{num}}=8\cdot Z$ on every 4D multi-index. The setting is the exact midpoint identity for the Regge/TT sector in four dimensions: the numerator built from coupling contributions is compared to a closed-form integer kernel.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList and summing each contribution at the six Fin 4 slots. The companion $Z$ is an explicit case table Fin 4^6 → ℤ (sample entries: $(0,0,1,1,2,2)\mapsto 4$, mixed pairs $\mapsto -2$, and so on). Both live in the kernel-cert module imported here.
Indices run in $\mathbb{F}_4\simeq{0,1,2,3}$; the six-tuple labels a single matrix/tensor slot of the midpoint operator. Chunking keeps each decide goal tiny and machine-checkable.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the concrete six-tuple $(3,1,3,1,1,3)$—the fold defining the numerator on the left, the pattern-match table for $Z$ on the right—and checks integer equality $m_2^{\mathrm{num}}=8Z$. No lemmas are invoked beyond the decidable equality of Int and the closed definitions of the two sides.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles all 256 pointwise facts by nested fin_cases on the six indices; this declaration is the cell for $(3,1,3,1,1,3)$. That global identity is the algebraic core of the exact midpoint $m_2$/TT relation in the 4D Regge analysis: once numerator equals eight times the explicit kernel everywhere, downstream gravity identities can quote a closed form instead of a fold.
In the Recognition Science gravity stack this is pure certification scaffolding—no new physical constant is fixed here—but it underwrites the discrete curvature/TT bookkeeping that sits beside the forcing chain’s $D=3$ spatial claim and the eight-tick octave when the continuum limit is taken. Closing every chunk removes a sorry-class gap in the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.