kernel_dynamical_time
plain-language theorem explainer
kernel_dynamical_time supplies the explicit ILG enhancement for orbital periods, using only T_dyn, tau0, C, and alpha. Gravity modelers and causality analysts in the Recognition Science setting cite it to express stationary perturbations. The definition is a direct arithmetic expression that adds a clipped power-law term to unity.
Claim. The dynamical-time kernel equals $1 + C · (max(0.01, T_dyn / τ₀))^α$, where C, α, and τ₀ are the amplitude, self-similarity exponent, and reference tick taken from the KernelParams bundle.
background
The ILG module formalizes the kernel w(k,a) = 1 + C · (a / (k τ₀))^α with α = (1 - 1/φ)/2. KernelParams is the structure holding alpha, C, tau0 together with tau0_pos and alpha_nonneg. tau0 is the fundamental tick duration imported from Constants (both the native and Compat versions). The dynamical-time variant substitutes the local orbital period T_dyn for the scale factor a so that stationary orbits produce time-independent enhancement.
proof idea
One-line definition that directly returns the arithmetic expression 1 + P.C * (max 0.01 (T_dyn / P.tau0)) ^ P.alpha.
why it matters
Supplies the concrete expression required by CausalityBoundsCert and by the three downstream theorems kernel_dynamical_time_pos, kernel_dynamical_time_ge_one, and kernel_dynamical_time_stationary. The stationary theorem states that constant T_dyn yields constant kernel value, eliminating secular growth of acceleration. This implements the ILG kernel inside the self-similar forcing chain (T5 J-uniqueness and T6 phi fixed point) where alpha originates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.