e_233121
plain-language theorem explainer
For the six Fin-4 indices (2,3,3,1,2,1), the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 256-way kernel certification that m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}3$, $c{=}3$, $d{=}1$, $i{=}2$, $j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the tabulated explicit kernel integer at those indices: $\mathrm{m2Num}(2,3,3,1,2,1)=8\cdot\mathrm{explicitZ}(2,3,3,1,2,1)$.
background
In the Regge exact-midpoint 4D analysis, the numerator m2Num is defined by folding a fixed coupling list: it sums contrib t a b c d i j over every term t in couplingZList, yielding an integer for each six-tuple of Fin 4 indices. The companion table explicitZ is a pattern-matched integer kernel on the same six indices (e.g. returning 4, −2, etc. on selected patterns).
This module is chunk 11 of the 256 kernel decides that certify the pointwise identity m2Num = 8 · explicitZ. The local setting is pure finite enumeration: every index lives in Fin 4, so the equality is a concrete integer identity once the fold and the table are expanded.
Upstream, only the two definitions are needed; no analytic lemma is invoked. Downstream assembly will reassemble all 256 cases into a single universal statement.
proof idea
One-line kernel proof: by decide. Lean reduces both sides on the concrete indices (2,3,3,1,2,1)—the fold that defines the numerator and the pattern match that defines the explicit kernel—and checks integer equality. No lemmas beyond the two definitions are applied.
why it matters
This declaration is one of the 256 atomic cases consumed by m2Num_eq_eight_explicitZ in the assemble module, which states
∀ (a b c d i j : Fin 4), m2Num a b c d i j = 8 * explicitZ a b c d i j
and discharges the quantifiers by fin_cases on each coordinate, routing each branch to a chunk theorem of this form.
In the broader Gravity/Regge midpoint pipeline, the factor-of-eight identity converts the folded coupling numerator into the closed explicit kernel, which is the algebraic backbone for the exact midpoint mass-squared identities in 4D. It does not itself touch the Recognition forcing chain (T0–T8) or the J-cost; it is infrastructure inside the discrete gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.