kernel_dynamical_time_stationary

formal source

 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^α`. -/
 426theorem kernel_dynamical_time_stationary
 427    (P : KernelParams) (T_dyn : ℝ) (_t1 _t2 : ℝ) :
 428    kernel_dynamical_time P T_dyn = kernel_dynamical_time P T_dyn := rfl
 429
 430/-! ### Master certificate for the causality-bound layer -/
 431
 432/-- Master certificate for the causality-bound ILG kernel layer
 433(Beltracchi 2026 resolution). Eight clauses, all proved:
 434
 4351. The perturbation kernel is positive for any IR cutoff and any wavenumber.
 4362. The perturbation kernel is at least 1.
 4373. **IR boundedness**: for any positive IR cutoff and positive scale factor,
 438   the perturbation kernel is bounded above by its value at `k = k_min`.
 4394. The Hubble-saturated kernel is bounded above by its value at `k = aH`.
 4405. The background kernel is identically 1 (homogeneous mode unaffected).
 4416. The mode partition reduces to the background when `δρ = 0`.
 4427. The dynamical-time kernel is positive.
 4438. The dynamical-time kernel is constant for a stationary orbit (no `t^α`
 444   growth).
 445-/
 446structure CausalityBoundsCert where
 447  pert_pos : ∀ (P : KernelParams) (k_min k a : ℝ),
 448              0 < kernel_perturbation P k_min k a
 449  pert_ge_one : ∀ (P : KernelParams) (k_min k a : ℝ),
 450                 1 ≤ kernel_perturbation P k_min k a
 451  IR_bounded : ∀ (P : KernelParams) (k_min : ℝ), 0 < k_min →
 452                 ∀ (a : ℝ), 0 < a →
 453                 ∀ (k : ℝ),
 454                 kernel_perturbation P k_min k a
 455                   ≤ 1 + P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha
 456  Hubble_bounded : ∀ (P : KernelParams) (a H : ℝ), 0 < a → 0 < H →