Gravity Ilg W T Nonneg With

A nonnegativity guarantee

In the Recognition Science framework's machine-checked library of formal theorems, a ledger (a discrete record of events) is used to build models of physical processes. One such model concerns the time evolution of a system under gravity. The declaration w_t_nonneg_with proves that a particular time factor, which appears in this model, is always greater than or equal to zero.

The time factor, written as w_t, depends on a dynamic time Tdyn, a reference time τ0, and several parameters. These parameters include a coupling constant Clag and a power alpha. The theorem states that if these parameters satisfy certain basic conditions (like being non-negative), and if the reference time is not zero, then the value of w_t is never negative. This is a sanity check: a time factor that could go negative would be physically meaningless in this context.

The proof relies on a few simple facts. The time ratio is clamped to be at least a small positive number, so it is never negative or zero. Raising a positive number to any real power gives a non-negative result. Finally, the coupling constant is between zero and one, which keeps the whole expression bounded below by zero.

This lemma is a small but necessary piece of a larger structure. It does not claim that the model is correct or that it matches observations. It only establishes a basic mathematical property of one component. The library also proves that when the dynamic time equals the reference time, the factor equals one, and that the factor is unchanged if both times are scaled by the same positive amount. These are consistency properties, not physical predictions.

/-- Nonnegativity of time-kernel under ParamProps. -/
lemma w_t_nonneg_with (cfg : Config) (hcfg : ConfigProps cfg)
  (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) :
  0 ≤ w_t_with cfg P Tdyn τ0 := by
  dsimp [w_t_with]
  set t := max cfg.eps_t (Tdyn / τ0) with ht
  have ht_nonneg : 0 ≤ t := by
    have hle : cfg.eps_t ≤ t := by
      simpa [ht] using le_max_left cfg.eps_t (Tdyn / τ0)
    exact le_trans hcfg.eps_t_nonneg hle
  have hrpow_nonneg : 0 ≤ Real.rpow t P.alpha := by
    simpa using Real.rpow_nonneg ht_nonneg P.alpha
  have h_rpow_minus_one : (-1 : ℝ) ≤ Real.rpow t P.alpha - 1 := by
    linarith
  have h_mul : (-P.Clag : ℝ) ≤ P.Clag * (Real.rpow t P.alpha - 1) := by
    have h := mul_le_mul_of_nonneg_left h_rpow_minus_one H.Clag_nonneg
    -- h : P.Clag * (-1) ≤ P.Clag * (Real.rpow t P.alpha - 1)
    simpa using h
  have h_base : 0 ≤ (1 : ℝ) - P.Clag := sub_nonneg.mpr H.Clag_le_one
  have h_lower : (1 : ℝ) - P.Clag ≤ 1 + P.Clag * (Real.rpow t P.alpha - 1) := by
    linarith
  exact le_trans h_base h_lower

lemma w_t_rescale_with (cfg : Config) (P : Params) (c Tdyn τ0 : ℝ) (hc : 0 < c) :
  w_t_with cfg P (c * Tdyn) (c * τ0) = w_t_with cfg P Tdyn τ0 := by
  dsimp [w_t_with]
  have hc0 : (c : ℝ) ≠ 0 := ne_of_gt hc
  have : (c * Tdyn) / (c * τ0) = Tdyn / τ0 := by field_simp [hc0]
  simp [this]

/-- 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 claim that the model correctly predicts any measured gravitational phenomenon. The lemma does not claim that the time factor is always greater than or equal to one, only that it is non-negative. The lemma does not establish the value of any physical constant or the validity of the framework's core theorems.

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: