w_t_ref
plain-language theorem explainer
The lemma establishes that the ILG time-weight function returns exactly 1 when its dynamic and reference times coincide at a nonzero value. Gravity modelers in the Recognition Science framework invoke this normalization to fix the reference epoch in dynamical weight calculations. The argument is a direct one-line specialization of the general reference identity to the default configuration.
Claim. For any ILG parameter tuple $P$ and nonzero real number $τ_0$, the time-weight function satisfies $w_t(P, τ_0, τ_0) = 1$.
background
The structure Params assembles the ILG constants alpha, Clag, A, r0, p, and hz_over_Rd that enter the weight definitions. The function w_t is obtained by fixing the general weight constructor w_t_with to the default configuration, whose properties are verified by a separate lemma that sets the epsilon tolerances to their nominal small values. The upstream reference identity states that w_t(τ0, τ0) = 1 under nonzero tick and configuration properties; the present lemma instantiates that identity for the default case.
proof idea
The proof is a one-line wrapper that applies the general reference identity w_t_ref_with to the default configuration, its verified properties, the supplied parameter tuple, and the nonzero condition on τ0.
why it matters
This identity supplies the normalization anchor for the time-weight function inside ILG gravity models. It closes the reference case for the default parameter set, allowing downstream calculations to treat the reference epoch as having unit weight. The result supports consistency checks within the ILG module but does not directly engage the T0-T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.