Gravity Ilg W T Nonneg

The time kernel's guarantee

The time kernel, a weighting function in a model of galaxy rotation, is never negative. The declaration w_t_nonneg in the framework's machine-checked library of formal theorems proves this for the default configuration: for any allowed parameters and any dynamical time and reference time, the kernel's value is greater than or equal to zero. The proof rests on the parameter conditions that the library defines as admissible, including a non-negative coupling constant and a reference time that is positive.

The kernel itself is a definitional choice, not a derived law. It is w_t = 1 + Clag * (t^alpha - 1), where t is the larger of a small floor value and the ratio of dynamical time to reference time. The floor, set to 0.01 in the default configuration, keeps the base of the power positive, which is what makes the non-negativity argument go through. The lemma w_t_nonneg is a theorem about that chosen formula, not a statement about the physical universe.

Two companion lemmas sharpen the picture. The reference identity w_t_ref proves that when the dynamical time equals the reference time, the kernel equals exactly 1. The rescaling lemma w_t_rescale proves that multiplying both times by the same positive factor leaves the kernel unchanged, a scale invariance that the model builds in. A further lemma, w_t_ge_one, proves the kernel is at least 1 when the dynamical time is at least the reference time and the coupling is non-negative. These are all properties of the definition, checked mechanically.

What the declaration does not claim is broader. It does not assert that this kernel is the only possible time weighting, nor that the model's parameters match any measured galaxy. It does not prove that the kernel is positive for all conceivable configurations, only for those satisfying the stated parameter properties. The lemma is a piece of internal hygiene for the framework's gravity model, not an empirical prediction. Its value is that any downstream theorem that assumes a non-negative kernel can cite it without re-checking the inequality by hand.

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

@[simp] def w_t (P : Params) (Tdyn τ0 : ℝ) : ℝ := w_t_with defaultConfig P Tdyn τ0

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

What this page does not claim

The kernel is not claimed to be the unique possible time weighting. The lemma does not assert that the model's parameters match any measured galaxy. Non-negativity is proved only for configurations satisfying the stated parameter properties, not for all conceivable inputs.

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: