kernel_dynamical_time_pos
The theorem establishes positivity of the dynamical-time kernel 1 + C ⋅ (max(0.01, T_dyn / τ₀))^α for any valid ILG parameter bundle and real dynamical time. Cosmologists deriving perturbation bounds or causality certificates in infra-luminous gravity models would cite this result. The proof is a short tactic sequence that unfolds the definition, applies nonnegativity of the maximum and real powers, and closes with linarith.
claimFor any kernel parameter bundle with exponent α, amplitude C ≥ 0, and reference time τ₀ > 0, and for any real dynamical time T_dyn, the expression 1 + C ⋅ (max(0.01, T_dyn / τ₀))^α is strictly positive.
background
The ILG kernel module formalizes w(k, a) = 1 + C ⋅ (a / (k τ₀))^α with α = (1 - 1/φ)/2 drawn from self-similarity. KernelParams is the structure bundling α, C, τ₀ > 0, and the nonnegativity proof for C. Upstream results supply the fundamental tick duration τ₀ from Constants and the BIT kernel families for related definitions.
proof idea
The proof unfolds the kernel definition, proves the inner maximum exceeds 0.01 via lt_max_of_lt_left, obtains nonnegativity of the real power via rpow_nonneg, shows the product with C is nonnegative via mul_nonneg using the stored C_nonneg field, and concludes with linarith.
why it matters in Recognition Science
This result supplies the pert_pos field inside the causalityBoundsCert definition. It fills the basic well-definedness step for the ILG kernel before monotonicity and boundedness lemmas, consistent with the Recognition Science forcing chain that fixes D = 3 and the eight-tick octave through the J-uniqueness and phi fixed-point steps.
scope and limits
- Does not apply when amplitude C is negative.
- Does not apply when reference time τ₀ is nonpositive.
- Does not address kernels outside the stated ILG parametrization.
- Does not derive explicit numerical lower bounds beyond strict positivity.
Lean usage
example (P : KernelParams) (T_dyn : ℝ) : 0 < kernel_dynamical_time P T_dyn := kernel_dynamical_time_pos P T_dynformal statement (Lean)
399theorem kernel_dynamical_time_pos (P : KernelParams) (T_dyn : ℝ) :
400 0 < kernel_dynamical_time P T_dyn := by
proof body
Tactic-mode proof.
401 unfold kernel_dynamical_time
402 have hmax_pos : 0 < max 0.01 (T_dyn / P.tau0) := by
403 apply lt_max_of_lt_left; norm_num
404 have hpow_nonneg : 0 ≤ (max 0.01 (T_dyn / P.tau0)) ^ P.alpha :=
405 Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
406 have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (T_dyn / P.tau0)) ^ P.alpha :=
407 mul_nonneg P.C_nonneg hpow_nonneg
408 linarith
409
410/-- The dynamical-time kernel is at least 1. -/