e_313303
plain-language theorem explainer
For the six-index slot (3,1,3,3,0,3) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic decide cell in the 4D Regge midpoint M2=TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=3$, $b=1$, $c=3$, $d=3$, $i=0$, $j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $N$ (Lean m2Num) is the fold of a fixed coupling list: it sums a local contribution at each coupling triple. The companion map $Z$ (Lean explicitZ) is a closed-form case table of small integers (entries such as $4$, $-2$, and so on) that is meant to be the exact kernel of the same midpoint identity.
The module is chunk 13 of a 256-cell decide grid that discharges $N=8Z$ pointwise. The global statement is the universal quantification over all six indices; each chunk theorem pins one concrete sextuple so the assembler can finish by exhaustive fin_cases.
Upstream, $N$ is defined by folding couplingZList with contrib, while $Z$ is the pattern-matched explicit table. No continuum limit or curvature hypothesis enters: the claim is pure finite arithmetic on $\mathrm{Fin},4$.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides at the concrete sextuple $(3,1,3,3,0,3)$, reduces the fold that defines the numerator and the case table that defines the explicit kernel to integers, and checks equality with $8Z$. No lemmas are invoked beyond decidable integer arithmetic.
why it matters
This cell feeds m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j,, N=8Z$ and proves it by six nested fin_cases over $\mathrm{Fin},4$, each branch landing on a chunk equality such as this one. That universal identity is the algebraic core of the Regge exact midpoint $M_2$–$TT$ certificate in four dimensions: it shows the folded midpoint numerator is exactly eight times the explicit kernel, so the discrete gravity identity holds on the entire finite index set.
Within Recognition Science gravity work, the certificate sits in the discrete geometric layer that supports continuum limits and effective Newtonian/relativistic readings. It does not itself invoke the forcing chain (T5–T8), $\varphi$, or the eight-tick octave; those enter only when the certified kernel is wired into broader RS mass or coupling claims. The open obligation this closes is purely combinatorial: one of the 256 decide cells needed before the assembler theorem is sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.