e_321122
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (3,2,1,1,2,2) equals eight times the explicit integer kernel table at that same index. Gravity analysts assembling the 4D midpoint M2TT identity cite it as one of 256 kernel cases. The proof is a single kernel `decide` on concrete Fin-4 data.
Claim. For indices $(a,b,c,d,i,j)=(3,2,1,1,2,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 14 of a 256-case kernel certification that the folded numerator of a 4D Regge midpoint M2TT identity agrees with an explicit integer table, scaled by eight. Indices run over Fin 4, i.e. the four discrete directions of the 4-simplex edge data.
The numerator m2Num is defined by folding a fixed coupling list: it sums a local contribution at each coupling term for the six indices. The companion explicitZ is a closed pattern-match table Fin 4^6 → ℤ listing the intended integer values (examples in the kernel cert include entries 4, −2, and so on).
The local claim is only the single tuple (3,2,1,1,2,2). Sibling theorems cover the other tuples in the same chunk; the assembly theorem quantifies over all six indices.
proof idea
One-line computational proof: by decide. Lean reduces both sides on the concrete Fin 4 literals. The left side evaluates the fold that defines the numerator; the right side looks up (or defaults in) the explicit kernel table and multiplies by 8. No lemmas are invoked beyond decidable equality on Int.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in (Fin 4)^6 by exhaustive fin_cases and discharge of each pointwise goal. That global equality is the certified bridge between the folded coupling definition and the closed-form kernel used in the Regge exact-midpoint M2TT analysis.
In the Recognition gravity stack this is bookkeeping infrastructure, not a new physical law: it locks the discrete 4D curvature/coupling numerator to an explicit integer table so later continuum or continuum-limit arguments can quote a proved algebraic identity rather than an unchecked expansion. It does not itself invoke the forcing chain (T5–T8), RCL, or the φ-ladder; those enter only if a parent gravity theorem imports this certified kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.