e_033220
plain-language theorem explainer
Pointwise check that the folded M2 numerator equals eight times the explicit integer coupling Z at multi-index (0,3,3,2,2,0) in the 4D Regge midpoint kernel. Gravity analysts cite it only as one cell of the 256-case cover. The proof is a single kernel decide on concrete Int values.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,2,2,0)$ with each entry in $\{0,1,2,3\}$, the folded midpoint $M_2$ numerator equals $8$ times the explicit integer coupling $Z$ at that multi-index.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator m2Num is the fold of a fixed coupling list: it sums a local contribution at each table entry for the given multi-index. The comparison target explicitZ is a sparse pattern of small integers (values such as $4$, $-2$, and defaults) tabulated by multi-index.
The ambient module is chunk 3 of the identity m2Num = 8 · explicitZ. The full statement ranges over all $4^6 = 4096$ index tuples; this file (and its siblings) discharge a 256-cell block by concrete evaluation rather than by a closed algebraic argument.
Upstream, both sides are pure definitions in the kernel certificate module: no analytic hypotheses, only integer arithmetic on a finite domain.
proof idea
One-line kernel proof: decide evaluates both sides at the fixed six-tuple $(0,3,3,2,2,0)$ and checks integer equality. No lemmas are invoked beyond the definitions of the fold m2Num and the pattern explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple of Fin-4 indices by exhaustive fin_cases and routes each cell to a chunk theorem of this form. Without the pointwise cells, the assembly cannot close.
In the gravity stack this identity is bookkeeping for the exact midpoint $M_2$ tensor structure in 4D Regge calculus: it certifies that the folded numerator is exactly eight copies of the tabulated coupling, so later continuum or continuum-limit arguments may replace one by the other. It does not itself touch the T0–T8 forcing chain, $\phi$, or the eight-tick octave; it is local algebraic hygiene inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.