w_t_rescale_with
plain-language theorem explainer
The lemma shows that the time weight w_t_with is invariant under simultaneous positive rescaling of dynamical time Tdyn and reference time τ0. ILG gravity modelers cite it when normalizing orbital time scales in lag-corrected rotation curves. The tactic proof unfolds the definition, cancels the common factor in the ratio argument via field arithmetic, and simplifies the resulting expression.
Claim. Let $w_{t,with}(cfg,P,T_{dyn},τ_0)$ be the function returning $1 + P.Clag·(t^α - 1)$ where $t = max(cfg.eps_t, T_{dyn}/τ_0)$. Then for any Config cfg, Params P and real $c > 0$, $w_{t,with}(cfg,P,c·T_{dyn},c·τ_0) = w_{t,with}(cfg,P,T_{dyn},τ_0)$.
background
In the Gravity.ILG module, Config is the structure holding the five epsilon thresholds (including eps_t for the time floor) and Params supplies the lag parameters alpha and Clag together with the remaining ILG constants. The function w_t_with applies the lag correction only after clamping the ratio Tdyn/τ0 at the eps_t floor. Tdyn itself is imported from ParameterizationBridge as the orbital period 2πr/v for circular motion.
proof idea
The tactic proof first dsimps the definition of w_t_with, then uses field_simp on the ratio (c·Tdyn)/(c·τ0) with the hypothesis c > 0 to obtain Tdyn/τ0, and finally applies simp to finish the equality.
why it matters
The result is invoked by the downstream lemma w_t_rescale (which specializes to defaultConfig) to guarantee that the lag term in ILG gravity remains unchanged under time rescaling. This invariance is required for consistent use of the dynamical time Tdyn across different orbital radii while preserving the alpha-Clag correction structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.