e_300030
plain-language theorem explainer
Single kernel point check: the folded coupling numerator at multi-index (3,0,0,0,3,0) equals eight times the closed-form integer kernel Z at that point. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite the full family of such point theorems. Proof is a pure `decide` on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,0,0,0,3,0)$ with each coordinate 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 $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on $(\mathbb{F}_4)^6$ are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each list entry at the six indices. The comparison target is an explicit pattern-matched integer function $Z$ on the same six indices (sample clauses return $4$, $-2$, etc.).
The local module is chunk 12 of a 256-point kernel certification: each point theorem asserts $m_2^{\mathrm{num}}=8Z$ at one concrete sextuple. The ambient claim is the universal identity over all of $(\mathbb{F}_4)^6$, assembled later by exhaustive fin_cases.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values (the fold over the coupling list versus the pattern match for $Z$, scaled by 8), and the decision procedure discharges equality.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathbb{F}_4$, $m_2^{\mathrm{num}}=8Z$, proved by six nested fin_cases that invoke the 256 point lemmas. That universal identity is the algebraic core of the 4D Regge midpoint M2–TT kernel certificate in the Gravity analysis stack. It is bookkeeping infrastructure for the discrete curvature/mass-squared side of the RS gravity bridge, not a forcing-chain (T0–T8) step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.