Pith. sign in
theorem

e_320102

proved
show as:
module
IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk14
domain
Gravity
line
35 · github
papers citing
none yet

plain-language theorem explainer

At multi-index (3,2,0,1,0,2) the folded Regge midpoint numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one of the 256 kernel point checks that assemble the global m2Num = 8·explicitZ identity. The proof is a single kernel decision on two concrete integers.

Claim. For indices $(a,b,c,d,i,j)=(3,2,0,1,0,2)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(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 14 of a 256-way split of the 4D Regge exact-midpoint identity for the $m_2$ numerator. The ambient setting is discrete gravity on a 4-simplex skeleton: one checks that a folded sum of coupling contributions matches a closed-form integer table, up to the universal factor 8.

Upstream, $m_2^{\mathrm{num}}$ is defined by folding couplingZList and accumulating each term's contribution at a six-index in $\mathbb{F}_4$. The companion table $Z$ is an explicit pattern-matched integer function on the same six indices (sample clauses return $4$, $-2$, etc.). The claim is the pointwise equality of those two integers at one fixed multi-index.

proof idea

One-line computational proof: decide evaluates both sides at the concrete Fin-4 tuple $(3,2,0,1,0,2)$ and checks integer equality in the kernel. No algebraic rewriting or named lemmas are invoked beyond the definitions of the numerator fold and the explicit $Z$ table.

why it matters

Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-index in $(\mathbb{F}_4)^6$ by exhausting cases. That global equality is the certified kernel step for the 4D Regge exact-midpoint $m_2$ TT identity used in the gravity analysis stack. Within Recognition Science this is pure discrete-geometry bookkeeping supporting the continuum limit of the recognition-derived gravitational sector; it does not itself invoke the forcing chain (T5–T8) or the RCL, but it hardens the discrete curvature side those continuum claims rest on.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.