e_202032
plain-language theorem explainer
At multi-index (2,0,2,0,3,2) on (Fin 4)^6, the Regge midpoint m2 numerator equals eight times the explicit Z table entry. Gravity analysts cite it as one of 256 kernel point checks that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,\,b{=}0,\,c{=}2,\,d{=}0,\,i{=}3,\,j{=}2$ in $\mathbb{F}_4$, the folded coupling numerator $m_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of a 256-way case split proving that the Regge midpoint $m_2$ numerator coincides with eight times a closed-form integer table on all of $(\mathbb{F}_4)^6$. The local setting is pure integer arithmetic on finite indices: no continuum limit is taken here.
Upstream, m2Num is defined by folding a fixed coupling list and summing a contribution at each tuple $(a,b,c,d,i,j)$. The companion explicitZ is a pattern-matched integer table on the same six Fin 4 arguments (sample values include $4$, $-2$, and so on). The claim is the pointwise equality of those two integers at one concrete multi-index.
The surrounding Gravity.Analysis development uses these identities to certify an exact midpoint TT identity in 4D Regge calculus, with the factor $8$ matching the discrete octave structure that appears elsewhere in the framework.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are fixed, so Lean’s decision procedure discharges the equality with no lemmas or rewriting. Sibling chunk theorems follow the same pattern for the other multi-indices.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2=8,Z$ and proves it by exhaustive fin_cases over all six indices, invoking one chunk equality per cell. Without the full set of 256 decides, the global identity does not close.
In the Recognition gravity stack this is scaffolding for an exact discrete TT/midpoint identity in 4D Regge calculus, not a continuum Einstein equation. The factor $8$ is consistent with the eight-tick octave (T7) bookkeeping that organizes discrete time in the forcing chain, though this lemma itself is only an integer table check. It closes one cell of the kernel certificate imported from ReggeExactMidpointM2TTIdentity4DKernelCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.