theorem
proved
term proof
kernel_dynamical_time_stationary
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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-/