Gravity Ilg W T Ref With

The reference identity

A time-scaling factor is a multiplier that adjusts a quantity depending on how a dynamic time compares with a reference time. The declaration w_t_ref_with proves a baseline property of such a factor: when the dynamic time equals the reference time, the factor equals exactly one. This is a theorem in the machine-checked library of formal theorems, meaning the statement has been verified by a computer from the definitions alone.

The factor itself, written w_t_with, takes a configuration, a set of parameters, a dynamic time, and a reference time. Its formula is 1 + Clag * (t^alpha - 1), where t is the ratio of the dynamic time to the reference time, and Clag and alpha are parameters. The lemma w_t_ref_with states that when the dynamic time equals the reference time, this expression simplifies to one. The proof uses the fact that the ratio of a number to itself is one, and that the configuration's epsilon parameter is at most one, so the maximum operation in the definition picks the value one. The result holds for any nonzero reference time and any configuration satisfying the basic positivity conditions.

The identity also holds for the simplified version w_t_ref, which uses the default configuration. A related lemma shows the factor is invariant under scaling both times by the same positive constant, so only the ratio matters. Another lemma proves the factor is never negative, and a further one shows it is at least one when the dynamic time is at least the reference time. These properties together give the factor a clear meaning: it is a dimensionless modifier that equals one at the reference point and grows or shrinks as the dynamic time moves away from it.

In Recognition Science, this factor appears in the context of galaxy rotation curves, where it adjusts a baryonic velocity to account for a time-related effect. The reference identity ensures that at the reference time, the factor does not alter the velocity, providing a consistent baseline for the model. This is a definitional and computational result, not a physical law. The theorem does not assert that the factor represents a real physical effect, nor does it specify what the reference time should be. It only establishes the mathematical property of the factor at a particular point.

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

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

The theorem does not state that the time-scaling factor represents a real physical effect. The theorem does not specify how the reference time should be chosen. The theorem does not establish any connection to measured galaxy rotation curves.

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: