kernel_dynamical_time_ge_one
plain-language theorem explainer
The dynamical-time kernel in the ILG model satisfies a lower bound of 1 for any parameter bundle and any dynamical time. Cosmologists studying scale-dependent modifications to gravity cite this to confirm that accelerations on test particles in stationary orbits remain constant rather than growing with time. The proof unfolds the kernel expression and applies nonnegativity of the correction term followed by linear arithmetic.
Claim. For any ILG kernel parameters bundle consisting of exponent $alpha = (1-1/phi)/2$, amplitude $C geq 0$, and reference timescale $tau_0 > 0$, together with any dynamical time $T_{dyn}$, the dynamical-time kernel obeys $1 leq 1 + C cdot (max(0.01, T_{dyn}/tau_0))^{alpha}$.
background
The ILG kernel takes the form $w(k,a) = 1 + C cdot (a/(k tau_0))^{alpha}$, where $alpha = (1-1/phi)/2$ is the self-similarity exponent derived from the Recognition Science fixed point and $tau_0$ is the fundamental tick duration. KernelParams packages these values together with explicit positivity and nonnegativity hypotheses. The present theorem concerns the dynamical-time specialization that substitutes a time-dependent quantity for the scale factor while retaining the same lower bound. Upstream, tau0 is defined as the duration of one tick in RS-native units and the BIT kernel families supply the base constant, inverse, and exponential kernels used to construct the ILG variant.
proof idea
The proof unfolds the definition of the dynamical-time kernel, proves positivity of the max expression by lt_max_of_lt_left, establishes nonnegativity of the power via Real.rpow_nonneg, shows the correction term is nonnegative by mul_nonneg, and finishes with linarith.
why it matters
The result guarantees that the kernel never drops below unity, eliminating cumulative growth of gravitational effects along stationary orbits and thereby resolving the Beltracchi concern noted in the module comment. It directly supports the listed main results on kernel positivity, reduction to 1 at reference scale, and monotonicity. Within the Recognition Science framework it aligns with the J-uniqueness fixed point and the eight-tick octave by keeping the phi-derived exponent bounded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.