e_020333
plain-language theorem explainer
Pointwise kernel identity: the Regge midpoint numerator at multi-index (0,2,0,3,3,3) equals eight times the explicit integer table at that same index. Gravity analysts cite it when assembling the global m2Num = 8·explicitZ certificate over (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,2,0,3,3,3)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(0,2,0,3,3,3)=8\,Z_{\mathrm{expl}}(0,2,0,3,3,3)$.
background
This module is chunk 2 of a 256-way kernel split certifying $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on all of $(\mathrm{Fin},4)^6$. The setting is the 4D Regge exact-midpoint TT identity analysis in the Gravity stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it sums contribution terms contrib t a b c d i j over couplingZList, yielding an integer. The comparison object $Z_{\mathrm{expl}}$ is an explicit pattern-matched integer table on six $\mathrm{Fin},4$ indices (sample clauses include values $4$, $-2$, and so on for distinguished index patterns).
The local claim is one concrete cell of that table equality. Upstream, both sides are pure defs in the KernelCert module; no analytic hypotheses are carried.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six indices are fixed numerals in Fin 4: the fold defining the numerator evaluates fully, and the explicit table matches on that pattern (or falls through to its default). The kernel discharges the resulting integer equality with no lemmas and no case split beyond what decide performs internally.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and is proved by exhaustive fin_cases over the six indices. Each chunk such as this one pins a single cell so the global identity can be certified without a monolithic decide.
In the Recognition gravity pipeline this identity is bookkeeping for the Regge midpoint / TT sector in 4D: it replaces a summed coupling expression by a sparse explicit integer table, which later supports exact algebraic identities rather than floating-point checks. It does not itself invoke the forcing chain (T0–T8), RCL, or the $\varphi$-ladder; it is infrastructure inside the discrete gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.