e_312311
plain-language theorem explainer
Pointwise identity: the midpoint Regge mass-squared numerator at Fin-4 indices (3,1,2,3,1,1) equals eight times the explicit Z-coupling table entry. Gravity analysts assembling the 4D TT midpoint kernel cite these 256 chunk lemmas. Proof is a single kernel decide on concrete integer arithmetic.
Claim. For indices $a=3$, $b=1$, $c=2$, $d=3$, $i=1$, $j=1$ in $\mathrm{Fin}\,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 is one chunk of the 4D Regge midpoint TT identity certification: it checks $m_2^{\mathrm{num}}=8\cdot Z$ at a block of kernel index sextuples (256 decides total across chunks).
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of contrib over couplingZList, an integer accumulation of coupling contributions at six $\mathrm{Fin},4$ slots. The comparison table $Z$ is an explicit pattern-matched integer function on the same six indices (sample clauses: $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$, and so on).
The local goal is purely arithmetic: evaluate both sides at one fixed sextuple and confirm equality in $\mathbb{Z}$.
proof idea
One-line computational proof: decide closes the ground equality of two concrete integers obtained by evaluating the fold definition of the numerator and the pattern match for the explicit table at $(3,1,2,3,1,1)$. No lemmas beyond the definitions of the two sides are required.
why it matters
Feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges the quantifiers by exhaustive fin_cases on all six indices. Each chunk lemma such as this one supplies one (or a block of) decided cells so the assembly does not re-run the kernel on every branch from scratch.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint TT mass-squared kernel in 4D Regge analysis: matching the folded coupling sum to eight times a closed-form table is the algebraic certificate that the discrete curvature/mass expression collapses as claimed. It is infrastructure, not a forcing-chain landmark (T0–T8), but it is required before continuum or continuum-limit gravity claims that quote the midpoint kernel can be trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.