kernel_dynamical_time
The dynamical-time ILG kernel supplies the explicit enhancement factor 1 + C times a power-law term in normalized orbital period. Researchers proving causality bounds and stationarity in the ILG layer cite this definition to control time dependence of gravitational acceleration. The definition is a direct algebraic expression using the amplitude C, exponent alpha, and reference tick tau0 from the parameter bundle.
claimThe dynamical-time kernel is defined by $1 + C (max(0.01, T_{dyn}/τ_0))^α$, where $C$, $α$, and $τ_0$ are the lag amplitude, self-similarity exponent, and reference tick duration taken from the ILG parameter bundle.
background
The module formalizes the ILG kernel as $w(k,a)=1+C·(a/(k τ_0))^α$ with $α=(1-1/φ)/2$. KernelParams is the structure holding alpha, C, and tau0 together with the constraint tau0>0. Upstream, tau0 is the fundamental tick duration imported from Constants, while alpha is taken from the Alpha module derivation.
proof idea
One-line definition that directly encodes the expression 1 + P.C * (max 0.01 (T_dyn / P.tau0))^P.alpha using field projection from KernelParams.
why it matters in Recognition Science
The definition is the explicit form required by the master CausalityBoundsCert and by the stationarity theorem kernel_dynamical_time_stationary, which shows the kernel is constant for fixed T_dyn and thereby eliminates secular growth of acceleration on stable orbits. It implements the ILG model inside the Recognition Science framework, where alpha originates from the phi self-similarity fixed point in the T5-T6 forcing chain.
scope and limits
- Does not prove positivity or lower bounds on the kernel.
- Does not incorporate wavenumber or scale-factor dependence of the general ILG form.
- Does not supply numerical values or CODATA matching for C or alpha.
- Does not treat time-varying dynamical periods.
formal statement (Lean)
395noncomputable def kernel_dynamical_time (P : KernelParams) (T_dyn : ℝ) : ℝ :=
proof body
Definition body.
396 1 + P.C * (max 0.01 (T_dyn / P.tau0)) ^ P.alpha
397
398/-- The dynamical-time kernel is positive. -/