Gravity Ilg

Gravity ILG

Gravity ILG is a module in the Recognition Science library that supplies the parametric interfaces for connecting a galaxy's dynamical time to its observed rotation curve. It is a definitional scaffold, not a derivation of gravity itself. The module defines the shapes of the baryonic velocity contributions (gas, disk, bulge), a configuration of numerical regularization parameters, and a time kernel that rescales the dynamical time before it enters the baryonic velocity sum.

The central object is the time kernel w_t, a function of a dynamical time Tdyn and a reference time τ0. It is built from a power law in the ratio Tdyn/τ0, with a parameter Clag controlling the strength of the lag and a parameter α setting the exponent. The kernel is clamped below by a small positive epsilon so it stays well defined, and the module establishes three properties of it. First, when the dynamical time equals the reference time, the kernel is exactly 1 (the reference identity). Second, the kernel is invariant under jointly rescaling both times by the same positive factor (the rescaling law). Third, under the stated parameter conditions, the kernel is nonnegative and is at least 1 whenever the dynamical time is at least the reference time.

These three lemmas are machine-checked for the default configuration, and the module also establishes the configuration's epsilon_t lies between 0 and 1. The plain-language content is that the time kernel is a well-behaved rescaling device: it does not distort the ratio of times, it returns to unity at the reference point, and it never goes negative or below one when the dynamical time is at least the reference time. The module establishes the algebraic hygiene of the bridge, not the physical claim that this bridge is how gravity works. The physical recognition-to-linking bridge that would make this a derivation of gravity remains open.

lemma w_t_ref (P : Params) (τ0 : ℝ) (hτ : τ0 ≠ 0) : w_t P τ0 τ0 = 1 :=
  w_t_ref_with defaultConfig defaultConfig_props P τ0 hτ

lemma w_t_rescale (P : Params) (c Tdyn τ0 : ℝ) (hc : 0 < c) :
  w_t P (c * Tdyn) (c * τ0) = w_t P Tdyn τ0 :=
  w_t_rescale_with defaultConfig P c Tdyn τ0 hc

lemma w_t_nonneg (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) :
    0 ≤ w_t P Tdyn τ0 := by
  -- For defaultConfig, eps_t = 0.01 > 0.
  -- Thus t = max(0.01, Tdyn/τ0) > 0.
  -- rpow t alpha is non-negative for t > 0.
  -- Result follows from Clag <= 1.
  unfold w_t
  exact w_t_nonneg_with defaultConfig defaultConfig_props P H Tdyn τ0

/-- Time-kernel is at least 1 when alpha >= 0, Clag >= 0 and Tdyn >= tau0. -/
lemma w_t_ge_one (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) (hτ : 0 < τ0) (hT : τ0 ≤ Tdyn) :
    1 ≤ w_t P Tdyn τ0 := by
  unfold w_t w_t_with
  let t := max defaultConfig.eps_t (Tdyn / τ0)
  have h_ratio : 1 ≤ Tdyn / τ0 := (one_le_div hτ).mpr hT
  have h_base : 1 ≤ t := le_max_of_le_right h_ratio
  -- Since base >= 1 and alpha >= 0, base^alpha >= 1
  have h_pow : 1 ≤ t ^ P.alpha := Real.one_le_rpow h_base H.alpha_nonneg
  have h_diff : 0 ≤ t ^ P.alpha - 1 := sub_nonneg.mpr h_pow
  have h_mul : 0 ≤ P.Clag * (t ^ P.alpha - 1) :=
    mul_nonneg H.Clag_nonneg h_diff
  -- Goal: 1 ≤ 1 + P.Clag * (t ^ P.alpha - 1)
  -- This follows from h_mul: 0 ≤ P.Clag * (t ^ P.alpha - 1)
  simp only [ge_iff_le, le_add_iff_nonneg_right]
  exact h_mul

What this page does not claim

This module does not derive gravity from recognition principles. This module does not establish the physical recognition-to-linking bridge. This module does not fit the time kernel to any observed galaxy data.

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/ILG.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: