e_011020
plain-language theorem explainer
Kernel-checked equality: the midpoint Regge mass-squared numerator at index sextuple (0,1,1,0,2,0) equals eight times the explicit integer coupling Z at those same indices. Gravity analysts assembling the full 4D midpoint identity cite this as one cell of the 256-case grid. Proof is a single native decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,1,0,2,0)$ with each index in $\{0,1,2,3\}$, 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 midpoint analysis for the mass-squared TT identity. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term evaluated at the six $\mathrm{Fin},4$ indices. The comparison object is an explicit integer table $Z$ on $(\mathrm{Fin},4)^6$, hard-coded on the sparse support that appears in the kernel (e.g. $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and analogous signed entries).
The local claim of the file is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on a 256-cell chunk of the index grid. Each cell is a separate decide theorem; the present declaration is the cell with indices $(0,1,1,0,2,0)$.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six indices are substituted into the fold definition of the numerator and the pattern-match table for $Z$, so the kernel closes the equality with no lemmas beyond evaluation.
why it matters
Feeds the 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$ by exhaustive fin_cases on the six indices. That quantified identity is the algebraic backbone of the exact midpoint $M_2$ TT check in 4D Regge gravity inside the Recognition stack: it certifies that the folded coupling numerator is exactly eight copies of the sparse explicit $Z$ table, with no residual terms on any cell.
Within the broader RS gravity program this is bookkeeping, not a forcing-chain step (T0–T8), but it is required scaffolding for any later claim that the discrete midpoint curvature/mass-squared sector matches the continuum TT projection at the certified coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.