Gravity Analysis Regge Exact Midpoint M2 Ttidentity4 Dkernel Glue Sum Term Q Eq

The kernel identity

The declaration sum_termQ_eq_explicitZ_div32 is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that for any choice of six indices a, b, c, d, i, j, each ranging over the four values 0, 1, 2, 3, the sum of certain rational terms termQ over a fixed list of couplings equals the integer combination explicitZ divided by 32. In plain language: a particular weighted sum of rational numbers, built from coupling coefficients and index-dependent factors, collapses to a single integer-scaled value.

The theorem is the final step in a chain that bridges two representations of the same quantity. Earlier theorems in the same file show that each termQ equals a corresponding integer contribution divided by 256, and that the sum of those contributions equals the integer m2Num divided by 256. The new theorem uses a scaling identity to rewrite m2Num divided by 256 as explicitZ divided by 32, so the whole sum over the coupling table matches the explicitZ form. The proof is by rewriting: it applies the earlier equalities and then simplifies the arithmetic with the ring tactic.

What the theorem does not claim is important. It does not assert that the sum equals any particular numeric value, because the indices a, b, c, d, i, j are arbitrary variables. It does not claim that explicitZ has any physical meaning on its own; explicitZ is defined as a specific integer function, and the theorem only relates the sum to it. The theorem also does not prove that the underlying gravity calculation is correct, only that this particular algebraic identity holds. The earlier theorem symFullQ_explicitZ_eq_closedZ, which compares explicitZ to a closed-form expression, is a separate statement and is not part of this declaration.

In the context of the framework, this identity is a kernel-level bridge: it closes a typed blocker in the gravity analysis by showing that the sum of rational terms can be expressed in the integer-scaled form needed for further reasoning. The practical consequence is that a computation that might otherwise require floating-point approximation is replaced by an exact rational equality, which the machine-checked library can verify by computation. This is a small but concrete step in the framework's program of deriving physical structure from exact, checkable arithmetic.

theorem sum_termQ_eq_explicitZ_div32 (a b c d i j : Fin 4) :
    (∑ idx : CouplingIdx, termQ couplingTable[idx] a b c d i j) =
      (explicitZ a b c d i j : ℚ) / 32 := by
  rw [sum_termQ_eq_m2Num_div256, m2Num_div256_eq_explicitZ_div32]

theorem sum_termQ_eq_explicitZ_div32 (a b c d i j : Fin 4) :
    (∑ idx : CouplingIdx, termQ couplingTable[idx] a b c d i j) =
      (explicitZ a b c d i j : ℚ) / 32 := by
  rw [sum_termQ_eq_m2Num_div256, m2Num_div256_eq_explicitZ_div32]

What this page does not claim

This theorem does not assign a numerical value to the sum for any fixed indices. This theorem does not establish any physical meaning for explicitZ. This theorem does not verify the correctness of the underlying gravity calculation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelGlue.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: