e_102333
plain-language theorem explainer
Pointwise identity: the Regge midpoint $m^2$ numerator at Fin-4 indices $(1,0,2,3,3,3)$ equals eight times the explicit $Z$ table entry there. Gravity analysts cite it as one cell of the 256-kernel certification that $m_2^{\mathrm{num}}=8Z$. The proof is a pure `decide` on concrete integers.
Claim. For indices $a=1$, $b=0$, $c=2$, $d=3$, $i=3$, $j=3$ in $\mathbb{F}_4$, the midpoint mass-squared numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
This module is chunk 4 of a 256-case kernel certification that the Regge exact-midpoint mass-squared numerator coincides with eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$ (four discrete directions in the 4D simplex bookkeeping).
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at the six indices. The comparison target $\mathrm{explicit}Z$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample entries include $4$, $-2$, and so on).
The local theoretical setting is purely algebraic and finite: no continuum limit, no floating-point geometry. Each chunk theorem pins one concrete sextuple so the global assembly can discharge the universal quantifier by exhaustive fin_cases.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values once the six indices are substituted into the fold definition of the numerator and the pattern match for the explicit $Z$ table; Lean’s decision procedure checks integer equality. No lemmas beyond the two kernel definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by nested fin_cases over all six $\mathrm{Fin},4$ arguments, dispatching each leaf to a chunk identity of this form.
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint Regge analysis in 4D: it certifies that the discrete numerator used in mass-squared identities is exactly eight copies of the explicit coupling table, so later continuum or continuum-limit arguments can quote a single closed form rather than a fold. It does not itself touch the forcing chain (T0–T8), $\phi$, or the eight-tick octave; it is a finite combinatorial certificate inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.