Encyclopedia Gravity Gravity Ilgreal Exponent Enhancement Ilg Real Exponent Enhancement Cert Holds

ARTICLE 4 claims 4 theorems

Gravity Ilgreal Exponent Enhancement Ilg Real Exponent Enhancement Cert Holds

A machine-checked certificate proves that a specific radial weight function grows without bound, stays strictly increasing, and never drops below 1 for positive radii.

Verify this page

The real-exponent envelope

In the Recognition Science framework, gravity's rotation curves receive a radial enhancement: a multiplicative weight applied to a baseline velocity squared. The real-exponent version of this weight is defined as w_real(R, r0, α) = 1 + C_lock · (R/r0)^α, where R is the radius from the galactic center, r0 is a reference scale, α is a real exponent, and C_lock is a positive constant locked by the framework. The exponent of interest is α = 1 − 1/φ, where φ is the golden ratio, a value in the open interval (0,1).

The declaration ilgRealExponentEnhancementCert_holds is a theorem in the framework's machine-checked library of formal theorems. It bundles four structural facts about this weight into a single certificate object. First, the weight is always greater than 1 for any positive R and r0, meaning the enhancement strictly increases the baseline value. Second, the weight is strictly monotone in R: as R grows, so does the weight. Third, the weight is unbounded, tending to infinity as R tends to infinity. Fourth, the enhanced velocity squared always dominates the Newtonian baseline, since multiplying a nonnegative baseline by a factor greater than 1 cannot decrease it. The certificate is proved with zero axioms beyond the framework's standard three, and the declaration simply asserts that such a certificate exists.

What this certificate does not claim is equally important. It does not assert that α = 1 − 1/φ is derived from the framework's forcing chain; the exponent is locked by identification, not by proof. It does not claim that the weight function is the actual gravitational law, only that it is a structural envelope with the stated monotonicity and growth properties. It does not claim that the enhancement matches any specific astronomical observation, since the certificate is a purely formal statement about a defined function. Finally, it does not claim that the weight applies to negative radii or zero reference scales, since every theorem requires R > 0 and r0 > 0.

THEOREM enhancement_real_above_one · IndisputableMonolith/Gravity/ILGRealExponentEnhancement.lean
enhancement_real_above_one · IndisputableMonolith/Gravity/ILGRealExponentEnhancement.lean:45 
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 · IndisputableMonolith/Gravity/ILGRealExponentEnhancement.lean
enhancement_real_strict_mono · IndisputableMonolith/Gravity/ILGRealExponentEnhancement.lean:55 
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
THEOREM enhancement_real_unbounded · IndisputableMonolith/Gravity/ILGRealExponentEnhancement.lean
enhancement_real_unbounded · IndisputableMonolith/Gravity/ILGRealExponentEnhancement.lean:83 
/-- 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 ilg_real_velocity_sq_dominates_newtonian · IndisputableMonolith/Gravity/ILGRealExponentEnhancement.lean
ilg_real_velocity_sq_dominates_newtonian · IndisputableMonolith/Gravity/ILGRealExponentEnhancement.lean:72 
/-- 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 exponent α = 1 − 1/φ is derived from the framework's forcing chain. The weight function is the actual gravitational law, rather than a structural envelope. The certificate matches any specific astronomical observation.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND