e_200113
plain-language theorem explainer
For the six-index slot (2,0,0,1,1,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a{=}2,b{=}0,c{=}0,d{=}1,i{=}1,j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(2,0,0,1,1,3)=8\,Z(2,0,0,1,1,3)$.
background
In the Regge exact-midpoint 4D analysis, the numerator m2Num is the fold of a fixed coupling list: each term contributes an integer contrib at six Fin-4 indices, and the fold starts from 0. The companion explicitZ is a sparse closed-form table on those same six indices (nonzero only on a short list of patterns such as (0,0,1,1,2,2) ↦ 4 and various sign-flipped pairs ↦ −2).
The module is chunk 8 of a 256-way kernel decide: the claim is the pointwise identity numerator = 8 · explicit table, specialized to one concrete six-tuple. The ambient goal is the TT midpoint identity in 4D Regge calculus, reduced to integer arithmetic on Fin 4.
proof idea
One-line decide. Both sides evaluate to concrete Int values once the six Fin-4 arguments are fixed: the left side runs the fold of couplingZList through contrib, the right side looks up (or defaults) explicitZ and multiplies by 8. Lean’s kernel decision procedure discharges the resulting integer equality with no lemmas or case splits in this chunk.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 indices by nested fin_cases and invokes each chunk theorem such as this one. That global equality is the certified bridge from the folded coupling definition to the sparse explicit kernel used in the Regge midpoint M2/TT identity work.
In the broader Recognition gravity stack this is pure discrete bookkeeping: it does not itself invoke the forcing chain (T0–T8), the J-cost, or the phi ladder, but it hardens the 4D combinatorial kernel those continuum claims sit on. Closing all 256 chunks removes scaffolding from the midpoint identity path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.