Encyclopedia Gravity Gravity Ilgasymptotic Enhancement Enhancement Unbounded

ARTICLE 3 claims 3 theorems

Gravity Ilgasymptotic Enhancement Enhancement Unbounded

A machine-checked theorem says a gravity correction factor in the Recognition Science framework grows without limit at large distances, so rotation curves cannot fall off the way Newtonian gravity predicts.

Verify this page

The unbounded enhancement

In the Recognition Science framework, a ledger, a discrete record of recognition events, gives rise to a correction factor for gravity. The factor multiplies the Newtonian prediction for how fast stars orbit a galaxy. The framework's machine-checked library of formal theorems proves that this factor is always positive, always greater than one, strictly increases with distance, and has no upper bound as the distance grows.

The declaration enhancement_unbounded is the formal statement of the last property. For any positive threshold you choose, no matter how large, there exists a radius beyond which the correction factor exceeds that threshold. In plainer terms, the factor keeps climbing forever. The proof works with a simplified version of the exponent, using a natural number instead of a real one, but the library notes the qualitative result is the same for the actual exponent.

The consequence for galaxy rotation is direct. The framework's theorem ilg_velocity_sq_dominates_newtonian shows the modified velocity squared is always at least the Newtonian value. Combined with the unbounded growth, the rotation curve cannot decay in the Keplerian fashion, where velocity falls as the square root of distance. Instead, the curve stays flat or rises, which is the observed behavior that motivates modified gravity theories.

The framework also records a structural identity for the Baryonic Tully-Fisher Relation, the observed power-law link between a galaxy's baryonic mass and its flat rotation velocity. The identity states that mass equals velocity to the fourth power divided by a constant, a slope of four. This is recorded as a proposition, not a derived theorem, and the numerical confirmation lives in a separate scorecard file.

What the declaration does not claim is equally important. It does not prove that the correction factor matches any specific galaxy's rotation curve. It does not establish the value of the constant C_lock from first principles; that value is a definitional choice. And the unbounded growth is a mathematical property of the chosen function, not a physical measurement of any real galaxy.

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 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 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 declaration does not prove the correction factor matches any specific galaxy's rotation curve. The value of the constant C_lock is a definitional choice, not a derived result. The unbounded growth is a mathematical property of the chosen function, not a physical measurement.

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