Gravity Ilgreal Exponent Enhancement Ilg Real Velocity Sq Dominates Newtonian

The domination theorem

The statement ilg_real_velocity_sq_dominates_newtonian is a formal theorem in the Recognition Science framework's machine-checked library. It concerns a quantity called w_real, a radial weight defined as w_real(R, r0, α) = 1 + C_lock · (R/r0)^α. Here R is a distance from a source, r0 is a reference radius, α is a positive real exponent, and C_lock is a positive constant. The theorem states that for any nonnegative value V_bar_sq, and for any positive R and r0, the inequality V_bar_sq ≤ w_real(R, r0, α) · V_bar_sq holds.

In plain terms, the theorem says that multiplying a nonnegative quantity by the radial weight w_real never decreases it. If V_bar_sq is interpreted as the square of a Newtonian velocity, then the theorem establishes that the corresponding velocity squared in this model is always at least as large as the Newtonian value. The proof is short: it relies on the fact that w_real is always greater than 1 for positive arguments, so multiplying by w_real cannot shrink a nonnegative number. This is a purely mathematical statement about real numbers; it does not by itself assert anything about physical gravity.

The theorem is part of a larger set of results about the real-exponent enhancement w_real. The same module proves that w_real is strictly increasing in R, that it grows without bound as R grows, and that it is always greater than 1. These facts together describe a weight that starts above 1 and increases without limit. The domination theorem is the direct consequence of the weight being above 1.

In the Recognition Science framework, this result is presented as a structural fact about a model of gravity. The framework does not claim that this theorem alone derives the full content of general relativity or Newtonian gravity. The theorem is a statement about a specific mathematical function and its properties. It does not specify what C_lock is, what α must be, or how w_real relates to any measured gravitational phenomenon. Those are separate questions, some of which the framework addresses elsewhere and some of which remain open.

What the theorem does establish is a clean, checkable inequality: a nonnegative Newtonian velocity squared is dominated by the enhanced velocity squared. This is a concrete mathematical anchor. It guarantees that within this model, the enhancement never reduces the velocity below the Newtonian baseline. The practical consequence is that any further work in the framework that uses w_real can rely on this monotonicity property without re-proving it.

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

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

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

What this page does not claim

The theorem does not assert that w_real describes actual gravity in the universe. It does not specify the values of C_lock or α. It does not claim that the Newtonian velocity square V_bar_sq is a measured quantity.

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: