Gravity Ilgreal Exponent Enhancement W Real

The radial weight function

In classical physics, the strength of a force usually fades with distance. Gravity, for example, follows an inverse-square law: double the distance and the pull drops to a quarter. The function w_real describes the opposite behavior, a radial enhancement where the effect grows as you move away from a central point. It is defined as w_real(R, r0, α) = 1 + C_lock · (R / r0)^α, where R is the distance from the center, r0 is a reference distance, α is a positive real exponent, and C_lock is a positive constant.

The function's behavior is governed by four properties, each one a formal theorem in the framework's machine-checked library of formal theorems. First, w_real is always greater than 1 for any positive R and r0, meaning the enhancement is a genuine increase, never a decrease. Second, it is strictly increasing in R: as the distance grows, the enhancement grows without exception. Third, it is unbounded, so no matter how large a value you name, there is some distance R at which w_real exceeds it. Fourth, when w_real multiplies a nonnegative quantity V_bar_sq, the product is at least as large as V_bar_sq itself; the enhancement never shrinks what it acts on.

These properties are not assumed but proved. The theorems enhancement_real_above_one, enhancement_real_strict_mono, enhancement_real_unbounded, and ilg_real_velocity_sq_dominates_newtonian are all derived from the definition of w_real, the positivity of C_lock, and the basic properties of real exponentiation. The proofs contain no gaps and introduce no new axioms. A single certificate structure, ILGRealExponentEnhancementCert, bundles all four properties together, and the theorem ilgRealExponentEnhancementCert_holds confirms that this certificate is nonempty, meaning the properties are consistent and instantiated.

In Recognition Science, this function plays a specific role. It is the real-exponent radial enhancement used in the ILG (Inverse-Law Gravity) asymptotic enhancement module. The exponent α is locked to the value 1 − 1/φ, where φ is the golden ratio, a connection that ties this gravity-like behavior to the framework's foundational constants. The framework models a scenario where the gravitational effect, instead of weakening, strengthens with distance according to this power law. The theorems establish the mathematical backbone of that scenario: the enhancement is always positive, always growing, and always dominant over the baseline it multiplies.

What w_real does not claim is equally important. It does not claim that this enhancement is observed in real gravity; that is an empirical question entirely outside these theorems. It does not claim that the exponent α must be 1 − 1/φ; the theorems hold for any positive real α, and the specific value is a separate identification, not a consequence of the proofs. It does not claim that C_lock has any particular numerical value; the theorems only require that it be positive. The function is a mathematical object with proven properties, and the framework's connection to physical reality is a further step, not part of this declaration.

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

theorem ilgRealExponentEnhancementCert_holds : Nonempty ILGRealExponentEnhancementCert :=
  ⟨{ C_pos := C_lock_pos
     enhancement_pos := enhancement_real_pos
     enhancement_above_one := enhancement_real_above_one
     enhancement_strict_mono := enhancement_real_strict_mono
     enhancement_unbounded := enhancement_real_unbounded
     newtonian_dominated := ilg_real_velocity_sq_dominates_newtonian }⟩

What this page does not claim

This function does not claim to describe observed gravity. The specific value of the exponent α is not derived in these theorems. The numerical value of C_lock is not fixed by these proofs.

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: