Gravity Ilg Eps T Le One Default

A small bound with a job

The declaration eps_t_le_one_default is a small, machine-checked proof about a number called eps_t. In the default configuration of the framework's galaxy model, eps_t is set to 0.01. The proof establishes that this value is less than or equal to 1. It is a simple fact, but it is a necessary one: the model's time kernel, a function that adjusts a galaxy's rotation curve based on a dynamical time scale, relies on this bound to behave correctly.

The time kernel is defined in the model as w_t_with. It takes a ratio of a dynamical time Tdyn to a reference time τ0, and it uses eps_t as a floor for that ratio. The floor prevents the kernel from becoming singular or ill-defined when the ratio is very small. The bound eps_t ≤ 1 is what allows the kernel to return exactly 1 when the dynamical time equals the reference time, a property proved separately as w_t_ref_with. Without the bound, that identity could fail, and the model's behavior at the reference time would be inconsistent.

The lemma is not a physical law. It does not state that any real galaxy must have a time ratio below one. It is a constraint on a parameter of a specific computational model, chosen by the framework's authors to ensure numerical stability. The proof itself is trivial, a direct computation from the definition of defaultConfig. Its role is to certify that the chosen default value satisfies the model's own requirements, making the model self-consistent.

In the broader context of the framework, this lemma is a small but load-bearing part of a larger structure. It is one of several properties that a configuration must satisfy, alongside non-negativity of eps_t and other parameters. The framework proves these properties for its default configuration, so that any theorem that assumes a valid configuration can be applied to the default one. This is how the framework builds a chain of reasoning: each small, verified step supports the next.

@[simp] def defaultConfig : Config :=
  { upsilonStar := 1.0
  , eps_r := 1e-12
  , eps_v := 1e-12
  , eps_t := 0.01
  , eps_a := 1e-12 }

lemma eps_t_le_one_default : defaultConfig.eps_t ≤ (1 : ℝ) := by
  norm_num

/-- Reference identity under nonzero tick: w_t(τ0, τ0) = 1. -/
lemma w_t_ref_with (cfg : Config) (hcfg : ConfigProps cfg)
  (P : Params) (τ0 : ℝ) (hτ : τ0 ≠ 0) : w_t_with cfg P τ0 τ0 = 1 := by
  dsimp [w_t_with]
  have hdiv : τ0 / τ0 = (1 : ℝ) := by
    field_simp [hτ]
  have hmax : max cfg.eps_t (τ0 / τ0) = (1 : ℝ) := by
    simpa [hdiv, max_eq_right hcfg.eps_t_le_one]
  simp [hmax]

What this page does not claim

The lemma does not state a physical bound on real galaxy time scales. It does not prove that the default configuration is the only valid one. It does not establish that the galaxy model itself is correct or matches observations.

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: