kernel_dynamical_time_ge_one
plain-language theorem explainer
The dynamical-time kernel satisfies kernel_dynamical_time P T_dyn ≥ 1 for every KernelParams bundle P and real T_dyn. Cosmologists checking positivity of infra-luminous gravity corrections in stationary orbits cite the bound to confirm the effective kernel never falls below its reference value. The argument unfolds the definition, proves the argument of the power is positive, establishes non-negativity of the correction term, and closes with linarith.
Claim. Let P be a KernelParams structure with exponent α, amplitude C ≥ 0 and reference scale τ₀ > 0. For any real dynamical time T_dyn the dynamical-time kernel obeys 1 ≤ 1 + C ⋅ (max(0.01, T_dyn / τ₀))^α.
background
The ILG kernel is defined in the module as w(k, a) = 1 + C ⋅ (a / (k τ₀))^α with α = (1 − 1/φ)/2. KernelParams bundles the three numeric fields α, C, τ₀ together with the positivity hypotheses tau0_pos : 0 < tau0 and C_nonneg : 0 ≤ C. Upstream, tau0 is supplied by IndisputableMonolith.Constants.tau0 as the fundamental tick duration and by the Derivation module as sqrt(hbar_codata G_codata / (π c_codata³)) / c_codata; alpha is the fine-structure constant 1/alphaInv.
proof idea
The tactic proof unfolds kernel_dynamical_time, applies lt_max_of_lt_left and norm_num to obtain 0 < max 0.01 (T_dyn / P.tau0), invokes Real.rpow_nonneg to obtain non-negativity of the powered term, uses mul_nonneg on P.C_nonneg and the power, then finishes with linarith.
why it matters
The bound guarantees the kernel remains at least unity, which directly supports the module comment that a stationary orbit produces no cumulative-time growth and thereby resolves Beltracchi's concern (1). It sits inside the ILG kernel formalization that connects to the CPM coercivity constants and the self-similar exponent derived from the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.