Encyclopedia Gravity Gravity Ilgasymptotic Enhancement Ilg Velocity Sq Dominates Newtonian

ARTICLE 4 claims 3 theorems 1 model

Gravity Ilgasymptotic Enhancement Ilg Velocity Sq Dominates Newtonian

A machine-checked theorem shows that a proposed modification to gravity makes its predicted rotation speeds exceed the Newtonian prediction at every radius.

Verify this page

The asymptotic dominance theorem

In the standard Newtonian picture, the orbital speed of a star around a galaxy's center falls off with distance: v² = GM/R. At large radii, this predicts a Keplerian decline, where the rotation curve drops. The theorem ilg_velocity_sq_dominates_newtonian in the framework's machine-checked library of formal theorems establishes that, under the Information-Limited Gravity (ILG) model, the predicted velocity squared is always at least the Newtonian value, and strictly greater at every positive radius.

The ILG model modifies the Newtonian prediction by a radial weight w(R) = 1 + C·(R/r0)^α, where α = 1 − 1/φ is the dynamical-time exponent and C = φ^(−3/2) is a locked amplitude from the three-channel factorization. The radial weight multiplies the Newtonian velocity squared: V²(R) = w(R)·V_bar²(R). The theorem proves that for any positive radius R, reference radius r0, and natural exponent n ≥ 1, the inequality V_bar_sq ≤ w_radial R r0 n * V_bar_sq holds, which is the statement that the ILG-modified velocity squared dominates the Newtonian baryonic prediction.

The proof relies on four structural facts about the radial weight, each proved in the same module: enhancement_pos (w(R) > 0), enhancement_above_one (w(R) > 1), enhancement_strict_mono (w is strictly increasing in R), and enhancement_unbounded (w(R) → ∞ as R → ∞ along a witness sequence). The theorem ilg_velocity_sq_dominates_newtonian is a direct corollary of enhancement_above_one: since w(R) > 1, multiplying the nonnegative Newtonian V_bar_sq by w(R) cannot decrease it. The proof uses only the positivity of the amplitude C_lock and the nonnegativity of the input velocity squared.

The theorem is a structural statement about the model's mathematics, not a claim about observed galaxies. It does not assert that the ILG model is true, that the SPARC data confirm it, or that any particular galaxy's rotation curve actually exhibits this dominance. The theorem is conditional on the ILG model's definitions and the assumption that the input V_bar_sq is nonnegative. The unbounded growth of w(R) is proved along a witness sequence, not for all radii simultaneously in the sense of a pointwise limit; the statement is that for any threshold M, there exists a radius R* where w exceeds M.

What the theorem does establish, within the framework, is that the ILG modification cannot produce a Keplerian decline at large radii. The rotation curve under ILG is forced to stay above the Newtonian curve everywhere and to grow without bound in the asymptotic regime. This is the structural backbone for the framework's claim that ILG reproduces the observed flat rotation curves of galaxies without dark matter. The theorem itself is a statement about the model's mathematics; the empirical check against SPARC data is a separate, unformalized numerical comparison.

THEOREM ilg_velocity_sq_dominates_newtonian · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
ilg_velocity_sq_dominates_newtonian · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean:140 
/-- The Newtonian baryonic velocity squared `V_bar²` for a point-mass
    enclosed `M_enc` and radius `R` is `G·M_enc/R`. The ILG-modified
    velocity squared is

      V²(R) = w(R) · V_bar²(R) ≥ V_bar²(R)

    so the ILG prediction is always ≥ Newtonian. -/
theorem ilg_velocity_sq_dominates_newtonian
    (V_bar_sq R r0 : ℝ)
    (hVb : 0 ≤ V_bar_sq) (hR : 0 < R) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n) :
    V_bar_sq ≤ w_radial R r0 n * V_bar_sq := by
  have hw : 1 < w_radial R r0 n := enhancement_above_one R r0 hR hr0 n hn
  have hwle : 1 ≤ w_radial R r0 n := le_of_lt hw
  have : V_bar_sq * 1 ≤ V_bar_sq * w_radial R r0 n :=
    mul_le_mul_of_nonneg_left hwle hVb
  linarith [mul_comm V_bar_sq (w_radial R r0 n)]
MODEL w_radial · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
w_radial · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean:54 
/-- The radial-weight function with a natural-power exponent `n ≥ 1`,
    giving the same monotone-and-unbounded envelope as the real exponent
    `α ∈ (0,1)`. -/
def w_radial (R r0 : ℝ) (n : ℕ) : ℝ := 1 + C_lock * (R / r0) ^ n
THEOREM enhancement_pos · enhancement_above_one · enhancement_strict_mono · enhancement_unbounded · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
enhancement_pos · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean:59 
theorem enhancement_pos (R r0 : ℝ) (hR : 0 < R) (hr0 : 0 < r0) (n : ℕ) :
    0 < w_radial R r0 n := by
  unfold w_radial
  have hpow : 0 ≤ (R / r0) ^ n := pow_nonneg (le_of_lt (div_pos hR hr0)) n
  have hC : 0 < C_lock := C_lock_pos
  have hCprod : 0 ≤ C_lock * (R / r0) ^ n := mul_nonneg (le_of_lt hC) hpow
  linarith
enhancement_above_one · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean:67 
theorem enhancement_above_one (R r0 : ℝ) (hR : 0 < R) (hr0 : 0 < r0)
    (n : ℕ) (hn : 0 < n) : 1 < w_radial R r0 n := by
  unfold w_radial
  have hpow : 0 < (R / r0) ^ n := pow_pos (div_pos hR hr0) n
  have hC : 0 < C_lock := C_lock_pos
  have h : 0 < C_lock * (R / r0) ^ n := mul_pos hC hpow
  linarith
enhancement_strict_mono · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean:75 
theorem enhancement_strict_mono (R₁ R₂ r0 : ℝ) (hR₁ : 0 < R₁)
    (hR₂ : R₁ < R₂) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n) :
    w_radial R₁ r0 n < w_radial R₂ r0 n := by
  unfold w_radial
  have hC : 0 < C_lock := C_lock_pos
  -- (R₁ / r0) ^ n < (R₂ / r0) ^ n
  have hd1 : 0 < R₁ / r0 := div_pos hR₁ hr0
  have hd_lt : R₁ / r0 < R₂ / r0 := by
    have hinv : 0 < r0⁻¹ := inv_pos.mpr hr0
    have : R₁ * r0⁻¹ < R₂ * r0⁻¹ := mul_lt_mul_of_pos_right hR₂ hinv
    simpa [div_eq_mul_inv] using this
  have hpow_lt : (R₁ / r0) ^ n < (R₂ / r0) ^ n :=
    pow_lt_pow_left₀ hd_lt (le_of_lt hd1) (Nat.pos_iff_ne_zero.mp hn)
  have hmul_lt : C_lock * (R₁ / r0) ^ n < C_lock * (R₂ / r0) ^ n := by
    exact mul_lt_mul_of_pos_left hpow_lt hC
  linarith
enhancement_unbounded · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean:92 
/-- For any positive lower threshold `M`, there exists a radius `R*` at
    which the enhancement exceeds `M`. This formalises "asymptotic
    divergence" of `w` along the witness sequence. -/
theorem enhancement_unbounded (r0 : ℝ) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n)
    (M : ℝ) (hM : 0 < M) :
    ∃ R : ℝ, 0 < R ∧ M < w_radial R r0 n := by
  unfold w_radial
  -- choose R := r0 * (M / C_lock)^(1/n) + r0 ...
  -- Simpler: pick R so that (R/r0)^n > M / C_lock, then C_lock*(R/r0)^n > M, so w > 1+M > M.
  have hC : 0 < C_lock := C_lock_pos
  -- Choose target u = max(1, M/C_lock + 1) for (R/r0)^n.
  set u := M / C_lock + 1 with hu_def
  have hu_pos : 0 < u := by
    have : 0 < M / C_lock := div_pos hM hC
    have : 0 < M / C_lock + 1 := by linarith
    simpa [hu_def] using this
  -- Pick R = r0 * u (so (R/r0)^1 = u, then (R/r0)^n ≥ u for u ≥ 1, n ≥ 1).
  -- We need u ≥ 1 to make (·)^n monotone past 1.
  refine ⟨r0 * (u + 1), ?pos, ?bound⟩
  · have : 0 < u + 1 := by linarith
    exact mul_pos hr0 this
  · -- (R/r0) = u + 1 > 1
    have hratio : (r0 * (u + 1)) / r0 = u + 1 := by
      field_simp
    have hge : 1 ≤ u + 1 := by linarith
    -- (u+1)^n ≥ u + 1 for n ≥ 1
    have hn_ne : n ≠ 0 := Nat.pos_iff_ne_zero.mp hn
    have hpow_ge : u + 1 ≤ (u + 1) ^ n := by
      have h₁ : (u + 1) ^ 1 = u + 1 := by ring
      have h₂ : (u + 1) ^ 1 ≤ (u + 1) ^ n :=
        pow_le_pow_right₀ hge (Nat.one_le_iff_ne_zero.mpr hn_ne)
      simpa [h₁] using h₂
    have hd_pow : (u + 1) ≤ ((r0 * (u + 1)) / r0) ^ n := by
      simp [hratio]; exact hpow_ge
    have : M < C_lock * (u + 1) := by
      have hCu : C_lock * u = C_lock * (M / C_lock + 1) := by simp [hu_def]
      have hexp : C_lock * (M / C_lock + 1) = M + C_lock := by
        field_simp
      have : C_lock * u = M + C_lock := by simp [hCu, hexp]
      have hadd : M + C_lock < C_lock * (u + 1) := by
        have hexp2 : C_lock * (u + 1) = C_lock * u + C_lock := by ring
        rw [hexp2]
        linarith
      linarith
    have hCprod : C_lock * (u + 1) ≤ C_lock * ((r0 * (u + 1)) / r0) ^ n :=
      mul_le_mul_of_nonneg_left hd_pow (le_of_lt hC)
    linarith
THEOREM enhancement_unbounded · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
enhancement_unbounded · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean:92 
/-- For any positive lower threshold `M`, there exists a radius `R*` at
    which the enhancement exceeds `M`. This formalises "asymptotic
    divergence" of `w` along the witness sequence. -/
theorem enhancement_unbounded (r0 : ℝ) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n)
    (M : ℝ) (hM : 0 < M) :
    ∃ R : ℝ, 0 < R ∧ M < w_radial R r0 n := by
  unfold w_radial
  -- choose R := r0 * (M / C_lock)^(1/n) + r0 ...
  -- Simpler: pick R so that (R/r0)^n > M / C_lock, then C_lock*(R/r0)^n > M, so w > 1+M > M.
  have hC : 0 < C_lock := C_lock_pos
  -- Choose target u = max(1, M/C_lock + 1) for (R/r0)^n.
  set u := M / C_lock + 1 with hu_def
  have hu_pos : 0 < u := by
    have : 0 < M / C_lock := div_pos hM hC
    have : 0 < M / C_lock + 1 := by linarith
    simpa [hu_def] using this
  -- Pick R = r0 * u (so (R/r0)^1 = u, then (R/r0)^n ≥ u for u ≥ 1, n ≥ 1).
  -- We need u ≥ 1 to make (·)^n monotone past 1.
  refine ⟨r0 * (u + 1), ?pos, ?bound⟩
  · have : 0 < u + 1 := by linarith
    exact mul_pos hr0 this
  · -- (R/r0) = u + 1 > 1
    have hratio : (r0 * (u + 1)) / r0 = u + 1 := by
      field_simp
    have hge : 1 ≤ u + 1 := by linarith
    -- (u+1)^n ≥ u + 1 for n ≥ 1
    have hn_ne : n ≠ 0 := Nat.pos_iff_ne_zero.mp hn
    have hpow_ge : u + 1 ≤ (u + 1) ^ n := by
      have h₁ : (u + 1) ^ 1 = u + 1 := by ring
      have h₂ : (u + 1) ^ 1 ≤ (u + 1) ^ n :=
        pow_le_pow_right₀ hge (Nat.one_le_iff_ne_zero.mpr hn_ne)
      simpa [h₁] using h₂
    have hd_pow : (u + 1) ≤ ((r0 * (u + 1)) / r0) ^ n := by
      simp [hratio]; exact hpow_ge
    have : M < C_lock * (u + 1) := by
      have hCu : C_lock * u = C_lock * (M / C_lock + 1) := by simp [hu_def]
      have hexp : C_lock * (M / C_lock + 1) = M + C_lock := by
        field_simp
      have : C_lock * u = M + C_lock := by simp [hCu, hexp]
      have hadd : M + C_lock < C_lock * (u + 1) := by
        have hexp2 : C_lock * (u + 1) = C_lock * u + C_lock := by ring
        rw [hexp2]
        linarith
      linarith
    have hCprod : C_lock * (u + 1) ≤ C_lock * ((r0 * (u + 1)) / r0) ^ n :=
      mul_le_mul_of_nonneg_left hd_pow (le_of_lt hC)
    linarith

What this page does not claim

The theorem does not assert that the ILG model is true or that observed galaxies exhibit this dominance. The theorem does not claim that the SPARC data confirm the ILG model. The theorem does not prove that the rotation curve cannot decay Keplerianly for all radii in a pointwise limit sense; it proves unbounded growth along a witness sequence.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND