Gravity Ilgasymptotic Enhancement Enhancement Above One

The radial weight

In the Recognition Science framework's Information-Limited Gravity (ILG) model, the radial weight is a function w(R) = 1 + C · (R / r0)^n, where R is a radius, r0 is a reference radius, C is a positive constant, and n is a positive integer. The declaration enhancement_above_one proves the theorem that for any positive R, r0, and n, this weight is always strictly greater than 1. In plain language: the model's modification to gravity always adds a positive amount, never subtracts or leaves it unchanged.

The proof is direct. Since R and r0 are positive, the ratio (R / r0)^n is positive. The constant C is defined as the square root of 1 over phi cubed, where phi is the golden ratio, and is itself positive. A positive constant times a positive number is positive, so the term C · (R / r0)^n is positive. Adding 1 to a positive number gives a number strictly greater than 1. The theorem is formalized in the framework's machine-checked library of formal theorems, with no unproved assumptions.

This inequality is the first step in a structural claim about rotation curves. The ILG model modifies the Newtonian baryonic velocity squared, V_bar², by multiplying it by the weight w(R). Because w(R) is always greater than 1, the ILG prediction for velocity squared is always at least as large as the Newtonian prediction. A separate theorem, ilg_velocity_sq_dominates_newtonian, formalizes this: V_bar² ≤ w(R) · V_bar². The model therefore predicts that rotation curves cannot decay as fast as the standard Keplerian expectation, because the enhancement grows without bound as R increases.

What the declaration does not claim is just as important. The theorem holds for the specific form of w(R) with a positive constant and a positive integer exponent n. It does not establish the physical correctness of the ILG model, nor does it compare the model's predictions against actual galaxy rotation data. The proof is a mathematical fact about a defined function, not an empirical validation. The framework's own documentation notes that the full real-exponent version, using α = 1 − 1/φ, is logically the same proof but is not formalized here; the integer-exponent version is used to avoid a more complex real-exponent surface.

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

/-- 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)]

What this page does not claim

The theorem does not establish the physical correctness of the ILG model or its agreement with any galaxy rotation data. The proof does not cover the real-exponent version of the radial weight; it is limited to positive integer exponents. The statement does not claim that the enhancement is large, only that it is strictly greater than 1.

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: