Gravity Ilgasymptotic Enhancement Ilg Asymptotic Enhancement Cert Holds

The enhancement certificate

In classical Newtonian gravity, a star orbiting a central mass feels a force that weakens with the square of distance, so its orbital speed falls off as the inverse square root of radius. Astronomers measuring spiral galaxies since the 1970s found instead that rotation curves stay flat far beyond the visible disk, a discrepancy that motivates modified gravity theories. One such theory, Information-Limited Gravity (ILG), alters the Newtonian prediction by a radial weight w(R) = 1 + C·(R/r0)^α, where α = 1 − 1/φ (with φ the golden ratio) and C = φ^(−3/2), both derived from deeper principles in the Recognition Science framework. The declaration ilgAsymptoticEnhancementCert_holds is a machine-checked certificate that bundles the essential structural properties of this weight into one theorem.

The certificate establishes four facts about w(R) for any positive radius R and scale r0, using a natural-power exponent n ≥ 1 that reproduces the same qualitative envelope as the real exponent α. First, the weight is always positive. Second, it is always greater than 1, meaning the ILG-modified velocity squared exceeds the Newtonian baryonic prediction at every radius. Third, the weight is strictly increasing with radius, so the enhancement grows as you move outward. Fourth, it is unbounded: for any positive threshold M, there exists a radius R* where the weight exceeds M, formalizing asymptotic divergence. A fifth bundled theorem states that the ILG velocity squared dominates the Newtonian value: V²(R) = w(R)·V_bar²(R) ≥ V_bar²(R). Together these imply the rotation curve cannot decay Keplerianly; it must stay above Newton's prediction and grow without bound.

In Recognition Science, this certificate is a structural prediction, not a fitted curve. The framework's library proves these facts with zero axioms beyond the standard three, and the docstring records the same qualitative envelope holds for the real-exponent version. The certificate also bundles a slope identity for the Baryonic Tully-Fisher Relation, the observed power law M_bary ∝ V_flat^β. The framework predicts β = 4, matching the deep-ILG limit where a_obs ≈ (a_0·a_bar)^(1/2), the same regime as MOND. That identity is recorded as a Prop and proved as an equivalence of two algebraic forms, but the integration from the acceleration relation to the slope is not formalized; the numerical confirmation sits in a separate scorecard file.

What the certificate does not claim is just as important as what it proves. It does not establish that the ILG weight matches any measured rotation curve; that is an empirical check against SPARC data, not a theorem. It does not prove the BTFR slope β = 4 from first principles, only the algebraic equivalence behind it. And it works over rational exponents n, not the full real exponent α, though the docstring states the real version is logically the same proof. The certificate is a structural backbone: it guarantees the qualitative shape of the prediction, leaving the quantitative comparison to observation as a separate, testable step.

/-- 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_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

/-- 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 : 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 certificate does not prove that ILG matches any measured rotation curve; that is an empirical check, not a theorem. The certificate does not derive the BTFR slope β = 4 from the acceleration relation; only the algebraic equivalence is formalized. The certificate works over rational exponents n, not the full real exponent α, though the docstring states the real version is logically the same proof.

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: