kernel_dynamical_time_pos
plain-language theorem explainer
The dynamical-time kernel is strictly positive for every valid ILG parameter bundle and every real dynamical time. Cosmologists using ILG models cite this to guarantee that perturbation kernels remain positive when deriving causality bounds. The proof unfolds the definition, establishes positivity of the max term and the powered correction via nonnegativity lemmas, then closes with linarith.
Claim. Let $P$ be an ILG kernel parameter bundle (exponent $α$, amplitude $C≥0$, reference timescale $τ_0>0$) and let $T_{dyn}$ be any real number. Then the dynamical-time kernel of $P$ at $T_{dyn}$ satisfies $0 < w(P,T_{dyn})$.
background
KernelParams bundles the ILG parameters: exponent $α=(1-1/φ)/2$, amplitude $C$, and reference time $τ_0>0$ with its positivity witness. The module formalizes the kernel $w(k,a)=1+C·(a/(k τ_0))^α$ where $α$ is derived from self-similarity and $C$ encodes coercivity slack. Upstream, $τ_0$ is the fundamental tick duration (defined as the tick constant in Constants and Compat.Constants) and the BIT kernel supplies the constant, inverse, and exponential families used in related constructions.
proof idea
Tactic proof. Unfold the definition of the dynamical-time kernel. Establish $0<max(0.01,T_{dyn}/τ_0)$ by lt_max_of_lt_left and norm_num. Apply Real.rpow_nonneg to obtain nonnegativity of the power term. Multiply by the nonnegativity of $C$ to get nonnegativity of the correction. Close with linarith.
why it matters
Supplies the positivity witness required by causalityBoundsCert, which assembles the full causality-bound certificate for the ILG kernel. It directly supports the module's first main result that the kernel is well-defined and positive for physical parameter ranges. The result sits inside the ILG formalization that connects to the Recognition Science forcing chain via the self-similar exponent $α$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.