w_t_nonneg_with
plain-language theorem explainer
Nonnegativity of the time-kernel weight holds when the configuration satisfies eps_t nonnegative and at most one, and parameters satisfy Clag between zero and one with alpha nonnegative. ILG gravity calculations cite this result to keep dynamical weights nonnegative. The tactic proof sets t to the max of eps_t and Tdyn over tau0, then chains rpow nonnegativity with linarith and mul_le_mul_of_nonneg_left to bound the expression from below by one minus Clag.
Claim. Assume $0 ≤ ε_t ≤ 1$ and $0 ≤ α$, $0 ≤ C_{lag} ≤ 1$. Then $0 ≤ w_t(ε_t, α, C_{lag}, T_{dyn}, τ_0)$.
background
Config records small regularization parameters with eps_t controlling the time cutoff. ConfigProps requires eps_t nonnegative and bounded by one. Params collects alpha, Clag, and auxiliary constants; ParamProps adds the sign and bound constraints on alpha and Clag. The local setting is the ILG gravity module, which imports the shifted cost H(x) = J(x) + 1 from CostAlgebra and the constant Clag = phi^{-5} from Constants.ILG. Upstream, the Recognition Composition Law supplies the functional equation satisfied by H, while ArithmeticFromLogic supplies the transitivity lemma used for the eps_t bound.
proof idea
The tactic proof first simplifies the definition of the weight. It sets t to max(eps_t, Tdyn/τ0) and proves t nonnegative by le_max_left composed with eps_t_nonneg via le_trans. Real.rpow_nonneg gives the power nonnegative. Linarith produces the bound -1 ≤ rpow - 1. Multiplication by nonnegative Clag and another linarith step show the full expression is at least 1 - Clag, which is nonnegative by Clag_le_one.
why it matters
The lemma is invoked by the main w_t_nonneg statement for the default configuration. It supplies the nonnegativity step required for time kernels inside ILG gravity, consistent with the phi-ladder constants and the eight-tick structure. No open scaffolding remains; the result closes the nonnegativity obligation for this kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.