Gravity Ilgderivation Rotational Flatness Unbounded

The unbounded correction

In the standard picture of a spiral galaxy, the orbital speed of a star should drop with distance from the center, just as the planets slow down farther from the Sun. Observations show instead that speeds stay roughly constant far out. That flatness is the classic dark matter problem. The Recognition Science framework addresses it by adding a correction to Newtonian gravity, and the declaration rotational_flatness_unbounded establishes one precise property of that correction: it grows without limit as the orbital time grows.

The framework models gravity through a recognition process, a discrete record of events that carries a forced cost. From that cost comes a time kernel, a multiplier that enhances the Newtonian velocity squared. The theorem proves that for any chosen finite bound, there is a dynamical time beyond which the kernel exceeds that bound. In plain terms, no matter how large a number you pick, there is an orbit with a period long enough that the correction is bigger than your number. This is not a vague tendency; it is a formal statement in the machine-checked library of formal theorems, with the proof relying only on the kernel being strictly increasing and diverging.

The consequence is structural. Because the enhancement grows without limit, the enhanced squared velocity w(T)·v_N² decays strictly slower than the Newtonian 1/r at every scale. That slower decay is exactly the shape of a flattened rotation curve. The theorem does not say how flat, and it does not give the asymptotic velocity. Those are empirical matters, fitted to the SPARC galaxy data, not derived results.

In Recognition Science, the declaration replaces an earlier placeholder that proved nothing. The honest form is what the kernel actually forces: strict growth on the un-clamped region and divergence to infinity. The unbounded version is the direct consequence of that divergence, stated as a standalone theorem. It is a clean example of how the framework converts a physical observation, flat rotation curves, into a precise mathematical statement about a kernel.

What the declaration does not claim is as important as what it proves. It does not derive the fine-structure constant, and it does not prove the Riemann Hypothesis. It does not even predict a specific rotation curve value. It establishes only the unboundedness of the correction, leaving the exact numbers to observation.

/-- The enhancement exceeds every finite bound: for any `M` there is a
    dynamical time beyond which `w_t > M`. (Direct consequence of the
    divergence half of `rotational_flatness_forced`.) -/
theorem rotational_flatness_unbounded (P : Params) (τ0 : ℝ) (hτ : 0 < τ0)
    (hα : 0 < P.alpha) (hC : 0 < P.Clag) (M : ℝ) :
    ∃ T : ℝ, ∀ T' ≥ T, M < w_t P T' τ0 := by
  have h := (rotational_flatness_forced P τ0 hτ hα hC).2
  have hev : ∀ᶠ T' in Filter.atTop, M + 1 ≤ w_t P T' τ0 :=
    Filter.tendsto_atTop.mp h (M + 1)
  rcases Filter.eventually_atTop.mp hev with ⟨T, hT⟩
  exact ⟨T, fun T' hT' => lt_of_lt_of_le (by linarith) (hT T' hT')⟩

/-- **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 declaration does not derive the fine-structure constant alpha. The declaration does not prove the Riemann Hypothesis. The declaration does not predict a specific asymptotic rotation velocity value.

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: