Gravity Ilgderivation W T Tendsto At Top

The unbounded correction

In the Recognition Science framework, the recognition cost, a forced price reality pays for each discrete event it records, leads to a correction term for orbital speeds. The term, written w_t, multiplies the Newtonian velocity to account for a recognition lag. The result named w_t_tendsto_atTop states that this correction term grows without any upper bound as the dynamical time, the time scale of an orbit, goes to infinity. In plain language: no matter how large a finite bound you pick, there is a long enough orbit time beyond which the correction exceeds that bound.

The result is conditional. It holds when the recognition lag constant is positive and when the fine-structure exponent, a parameter in the framework's cost formula, is also positive. Under those conditions, the proof in the machine-checked library of formal results shows the divergence directly from the formula for w_t. The same library also proves the correction is strictly increasing with dynamical time, so the two results together say the correction both grows and grows without limit.

What this establishes for rotation curves is structural, not numerical. Because w_t grows without bound, the enhanced squared velocity, w_t times the Newtonian v squared, decays strictly slower than the Newtonian 1/r falloff at every scale. That is the formal content of the phrase "rotation curves flatten." The result does not say how flat, at what radius, or what the terminal velocity is. Those values are an empirical matter, to be settled by fitting data such as the SPARC catalog, and the framework explicitly does not claim them as results.

The practical consequence is that the framework's correction mechanism is not a small patch that runs out. It is an unbounded effect, so no finite radius exhausts the recognition-lag correction. That is the difference between a model that tweaks rotation curves and one that forces their flattening as a structural consequence. The exact shape of the curve, however, remains a question for observation, not for a formal result.

/-- **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 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

This answer does not claim the result provides a numerical value for the flattening velocity. This answer does not claim the correction term is physically realized at all radii. This answer does not claim the framework's derivation is a complete model of galaxy dynamics.

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: