e_120331
plain-language theorem explainer
For the six-index tuple (1,2,0,3,3,1) in (Fin 4)^6, the folded Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact 4D midpoint TT identity cite this as one atomic case among the chunked kernel decides. The proof is a single kernel decision (by decide) on concrete integer arithmetic.
Claim. For indices $a=1,b=2,c=0,d=3,i=3,j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel: $m_2^{\mathrm{num}}(1,2,0,3,3,1)=8\,Z_{\mathrm{exp}}(1,2,0,3,3,1)$.
background
This module sits in the Gravity analysis layer that certifies an exact midpoint TT identity for 4D Regge calculus. The local setting (module doc) is the sixth chunk of the statement $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{exp}}$, discharged by 256 kernel decisions on concrete multi-indices.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the six Fin-4 slots. The comparison value $Z_{\mathrm{exp}}$ is an explicit integer-valued kernel on $(\mathrm{Fin},4)^6$, given by a large pattern-match (sample clauses send $(0,0,1,1,2,2)$ to 4 and $(0,0,1,2,1,2)$ to $-2$).
Both definitions live in the KernelCert import; the present file only evaluates one fixed six-tuple.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the equality on the concrete Fin-4 literals to integers (the fold for the numerator, the match for the explicit kernel) and checks that the integers coincide. No lemmas are invoked beyond the decidable equality of Int.
why it matters
The parent theorem is m2Num_eq_eight_explicitZ in the Assemble module, which asserts the identity for every six-tuple in $(\mathrm{Fin},4)^6$. Its proof introduces the six indices and runs fin_cases on each; the resulting atomic goals are closed by chunk theorems such as this one.
In the Recognition gravity stack, the exact midpoint TT identity is infrastructure for discrete curvature bookkeeping on the eight-tick, $D=3$ lattice forced by the T0–T8 chain. Establishing $m_2^{\mathrm{num}}=8,Z_{\mathrm{exp}}$ case-by-case removes a residual algebraic gap between the folded coupling definition and the closed kernel used downstream. This declaration is pure scaffolding closure for one multi-index; it does not itself touch continuum limits or phenomenological mass formulae.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.