m2Num
plain-language theorem explainer
Integer numerator of the 4D midpoint m² TT kernel coefficient at six Fin-4 index slots, formed by summing scaled integer contributions over the full coupling table. Gravity analysts cite it to move rational m² coefficients onto decidable Int arithmetic (kernel decide, no native_decide). The body is a single foldl of contrib over couplingZList from 0.
Claim. For indices $a,b,c,d,i,j\in\{0,1,2,3\}$, the integer $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the sum, over every entry $t$ of the assembled 4D midpoint coupling table, of the scaled integer contribution of $t$ at those indices.
background
This module holds generated kernel certificates for the midpoint $m^2$ transverse-traceless identity in 4D Regge analysis. The script builds Int List.foldl tables at scale 32 so that kernel goals close by decide alone.
Each coupling is a CZ record (integer numerator/denominator plus discrete edge data). The per-coupling contribution multiplies signed edge factors De, Dep, D2 by a scaled numerator term (-c.num)*(16/c.den). The full table couplingZList is the concatenation of sixteen precomputed chunks.
m2Num is the pure integer accumulation of those contributions at a fixed six-index slot. Downstream glue theorems relate the rational $m^2$ coefficient to this integer divided by 256.
proof idea
Definition, not a proof. It is the fold
couplingZList.foldl (fun acc t => acc + contrib t a b c d i j) 0.
No lemmas are applied at the definition site; equality to a list-map sum is recovered later by induction on the list in the glue layer.
why it matters
Central bridge object for the midpoint $m^2$ TT kernel in 4D Regge gravity. Parent results include m2Coeff_eq_m2Num_div (array/Finset $m^2$ coefficient equals the Int fold over 256) and m2CoeffSum_eq_m2Num_div (Finset sum equals the bridged Int fold over 256). Assembly theorems such as m2Num_eq_eight_explicitZ and the per-index e_****** certificates reduce the fold to an explicit closed form by decide.
In the Recognition gravity stack this supplies the certified discrete kernel data behind the midpoint TT identity, keeping the certificate path inside pure Int arithmetic rather than floating or native evaluation. It is scaffolding for the larger Regge exact-identity chain, not a continuum GR claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.