kernel_dynamical_time_ge_one
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not claim equality to 1 except when the correction term vanishes.
- Does not treat time-dependent evolution of the kernel itself.
- Does not incorporate explicit wave number or spatial dimension into the bound.
- Does not supply numerical values or matching to observational data.
formal statement (Lean)
411theorem kernel_dynamical_time_ge_one (P : KernelParams) (T_dyn : ℝ) :
412 1 ≤ kernel_dynamical_time P T_dyn := by
proof body
Tactic-mode proof.
413 unfold kernel_dynamical_time
414 have hmax_pos : 0 < max 0.01 (T_dyn / P.tau0) := by
415 apply lt_max_of_lt_left; norm_num
416 have hpow_nonneg : 0 ≤ (max 0.01 (T_dyn / P.tau0)) ^ P.alpha :=
417 Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
418 have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (T_dyn / P.tau0)) ^ P.alpha :=
419 mul_nonneg P.C_nonneg hpow_nonneg
420 linarith
421
422/-- **No cumulative-time growth.** For a stationary orbit `T_dyn(t) = T_dyn`
423constant in time `t`, the dynamical-time kernel is constant in time. This
424resolves Beltracchi's concern (1): the gravitational acceleration on a
425test particle in a stable orbit does not grow as `t^α`. -/