Gravity Ilgasymptotic Enhancement Enhancement Strict Mono

A monotone radial weight

The declaration enhancement_strict_mono establishes a monotonicity property for a specific function used in the framework's model of galactic rotation. The function, written as w(R) = 1 + C·(R/r0)^n, is a radial weight: it multiplies the Newtonian prediction for a galaxy's rotation speed at a given radius R, with r0 a reference scale, C a positive constant, and n a positive integer exponent. The theorem states that if R1 < R2, then w(R1) < w(R2). In plain terms, as you look farther from the galactic center, the weight factor strictly increases; it never stays flat and never decreases.

This monotonicity is one of four structural facts the framework's library proves about this weight function. Together with the facts that w is always positive, always greater than 1, and grows without bound as R grows, these properties form the backbone of a prediction about rotation curves. The prediction: the modified velocity squared, which is the weight times the Newtonian baryonic prediction, exceeds the Newtonian value at every radius and grows without bound, so the rotation curve cannot decay in the Keplerian manner that a purely Newtonian model would give.

The proof works over natural-power exponents n ≥ 1, which gives the same qualitative envelope as the real exponent α = 1 − 1/φ that appears in the framework's fuller treatment. The library states the real-exponent version uses the same logical proof but works with a different formal surface. The theorem is checked by the machine: the file reports 0 sorry and 0 new axioms.

What this declaration does not claim is as important as what it does. It does not assert that this monotone weight function is the correct description of any particular galaxy, nor does it claim that the framework's model matches observed rotation curves. The theorem is a structural fact about a mathematical function defined within the framework. Whether that function corresponds to reality is a separate question, addressed elsewhere by comparing predictions against data. The monotonicity itself is a consequence of the function's definition and the positivity of its parameters, not an empirical finding.

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

/-- 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 ilgAsymptoticEnhancementCert_holds : Nonempty ILGAsymptoticEnhancementCert :=
  ⟨{ C_pos := C_lock_pos
     enhancement_pos := enhancement_pos
     enhancement_above_one := enhancement_above_one
     enhancement_strict_mono := enhancement_strict_mono
     enhancement_unbounded := enhancement_unbounded
     newtonian_dominated := ilg_velocity_sq_dominates_newtonian
     btfr_slope_iff := btfr_slope_identity_iff }⟩

What this page does not claim

The monotonicity theorem says nothing about whether the framework's model matches any observed galaxy's rotation curve. The theorem does not establish that the weight function is the unique or correct form for galactic dynamics. The proof's restriction to natural-power exponents does not claim the real-exponent version is false, only that it uses a different formal surface.

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: