w_t_ref_with
plain-language theorem explainer
The reference time-weighting identity shows that the ILG weighting function returns exactly one when dynamic time equals the reference tick τ0, provided τ0 is nonzero and the configuration satisfies the epsilon bounds. Gravity modelers cite it to anchor the normalization step in the ILG equations. The tactic proof normalizes the ratio τ0/τ0 to one, applies the eps_t ≤ 1 bound to fix the max at one, and reduces the expression directly.
Claim. Given a configuration $cfg$ whose time-epsilon bound satisfies $0 ≤ ε_t ≤ 1$, a parameter record $P$, and nonzero real $τ_0$, the weighted time function satisfies $w_t(cfg, P, τ_0, τ_0) = 1$, where $w_t$ is defined by $1 + P.Clag · (t^α - 1)$ and $t = max(ε_t, Tdyn/τ_0)$.
background
In the ILG gravity module, Config is a structure holding the time-epsilon parameter eps_t together with other bounds. ConfigProps asserts that eps_t is nonnegative and at most one. Params records the lag coefficient Clag and the exponent alpha. The weighting function w_t_with computes t as the maximum of eps_t and the normalized dynamic time Tdyn/τ0, then returns 1 + Clag · (t^α - 1). This supplies the explicit formula used by the present lemma.
proof idea
The tactic proof dsimplifies the definition of w_t_with. It applies field_simp to obtain τ0/τ0 = 1 from the nonzero hypothesis. It then uses simpa together with the eps_t_le_one fact to conclude that the max equals 1. Finally, simp reduces the whole expression to 1.
why it matters
This lemma supplies the reference case for the time-weighting factor in the ILG gravity implementation and is invoked directly by the downstream lemma w_t_ref to obtain the identity with default configuration. It anchors the normalization step in the recognition-based gravity model, consistent with the self-similar fixed point and eight-tick octave structures elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.