Gravity Ilg W T Ge One

The time-kernel bound

The declaration w_t_ge_one is a proved lemma inside a machine-checked library of formal theorems. It concerns a specific function, the time-kernel, which in this framework models how a dynamic time interval compares to a fixed reference scale. The function takes two inputs: a dynamic time Tdyn and a reference time τ0. The lemma states that when the dynamic time is at least as large as the reference time, and both are positive, the value of the time-kernel is at least 1. In plainer terms, if the measured interval is not shorter than the reference, the kernel does not dip below its baseline value of 1.

The proof of this lemma is not a physical measurement or a postulate. It is a formal derivation from the definitions of the function and its parameters. The function itself is defined with a few adjustable constants, such as a coupling strength Clag and an exponent alpha. The lemma holds under a set of explicit conditions on these parameters: they must be non-negative, and the coupling strength must be at most 1. These conditions are part of the statement, not hidden assumptions. The result is a mathematical fact about the defined function, verified step by step in the library's logic.

In Recognition Science, this lemma is a small piece of a larger structure. It is a property of the time-kernel that the framework proves, not one it assumes. The lemma also shows a scaling property: multiplying both the dynamic and reference times by the same positive factor leaves the kernel unchanged. This means the function depends only on the ratio of the two times, not on their absolute size. These are formal properties of a model, and they are true within the model's definitions.

What the lemma does not claim is just as important. It does not state that this time-kernel is the correct description of any real physical system. It does not assert that the parameters have measured values, or that the function matches galactic rotation data. The lemma is a theorem about a definition, not a law of nature. It is a piece of the framework's internal mathematics, and its truth is conditional on the model's chosen form. The framework's library proves this bound, but it does not, from this lemma alone, claim to explain gravity.

/-- 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

/-- 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

structure ParamProps (P : Params) : Prop where
  alpha_nonneg : 0 ≤ P.alpha
  Clag_nonneg  : 0 ≤ P.Clag
  Clag_le_one  : P.Clag ≤ 1
  A_nonneg     : 0 ≤ P.A
  r0_pos       : 0 < P.r0
  p_pos        : 0 < P.p

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 lemma does not claim the time-kernel is a correct physical model. No measured values for the model's parameters are asserted. The lemma alone does not constitute a derivation of gravitational phenomena.

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: