w_t_with
plain-language theorem explainer
w_t_with defines the time-kernel for the ILG correction as one plus Clag times the excess of the clamped dynamical-time ratio raised to alpha. Galaxy-dynamics modelers in Recognition Science cite it when parameterizing the transition from Newtonian to modified regimes via Tdyn relative to reference tau0. The definition is a direct algebraic substitution of the maximum function and real exponentiation.
Claim. Let $w_{t,with}(cfg,P,T_{dyn},τ_0)=1+P.Clag⋅(max(cfg.ε_t,T_{dyn}/τ_0)^{P.α}-1)$, where $cfg$ is the Config record supplying the time floor ε_t and $P$ is the Params record supplying the exponent α together with the coefficient Clag.
background
The Gravity.ILG module augments Newtonian gravity with a time-dependent correction whose amplitude is set by the lag coefficient Clag. Config is the structure holding small positive tolerances including eps_t; Params collects alpha (the fine-structure constant), Clag (defined as phi^{-5}), and auxiliary scaling constants. Upstream Tdyn computes the orbital period 2πr/v, supplying the dynamical timescale that is compared with τ0 in the ParameterizationBridge.
proof idea
This is a direct definition. It computes the clamped ratio t as max(cfg.eps_t, Tdyn/τ0), then returns 1 plus P.Clag multiplied by (t raised to the power P.alpha minus 1) via Real.rpow.
why it matters
w_t_with is the core implementation invoked by the simplified w_t and w_t_display (which fix defaultConfig) and underpins the lemmas w_t_ge_one, w_t_nonneg_with, w_t_ref_with and w_t_rescale_with. It supplies the concrete time dependence required for the grounded formula in ILGDerivation and the rotation-solution existence result. In the Recognition framework it encodes the T7 eight-tick octave through the normalized time ratio and fixes the correction amplitude via Clag=phi^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.