w_t_nonneg
plain-language theorem explainer
The lemma establishes non-negativity of the time weight w_t for any Params tuple obeying ParamProps and any real Tdyn, τ0. Modelers of galactic dynamics or ILG rotation curves cite it to keep derived potentials and kernels non-negative. The proof is a one-line specialization of w_t_nonneg_with to defaultConfig and its properties, using that the effective exponent base exceeds zero and Clag is at most one.
Claim. Let $P$ be a parameter tuple with components alpha, Clag, A, r0, p, hz_over_Rd. If ParamProps($P$) holds (so $0 ≤ P.alpha$, $0 ≤ P.Clag ≤ 1$, $0 ≤ P.A$, $P.r0 > 0$, $P.p > 0$), then for all real $T_{dyn}$, $τ_0$ one has $0 ≤ w_t(P, T_{dyn}, τ_0)$.
background
In Gravity.ILG the structure Params collects the model constants alpha (fine-structure), Clag (lag factor), A (amplitude), r0 (reference radius), p (power), and hz_over_Rd. ParamProps asserts the standing inequalities alpha ≥ 0, 0 ≤ Clag ≤ 1, A ≥ 0, r0 > 0, p > 0. These conditions guarantee that the power-law term inside w_t stays non-negative once the effective time base is positive. Upstream, H from CostAlgebra supplies the shifted cost used in the broader algebra, while tau0 from Constants supplies the fundamental tick duration appearing in the ratio Tdyn/τ0.
proof idea
The proof is a one-line term wrapper. It unfolds w_t and applies w_t_nonneg_with at defaultConfig together with defaultConfig_props, threading the supplied P, H, Tdyn and τ0. The inline comment records that the default eps_t = 0.01 forces the base t > 0, so the real-power term is non-negative and the Clag ≤ 1 bound finishes the inequality.
why it matters
The result secures non-negativity of the time kernel inside the ILG gravity construction, a prerequisite for the physical consistency of the baryon curves and velocity fields that depend on w_t. It closes a small but necessary positivity step between the Recognition Composition Law (via H) and the three-dimensional gravity sector. Although currently unused downstream, it supports the claim that all derived quantities remain non-negative throughout the allowed parameter domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.