w_t_ge_one
plain-language theorem explainer
The lemma shows that the ILG time kernel is bounded below by 1 when the lag coefficient and power are non-negative and dynamical time exceeds the reference scale. Galaxy rotation modelers cite the bound to keep the effective mass term positive inside fixed-point equations. The argument reduces the claim to non-negativity of a product after verifying that the base of the power is at least one.
Claim. Let $P$ be parameters with $0 ≤ α$ and $0 ≤ C_{lag}$. For $T_{dyn} ≥ τ_0 > 0$, the time kernel satisfies $1 ≤ w_t(P, T_{dyn}, τ_0)$.
background
In the ILG module the time kernel is defined via an auxiliary that returns 1 + C_lag ⋅ (t^α − 1), where t equals the maximum of a small cutoff eps_t and the ratio T_dyn/τ_0. ParamProps collects the sign conditions α ≥ 0 and C_lag ≥ 0 together with positivity of r_0 and p. Upstream CostAlgebra supplies the shifted cost H(x) = J(x) + 1 that turns the Recognition Composition Law into d'Alembert form, though the present bound uses only elementary real-power inequalities. The local setting is the construction of the ILG effective gravity law that augments Newtonian rotation curves inside the Recognition Science forcing chain.
proof idea
Unfold the definitions of the time kernel and its auxiliary. Set t to the maximum of the default cutoff and the time ratio. Apply the division lemma to obtain that the ratio is at least 1, hence t ≥ 1. Invoke the real-power inequality one_le_rpow to conclude t^α ≥ 1. Subtract one, multiply by the non-negative C_lag, and add to 1 via le_add_iff_nonneg_right.
why it matters
The bound is invoked by the rotation-velocity existence theorem in RotationILG, which applies the intermediate-value theorem to v² − w_t ⋅ K. It supplies the positivity needed for the ILG fixed-point construction that reproduces flat galactic curves while remaining inside the Recognition Science framework with its phi-ladder mass formulas and eight-tick octave. The result closes a technical gap in the gravity sector without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.