Gravity Ilgreal Exponent Enhancement

The real-exponent weight

In classical gravity, the inverse-square law describes how the force weakens with distance. Some extensions of gravity propose that at very large scales, the force does not fall off quite as fast, producing an enhancement over the Newtonian prediction. The Recognition Science framework formalizes one such extension through a radial weight function: w(R, r0, α) = 1 + C · (R/r0)^α, where R is the distance from the source, r0 is a reference scale, C is a positive constant, and α is the enhancement exponent.

The framework's library of machine-checked formal theorems has now extended its analysis from integer powers to the locked real exponent α = 1 − 1/φ, where φ is the golden ratio. This value lies strictly between 0 and 1, making the enhancement grow more slowly than a linear function but still without bound. The module proves four structural facts about this real-exponent weight. First, the weight is always greater than 1 for any positive distance and reference scale. Second, it is strictly increasing as the distance grows. Third, it diverges to infinity as the distance tends to infinity. Fourth, the resulting velocity squared always dominates the Newtonian value.

These results are not merely asserted; they are proven in the framework's formal library with zero unproven assumptions and zero new axioms. The proofs rely on standard properties of real powers and the positivity of the locked constant. The module also bundles these theorems into a certificate structure, a single object that packages all four guarantees together, and proves that this certificate exists. This means the entire set of properties holds simultaneously for the real-exponent enhancement.

The practical consequence is that the real-exponent enhancement, unlike some integer-power versions, cannot saturate or turn over. It keeps growing as far as the theory is taken, and it never dips below the Newtonian curve. This gives the framework a clean, monotone, unbounded correction to gravity at large scales, with the specific exponent tied to the golden ratio. The theorems establish the mathematical envelope; whether this matches observed galactic rotation curves remains a separate empirical question.

theorem enhancement_real_above_one (R r0 α : ℝ)
    (hR : 0 < R) (hr0 : 0 < r0) :
    1 < w_real R r0 α := by
  unfold w_real
  have hC : 0 < C_lock := C_lock_pos
  have hd : 0 < R / r0 := div_pos hR hr0
  have hpow : 0 < (R / r0) ^ α := Real.rpow_pos_of_pos hd α
  have : 0 < C_lock * (R / r0) ^ α := mul_pos hC hpow
  linarith

theorem enhancement_real_strict_mono (R₁ R₂ r0 α : ℝ)
    (hR₁ : 0 < R₁) (hR₂ : R₁ < R₂) (hr0 : 0 < r0) (hα : 0 < α) :
    w_real R₁ r0 α < w_real R₂ r0 α := by
  unfold w_real
  have hC : 0 < C_lock := C_lock_pos
  have h1 : 0 < R₁ / r0 := div_pos hR₁ hr0
  have h2 : 0 < R₂ / r0 := div_pos (lt_trans hR₁ hR₂) hr0
  have hd : 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) ^ α < (R₂ / r0) ^ α :=
    Real.rpow_lt_rpow (le_of_lt h1) hd hα
  have hmul_lt : C_lock * (R₁ / r0) ^ α < C_lock * (R₂ / r0) ^ α :=
    mul_lt_mul_of_pos_left hpow_lt hC
  linarith

/-- Asymptotic divergence of the real-exponent enhancement. -/
theorem enhancement_real_unbounded (r0 α : ℝ)
    (hr0 : 0 < r0) (hα : 0 < α)
    (M : ℝ) (hM : 0 < M) :
    ∃ R : ℝ, 0 < R ∧ M < w_real R r0 α := by
  unfold w_real
  -- Want C_lock * (R/r0)^α > M, i.e. (R/r0)^α > M/C_lock.
  set u : ℝ := M / C_lock + 1 with hu_def
  have hC : 0 < C_lock := C_lock_pos
  have hu_pos : 0 < u := by
    have h₁ : 0 < M / C_lock := div_pos hM hC
    have : 0 < M / C_lock + 1 := by linarith
    simpa [hu_def] using this
  -- Choose y so that y^α = u, namely y = u^(1/α).
  have hα_ne : α ≠ 0 := ne_of_gt hα
  set y : ℝ := u ^ (1 / α) with hy_def
  have hy_pos : 0 < y := by
    have : 0 < u ^ (1 / α) := Real.rpow_pos_of_pos hu_pos (1 / α)
    simpa [hy_def] using this
  have hyα : y ^ α = u := by
    have h_inv : (1 / α) * α = 1 := by
      field_simp
    have hmul := Real.rpow_mul (le_of_lt hu_pos) (1 / α) α
    -- hmul : u ^ ((1/α) * α) = (u ^ (1/α)) ^ α
    rw [hy_def, ← hmul, h_inv, Real.rpow_one]
  -- Set R = r0 * y; then (R/r0)^α = y^α = u, and C_lock * u = M + C_lock > M.
  refine ⟨r0 * y, mul_pos hr0 hy_pos, ?bound⟩
  have hratio : (r0 * y) / r0 = y := by field_simp
  have hRpow : ((r0 * y) / r0) ^ α = u := by rw [hratio]; exact hyα
  have hCu : C_lock * u = M + C_lock := by
    have : C_lock * (M / C_lock + 1) = M + C_lock := by field_simp
    simpa [hu_def] using this
  have hCpos : 0 < C_lock := hC
  have : C_lock * ((r0 * y) / r0) ^ α = M + C_lock := by
    rw [hRpow]; exact hCu
  linarith

/-- Newtonian-domination at the real-exponent level. -/
theorem ilg_real_velocity_sq_dominates_newtonian
    (V_bar_sq R r0 α : ℝ)
    (hVb : 0 ≤ V_bar_sq) (hR : 0 < R) (hr0 : 0 < r0) :
    V_bar_sq ≤ w_real R r0 α * V_bar_sq := by
  have hw : 1 < w_real R r0 α := enhancement_real_above_one R r0 α hR hr0
  have hwle : 1 ≤ w_real R r0 α := le_of_lt hw
  have : V_bar_sq * 1 ≤ V_bar_sq * w_real R r0 α :=
    mul_le_mul_of_nonneg_left hwle hVb
  linarith [mul_comm V_bar_sq (w_real R r0 α)]

What this page does not claim

The module does not prove that the real-exponent enhancement matches any observed galactic rotation data. The module does not derive the value of the constant C_lock; it only assumes it is positive. The theorems do not apply to negative distances or reference scales, which are excluded by hypothesis.

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/ILGRealExponentEnhancement.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: