Gravity Ilg W T Rescale With

The time-kernel rescaling

The declaration w_t_rescale_with establishes a scale-invariance property for a time kernel, a function that maps two durations to a number. The property says that multiplying both durations by the same positive factor leaves the output unchanged: w_t(c*Tdyn, c*tau0) = w_t(Tdyn, tau0) for any positive c. In plain terms, only the ratio Tdyn/tau0 matters, not the absolute size of either duration. This is a theorem in the framework's machine-checked library of formal theorems, proved in the file IndisputableMonolith/Gravity/ILG.lean.

The time kernel itself is a definitional choice within the framework. It models a multiplicative correction factor applied to a dynamical timescale Tdyn relative to a reference timescale tau0. The kernel is built from a parameter alpha and a coefficient Clag, and it is constructed so that when the two timescales are equal, the kernel equals 1. The rescaling lemma then shows that this construction is invariant under a common scaling of both timescales, a property that holds for any positive scaling factor c.

What the declaration does not claim is also precise. It does not assert that the time kernel is the unique function with this rescaling property; many functions depend only on a ratio. It does not claim that the kernel's specific form, with its parameters alpha and Clag, is forced by the framework's foundational theorems. The parameters remain configurable, and the lemma holds for any real values of alpha and Clag, subject only to the positivity of the scaling factor. The rescaling property is a structural fact about the chosen definition, not a derivation of that definition from deeper principles.

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]

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τ

What this page does not claim

The time kernel is the unique function with the rescaling property. The specific form of the time kernel is derived from the framework's foundational theorems. The parameters alpha and Clag are fixed by the framework rather than configurable.

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: