e_022320
plain-language theorem explainer
For the six-index tuple (0,2,2,3,2,0) in (Fin 4)^6, the folded Regge numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite this as one cell of the 4D midpoint M2TT identity table. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,3,2,0)$ with each index in $\mathbb{F}_4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,2,2,3,2,0)=8\,Z_{\mathrm{ex}}(0,2,2,3,2,0)$.
background
This module is chunk 2 of a 256-cell kernel certification that the 4D Regge midpoint numerator equals eight times an explicit integer kernel. Indices run over $\mathrm{Fin},4$, labeling discrete edge/face slots in the midpoint triangulation scheme.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the six indices. The comparison target $Z_{\mathrm{ex}}$ is a closed-form integer table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on matched patterns).
Local goal of the chunk: discharge one concrete equality $m_2^{\mathrm{num}}=8Z_{\mathrm{ex}}$ so the assembler can recombine all cells by exhaustive fin_cases.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values (the fold for the numerator versus the pattern match for the explicit kernel, then multiply by 8), and Lean’s decision procedure checks equality on those integers. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by nested fin_cases and per-cell decides such as this one. That global equality is the certified algebraic core of the Regge exact-midpoint M2TT identity in 4D gravity analysis inside the monolith.
In the Recognition Science gravity stack this is bookkeeping, not a new physical law: it locks the discrete curvature/coupling numerator to the explicit kernel used downstream in continuum or continuum-limit comparisons. It does not itself invoke the forcing chain (T5–T8), RCL, or $\varphi$-ladder mass formulae; those sit at a higher layer once the Regge identity is trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.