e_000311
plain-language theorem explainer
For the six-index slot (0,0,0,3,1,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts certifying the 4D Regge exact-midpoint M2TT identity cite this as one atomic kernel check. The proof is a single decide on two concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,0,0,3,1,1)=8\,Z_{\mathrm{ex}}(0,0,0,3,1,1)$, where $Z_{\mathrm{ex}}$ is the explicit integer kernel and $m_2^{\mathrm{num}}$ is the fold of coupling contributions over the fixed coupling list.
background
The module certifies, index-by-index, that the 4D Regge exact-midpoint M2TT numerator equals eight times an explicit integer kernel. Local setting (module doc): "m2Num = 8·explicitZ, chunk 0 (256 kernel decides)."
m2Num a b c d i j is defined as the fold of contrib t a b c d i j over couplingZList, starting from 0; it is an integer built from discrete coupling data. explicitZ is a pattern-matched closed form Fin 4^6 → ℤ that returns small integers (e.g. 4, −2) on selected multi-indices and (implicitly) the default elsewhere.
Both live in the KernelCert module. The present declaration fixes one concrete six-tuple in chunk 0 of the 4^6 enumeration.
proof idea
One-line kernel proof: by decide. Lean reduces both sides at the concrete indices (0,0,0,3,1,1) to integers and checks equality by computation. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states ∀ a b c d i j, m2Num a b c d i j = 8 * explicitZ a b c d i j and discharges the universal claim by exhaustive fin_cases on all six Fin 4 arguments. This chunk is one of the 256 decide-facts in chunk 0 that underwrite that identity.
In the Recognition gravity stack, the exact midpoint M2TT identity is part of the discrete curvature/Regge analysis supporting the continuum limit. It does not itself invoke the T0–T8 forcing chain, φ-ladder masses, or the RCL; it is infrastructure for the 4D geometric side of the program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.