e_113231
plain-language theorem explainer
One of 256 concrete kernel cases: the midpoint Regge mass-squared numerator at multi-index (1,1,3,2,3,1) equals eight times the explicit integer coupling Z at that same tuple. The assembly theorem that states the identity for every Fin-4 sextuple cites these chunks. Proof is a single kernel decide on fully evaluated integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(1,1,3,2,3,1)$ with each entry in $\mathbb{F}_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 is chunk 5 of a 256-case kernel certification that the midpoint Regge $m_2$ numerator coincides with eight times an explicit integer table $Z$ on all sextuples in $(\mathbb{F}_4)^6$. The setting is 4D discrete gravity analysis: couplings are summed over a fixed list and compared against a closed-form pattern.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a contribution function over couplingZList, starting from 0. The comparison target explicitZ is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a finite pattern of integer values (e.g. $4$, $-2$, and related entries on distinguished index patterns). Both live in the kernel-cert module imported here.
The local claim is only the single evaluated equality at indices $(1,1,3,2,3,1)$; sibling theorems cover the other concrete sextuples in the same chunk style.
proof idea
One-line computational proof: decide. After substituting the concrete Fin-4 arguments, both sides reduce to closed integers (the fold for the numerator versus the pattern match for explicit $Z$), and the kernel decision procedure checks equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the universal quantifier by exhaustive fin_cases on each coordinate, routing each leaf to a chunk equality such as this one.
In the gravity analysis stack this identity is the algebraic backbone of the exact midpoint $M_2$–TT relation in 4D Regge calculus: once numerator and explicit kernel match everywhere, downstream curvature and mass-squared identities can quote a single closed form rather than a fold. It is bookkeeping inside the discrete-gravity certification, not a forcing-chain (T0–T8) step, but it hardens the 4D Regge side of the RS gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.