Encyclopedia Gravity Gravity Ilgderivation W T Strict Mono Unclamped

ARTICLE 4 claims 4 theorems

Gravity Ilgderivation W T Strict Mono Unclamped

A formal theorem about a time-dependent factor in one theory of gravity shows that longer orbits get a strictly larger enhancement, and it says nothing about the final velocity value.

Verify this page

The monotone kernel

In the modified-gravity account developed in the machine-checked library, the rotation of a galaxy is described by a Newtonian baseline multiplied by an enhancement factor w_t (a time-kernel: a function that adjusts the Newtonian prediction depending on the orbital period). The declaration w_t_strictMono_unclamped is a proved theorem about that factor on the un-clamped region, the range where the ratio of dynamical time to a reference scale is at least a small threshold. It states that if the enhancement parameter alpha and the recognition lag Clag are both positive, then for any two dynamical times T1 and T2 with T1 < T2, the enhancement at T2 is strictly larger than at T1.

The content is monotonicity, and monotonicity has a direct physical reading. Longer orbits, which have larger dynamical times, receive a strictly larger enhancement. The theorem's own docstring spells out the consequence: the enhanced squared velocity decays strictly slower than the Newtonian 1/r law at every radius. That is the structural content of what is often called rotation curve flattening. The theorem is part of a pair; its companion result proves the enhancement diverges as the dynamical time grows without bound, so no finite radius exhausts the correction.

What the theorem does not claim is just as important as what it proves. It does not fix the asymptotic velocity value that a flattened rotation curve approaches. That value is an empirical matter, to be settled by fits to data such as the SPARC catalog, not by the theorem. The theorem also does not assert that the enhancement applies everywhere; it is proved only on the un-clamped region, the domain where the ratio Tdyn/τ0 is at least the configured threshold eps_t. Outside that region, the statement is simply not made.

In Recognition Science, this monotonicity result is one step in a larger derivation. The time-kernel itself is uniquely determined by two inputs: the recognition lag Clag = φ⁻⁵ and the fine-structure exponent α = (1 − 1/φ)/2, where φ is the golden ratio. The theorem w_t_formula_grounded proves that formula, and the monotonicity theorem builds on it. The framework's library, a machine-checked collection of formal theorems, records the proof; the declaration is the formal statement that the proof establishes.

The practical upshot for a reader is precise: within this account, the flattening of rotation curves is not an assumption but a forced consequence of the kernel's monotonicity, once the two parameters are positive. The exact shape of the curve, however, remains a question for observation, not for the theorem.

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_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 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⟩
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 theorem does not claim the enhancement applies outside the un-clamped region, where Tdyn/τ0 is below the threshold eps_t. The theorem does not claim any specific numerical value for the flattened rotation curve's asymptotic velocity.

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