Encyclopedia Gravity Gravity Ilgasymptotic Enhancement

ARTICLE 4 claims 4 theorems

Gravity Ilgasymptotic Enhancement

A simple multiplier on Newton's law of gravity, derived from the framework's ledger, is proved to grow without bound, which keeps spiral galaxy rotation curves flat instead of falling off.

Verify this page

The radial weight and its proof

In classical Newtonian gravity, the orbital speed of a star at radius R around a galaxy should fall off as 1/√R once you are outside the bulk of the mass. Observations of spiral galaxies show the speed stays roughly flat, a discrepancy that motivates modified gravity theories. Information-Limited Gravity (ILG) is one such theory: it multiplies the Newtonian prediction by a radial weight w(R) = 1 + C·(R/r₀)^α, where r₀ is a scale radius, α = 1 − 1/φ is a dynamical-time exponent, and C = φ^(−3/2) is a locked amplitude. Both α and C are derived within the framework, not chosen to fit data.

The framework establishes four structural facts about this weight, proved with no unproved assumptions. First, the weight is always positive. Second, it is always greater than 1, meaning the ILG prediction always exceeds the Newtonian baryonic prediction. Third, it is strictly increasing with radius. Fourth, it is unbounded: for any positive threshold M, there exists a radius at which the weight exceeds M. The proof works with natural-power exponents to avoid technicalities, but the same qualitative envelope holds for the real exponent α. The key consequence is that the ILG-modified velocity squared, V²(R) = w(R)·V_bar²(R), always dominates the Newtonian value, so the rotation curve cannot decay Keplerianly.

This unbounded growth is the structural reason the framework predicts flat rotation curves. The framework also records a Baryonic Tully-Fisher Relation (BTFR) slope identity: in the deep-ILG limit, the observed acceleration approaches the geometric mean of the Newtonian acceleration and a constant, which yields M = V⁴/(G·a₀), so the BTFR slope β = 4. This identity is stated as a proposition and proved equivalent to a simple algebraic rearrangement; the numerical confirmation against SPARC data sits in a separate scorecard module, not in this file.

What the framework does not do is integrate the velocity profile over a full disk or fit the SPARC data. It proves the structural envelope: the weight is positive, above one, monotone, and unbounded, which forces the velocity-squared dominance over Newtonian. The physical bridge from the framework's ledger to the ILG weight is itself an open target, but the radial weight's structural behavior is a proved theorem.

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)]
THEOREM enhancement_above_one · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
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
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
THEOREM btfr_slope_identity_iff · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
btfr_slope_identity_iff · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean:177 
theorem btfr_slope_identity_iff : BTFRSlopeIdentity := by
  intros M V a0 G _hM _hV ha0 hG
  have hpos : 0 < G * a0 := mul_pos hG ha0
  have hne : (G * a0) ≠ 0 := ne_of_gt hpos
  constructor
  · intro h
    have : M * (G * a0) = (V ^ 4 / (G * a0)) * (G * a0) := by rw [h]
    rw [this, div_mul_cancel₀ _ hne]
  · intro h
    have : V ^ 4 = M * (G * a0) := h.symm
    rw [this, mul_div_assoc, div_self hne, mul_one]

What this page does not claim

The framework does not fit the SPARC data or numerically confirm the BTFR slope against observations. The physical derivation of the ILG radial weight from the recognition ledger is not proved here. The real-exponent version of the enhancement theorems is not formalized in this module, only the natural-power envelope.

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