w_t
plain-language theorem explainer
w_t specializes the general ILG time kernel to the default configuration parameters. Modelers of galactic rotation curves or resonance effects cite the default form when fixing eps_t at 0.01. The implementation reduces directly to the parameterized expression via substitution.
Claim. $w_t(P, T_{dyn}, τ_0) = 1 + C_{lag} (max(0.01, T_{dyn}/τ_0)^α - 1)$, where $P$ is the parameter record supplying $α$ and $C_{lag}$, and the max enforces the minimum tick threshold from defaultConfig.
background
Params records the core ILG coefficients: alpha for the power-law exponent and Clag for the lag amplitude, together with geometric scales A, r0, p and hz_over_Rd. The upstream w_t_with builds the kernel as 1 plus Clag times (t^alpha minus 1), where t is the clipped dynamical-time ratio. Tdyn supplies the orbital period 2πr/v from the parameterization bridge. This definition anchors the default behavior inside the Gravity.ILG module for downstream resonance work.
proof idea
One-line wrapper that applies w_t_with to defaultConfig, the supplied Params record, and the arguments Tdyn and τ0.
why it matters
The definition feeds eight_tick_resonance_certified and eight_tick_period, which certify the resonance reduction at the eight-tick period. It realizes the power-law time kernel described in the ILG bridge comments, connecting the dynamical timescale ratio to the T7 eight-tick octave of the forcing chain. Open questions remain on how alpha and Clag are fixed by the full Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.