Encyclopedia Gravity Gravity Ilgderivation

ARTICLE 4 claims 4 theorems

Gravity Ilgderivation

The ILG time-kernel is the unique correction to Newtonian gravity forced by the recognition lag, and its monotonic growth and unbounded divergence are what rotation-curve flattening structurally means.

Verify this page

The ILG time-kernel

The ILG time-kernel is a function that modifies Newtonian gravity at large scales. In Recognition Science, it is the unique correction forced by the recognition lag, the fixed cost of recognizing a later state of a system. The kernel is written w_t and it multiplies the Newtonian squared velocity. Its formula is not fitted: it is determined by two constants that come out of the forcing chain, the recognition lag C_lag = phi^-5 and the fine-structure exponent alpha = (1 - 1/phi)/2. The theorem w_t_formula_grounded states this exactly.

The kernel has two established properties that together carry the structural content of flat rotation curves. First, on the un-clamped region where the dynamical time is large enough, the kernel is strictly increasing in the dynamical time whenever alpha and C_lag are positive. Longer orbits get a strictly larger recognition-lag enhancement, so the ILG rotation curve decays strictly slower than the Keplerian curve at every radius. This is the theorem w_t_strictMono_unclamped. Second, the enhancement is unbounded: as the dynamical time grows without bound, w_t tends to infinity. No finite radius exhausts the recognition-lag correction. This is the theorem w_t_tendsto_atTop. The combined theorem rotational_flatness_forced states both properties together, and rotational_flatness_unbounded makes the divergence explicit: for any finite bound M there is a dynamical time beyond which the kernel exceeds M.

The consequence is that the enhanced squared velocity w_t(Tdyn(r)) times v_N(r)^2 decays strictly slower than the Newtonian v_N(r)^2 proportional to 1/r at every scale. That is what "rotation curves flatten" means structurally. The exact asymptotic velocity value is an empirical matter, to be settled by fits to SPARC data, not a theorem. The module does not claim a specific flat velocity; it claims the shape of the correction and its unbounded growth.

THEOREM w_t_formula_grounded · IndisputableMonolith/Gravity/ILGDerivation.lean
w_t_formula_grounded · IndisputableMonolith/Gravity/ILGDerivation.lean:9 
/-- **THEOREM: ILG Time-Kernel Derivation**
    The time-kernel $w_t$ is uniquely determined by the recognition lag $C_{lag} = \varphi^{-5}$
    and the fine-structure exponent $\alpha$.

    This theorem formalizes the connection between the RRF gradient cost and the
    effective modified gravity at large scales. -/
theorem w_t_formula_grounded (P : Params) (Tdyn τ0 : ℝ) :
    P.Clag = phi ^ (-(5 : ℝ)) →
    P.alpha = (1 - 1/phi) / 2 →
    w_t P Tdyn τ0
      = 1 + (phi ^ (-(5 : ℝ)))
          * (Real.rpow (max defaultConfig.eps_t (Tdyn / τ0)) ((1 - 1/phi) / 2) - 1) := by
  intro hClag hAlpha
  simp [w_t, w_t_with, hClag, hAlpha]
THEOREM w_t_strictMono_unclamped · IndisputableMonolith/Gravity/ILGDerivation.lean
w_t_strictMono_unclamped · IndisputableMonolith/Gravity/ILGDerivation.lean:24 
/-- **Kernel strict monotonicity (rotational flattening, part 1).**
    On the un-clamped region (`eps_t ≤ Tdyn/τ0`), the ILG time-kernel is
    strictly increasing in the dynamical time whenever `alpha > 0` and
    `Clag > 0`. Longer orbits get a strictly larger recognition-lag
    enhancement, so the ILG rotation curve decays strictly slower than
    Keplerian at every radius: `w(T₂)·K/r₂ ÷ w(T₁)·K/r₁ > (K/r₂)/(K/r₁)`. -/
theorem w_t_strictMono_unclamped (P : Params) (τ0 : ℝ) (hτ : 0 < τ0)
    (hα : 0 < P.alpha) (hC : 0 < P.Clag) :
    ∀ T₁ T₂ : ℝ, defaultConfig.eps_t ≤ T₁ / τ0 → T₁ < T₂ →
      w_t P T₁ τ0 < w_t P T₂ τ0 := by
  intro T₁ T₂ h1 hlt
  have heps : (0 : ℝ) < defaultConfig.eps_t := by norm_num [defaultConfig]
  have h1pos : (0 : ℝ) < T₁ / τ0 := lt_of_lt_of_le heps h1
  have hdiv : T₁ / τ0 < T₂ / τ0 := by gcongr
  have hm1 : max defaultConfig.eps_t (T₁ / τ0) = T₁ / τ0 := max_eq_right h1
  have hm2 : max defaultConfig.eps_t (T₂ / τ0) = T₂ / τ0 :=
    max_eq_right (le_trans h1 hdiv.le)
  have hr : Real.rpow (T₁ / τ0) P.alpha < Real.rpow (T₂ / τ0) P.alpha :=
    Real.rpow_lt_rpow h1pos.le hdiv hα
  simp only [w_t, w_t_with, hm1, hm2]
  nlinarith [hr, hC]
THEOREM w_t_tendsto_atTop · IndisputableMonolith/Gravity/ILGDerivation.lean
w_t_tendsto_atTop · IndisputableMonolith/Gravity/ILGDerivation.lean:46 
/-- **Kernel divergence (rotational flattening, part 2).**
    For `alpha > 0`, `Clag > 0`, the enhancement is unbounded in the
    dynamical time: `w_t → ∞` as `Tdyn → ∞`. No finite radius exhausts the
    recognition-lag correction. -/
theorem w_t_tendsto_atTop (P : Params) (τ0 : ℝ) (hτ : 0 < τ0)
    (hα : 0 < P.alpha) (hC : 0 < P.Clag) :
    Filter.Tendsto (fun Tdyn => w_t P Tdyn τ0) Filter.atTop Filter.atTop := by
  have h1 : Filter.Tendsto (fun T : ℝ => T / τ0) Filter.atTop Filter.atTop :=
    Filter.tendsto_id.atTop_div_const hτ
  have h2 : Filter.Tendsto (fun T : ℝ => max defaultConfig.eps_t (T / τ0))
      Filter.atTop Filter.atTop :=
    Filter.tendsto_atTop_mono (fun T => le_max_right _ _) h1
  have h3 : Filter.Tendsto (fun t : ℝ => Real.rpow t P.alpha)
      Filter.atTop Filter.atTop := tendsto_rpow_atTop hα
  have h4 := h3.comp h2
  have h5 := Filter.tendsto_atTop_add_const_right Filter.atTop (-1 : ℝ) h4
  have h6 := Filter.Tendsto.const_mul_atTop hC h5
  have h7 := Filter.tendsto_atTop_add_const_left Filter.atTop (1 : ℝ) h6
  simpa [w_t, w_t_with, Function.comp, sub_eq_add_neg] using h7
THEOREM rotational_flatness_forced · IndisputableMonolith/Gravity/ILGDerivation.lean
rotational_flatness_forced · IndisputableMonolith/Gravity/ILGDerivation.lean:66 
/-- **THEOREM: Rotational flattening forced (honest form).**
    Replaces the former vacuous placeholder (`∃ v_flat, ... ∀ r, True`, which
    proved nothing). What the ILG kernel actually forces, and what this
    theorem states: for `alpha > 0` and `Clag > 0` the enhancement
    (i) strictly grows with dynamical time on the un-clamped region, and
    (ii) diverges as `Tdyn → ∞`. Consequently the enhanced squared velocity
    `w_t(Tdyn(r)) · v_N(r)²` decays strictly slower than the Newtonian
    `v_N(r)² ∝ 1/r` at every scale, which is the structural content of
    "rotation curves flatten." The exact asymptotic velocity value is an
    empirical matter (SPARC fits), not a theorem, and is not claimed here. -/
theorem rotational_flatness_forced (P : Params) (τ0 : ℝ) (hτ : 0 < τ0)
    (hα : 0 < P.alpha) (hC : 0 < P.Clag) :
    (∀ T₁ T₂ : ℝ, defaultConfig.eps_t ≤ T₁ / τ0 → T₁ < T₂ →
      w_t P T₁ τ0 < w_t P T₂ τ0)
    ∧ Filter.Tendsto (fun Tdyn => w_t P Tdyn τ0) Filter.atTop Filter.atTop :=
  ⟨w_t_strictMono_unclamped P τ0 hτ hα hC, w_t_tendsto_atTop P τ0 hτ hα hC⟩

What this page does not claim

The exact asymptotic rotation velocity is not derived here; it is an empirical matter. The fine-structure constant alpha is not derived in this module; it is an input parameter. This module does not claim a specific modified-gravity action or field equation.

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/ILGDerivation.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