e_133113
plain-language theorem explainer
For the six-index tuple (1,3,3,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 atomic cell in the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}1,b{=}3,c{=}3,d{=}1,i{=}1,j{=}3$ in $\mathrm{Fin}\,4$, the integer $m_2$ numerator obtained by folding coupling contributions equals $8$ times the explicit kernel value $Z$ at those indices.
background
This module is chunk 7 of a 256-cell kernel certification that the Regge-exact midpoint $M_2$ numerator in 4D equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, matching discrete 4-simplex edge/face labels in the Regge calculus setting.
The numerator $m_2\mathrm{Num}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at those six indices. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (typical nonzero entries are $\pm 2,,4$).
The local claim is one concrete six-tuple instance of the global identity $m_2\mathrm{Num}=8\cdot Z$, discharged by computation rather than by a symbolic expansion of the fold.
proof idea
One-line proof by decide. Both sides are closed integer expressions once the six concrete $\mathrm{Fin},4$ values are substituted: the left side evaluates the fold of contrib over couplingZList; the right side is $8$ times the matching clause of explicitZ. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases and dispatches each cell to a chunk theorem of this form. Without the cell-wise equalities, the global midpoint $M_2$ numerator identity in the 4D Regge analysis does not close.
In the Recognition gravity stack this is bookkeeping infrastructure for discrete curvature/mass-side numerics, not a forcing-chain landmark (T5–T8). It certifies that the folded coupling definition agrees with the sparse closed form used downstream, so later continuum or continuum-limit arguments can quote $8Z$ instead of re-folding the list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.