Gravity Analysis Regge Exact Midpoint M2 Ttidentity4 D Explicit M2 Coeff Eq Expl

The coefficient bridge

In four-dimensional geometry, a gravitational calculation often produces a large table of rational numbers, each one a coefficient in a formula. The declaration explicitM2Coeff_eq_explicitZ_div32 states that two such tables are the same: the rational table explicitM2Coeff equals the integer table explicitZ divided by 32, for every entry. The proof is a definitional equality, meaning the two expressions reduce to the same value by their definitions alone, with no extra assumptions.

This is a scale bridge. The integer table is the raw certificate, a list of whole numbers produced by a script. The rational table is what the physics uses, a list of fractions. The theorem says the fractions are not an approximation or a separate guess: they are exactly the integers divided by 32. The factor 32 is not fitted; it falls out of the definitions. This matters because the rational table feeds into a larger identity about the midpoint Bloch form, a quadratic expression in a metric and a wave vector. If the bridge were off by even one unit, the whole identity would fail.

The declaration is one small step in a chain that closes a four-dimensional identity. It does not claim that the identity itself is true; that is a separate theorem. It does not say anything about physics, only about the equality of two coefficient tables. It does not explain why the factor is 32, nor does it derive the tables from first principles. It is a certificate, a precise statement that one table is the other scaled by a constant, and that is all.

For a reader, the consequence is trust. A large calculation with hundreds of coefficients can hide a typo. This theorem, checked by a machine, removes that worry for the bridge step. The identity that follows can be examined on its own merits, knowing the coefficients it uses are exactly the integers divided by 32.

/-- Scale bridge: explicit ℚ table = Int table / 32 (definitional). -/
theorem explicitM2Coeff_eq_explicitZ_div32 :
    ∀ a b c d i j : Fin 4,
      explicitM2Coeff a b c d i j = (explicitZ a b c d i j : ℚ) / 32 := by
  intro a b c d i j
  rfl

/-- Scale bridge: explicit ℚ table = Int table / 32 (definitional). -/
theorem explicitM2Coeff_eq_explicitZ_div32 :
    ∀ a b c d i j : Fin 4,
      explicitM2Coeff a b c d i j = (explicitZ a b c d i j : ℚ) / 32 := by
  intro a b c d i j
  rfl

What this page does not claim

The declaration does not prove the four-dimensional identity itself, only the equality of two coefficient tables. The declaration does not explain why the scaling factor is 32 or derive the tables from first principles. The declaration makes no physical claim about gravity, only a mathematical statement about two tables of numbers.

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/ReggeExactMidpointM2TTIdentity4D.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: