e_001023
plain-language theorem explainer
Pointwise identity: the Regge midpoint numerator coupling at multi-index (0,0,1,0,2,3) equals eight times the explicit kernel value Z at the same index. Gravity analysts cite it as one cell of the 256-case kernel that builds the global m2Num = 8·explicitZ theorem. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,0,1,0,2,3)$ in $\mathrm{Fin}\,4$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 0 of a 256-case kernel certifying that the Regge-exact midpoint numerator coupling equals eight times an explicit integer table in 4D. The ambient setting is the discrete TT (transverse-traceless) identity for the midpoint Regge calculus mass-squared numerator.
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 Int. The comparison target explicitZ is a total function on six Fin 4 indices with a finite case table of small integers (entries such as $4$, $-2$, and the default $0$).
Chunk theorems fix one concrete six-tuple and assert equality after multiplying the table value by eight. Downstream assembly runs fin_cases over all six indices and dispatches to these cells.
proof idea
One-line closed proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals, so the kernel evaluates the fold that defines the numerator and the case table that defines the explicit kernel, then checks $n = 8z$ by computation. No lemmas are invoked beyond decidable equality on Int.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases on each Fin 4 argument. Each chunk cell such as this one discharges one branch of that case split.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge TT sector in $D=4$ (spatial $D=3$ plus time), not a new dynamical law. It locks the discrete numerator against the closed-form kernel so later mass and continuum-limit arguments can quote a single clean equality rather than an opaque fold. It does not itself touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder; it is infrastructure under the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.