e_113233
plain-language theorem explainer
For the six-index tuple (1,1,3,2,3,3) on Fin 4, the Regge midpoint m2 numerator equals eight times the corresponding explicit Z table entry. Gravity analysts cite it as one kernel cell in the 4D midpoint identity. The proof is a single decide on the concrete integers.
Claim. For indices $a=b=1$, $c=3$, $d=2$, $i=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 table value $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge exact-midpoint analysis. The local goal is the pointwise identity $m_2^{\mathrm{num}}=8,Z$ on all six-tuples of indices in $\mathbb{F}_4$, proved by splitting the $4^6$ kernel into decide chunks.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: each term contributes an integer depending on the six indices, and the fold starts at $0$. The companion table $Z$ is an explicit pattern-match on those same indices, returning small integers such as $4$, $-2$, and so on for the nonzero patterns.
Chunk 5 is one block of those kernel cells. The present declaration is the single cell with indices $(1,1,3,2,3,3)$.
proof idea
One-line computational proof: decide evaluates both sides on the concrete Fin-4 six-tuple. The left side runs the fold that defines the numerator; the right side looks up the explicit Z clause (or the default zero) and multiplies by eight. No lemmas are invoked beyond the kernel decision procedure.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states the identity for every six-tuple in $\mathbb{F}_4$ and discharges the universal quantifier by exhaustive fin_cases. This cell is one of the concrete equalities that block feeds. In the broader gravity stack it certifies that the midpoint Regge m2 numerator is exactly eight times a sparse integer table, a bookkeeping step toward the 4D TT identity rather than a dynamical law. It does not itself touch the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete kernel hygiene inside the Regge analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.