CausalityBoundsCert
plain-language theorem explainer
CausalityBoundsCert packages eight verified bounds on the ILG kernel perturbation, ensuring positivity, monotonicity, and scale-factor control for causality preservation. Cosmologists and ILG modelers cite it when checking infrared and Hubble-scale regularity of w(k,a). The structure is populated directly by applying kernel positivity and boundedness lemmas from the same module.
Claim. Structure asserting eight properties of the ILG kernel $w(k,a)=1+C(a/(kτ_0))^α$: the perturbation term is positive and ≥1 for any IR cutoff and wavenumber; bounded above by its value at $k=k_{min}$ for positive scale factor; the Hubble-saturated form bounded at $k=aH$; background term identically 1; mode partition reduces to background density when density contrast vanishes; dynamical-time kernel positive and constant for stationary orbits.
background
The ILG kernel is defined as $w(k,a)=1+C(a/(kτ_0))^α$ with exponent α=(1-1/φ)/2 derived from self-similarity and amplitude C tied to coercivity slack. KernelParams bundles the triple (α,C,τ₀) together with τ₀>0 and α≥0. The module imports H from CostAlgebra, where H(x)=J(x)+1 converts the Recognition Composition Law into the d'Alembert equation H(xy)+H(x/y)=2H(x)H(y). Upstream tau0 supplies the fundamental tick duration in RS-native units.
proof idea
This is a structure definition. Its eight fields are filled by direct application of the sibling lemmas kernel_perturbation_pos, kernel_perturbation_ge_one, kernel_perturbation_bounded_above, kernel_with_Hubble_bounded_above, and the corresponding positivity and constancy statements for the dynamical-time kernel.
why it matters
The certificate is the single object consumed by causalityBoundsCert, which asserts the ILG kernel layer respects causality bounds (Beltracchi 2026 resolution). It closes the infrared and Hubble regularity requirements for the kernel that appears in the CPM coercivity constants and feeds the eight-tick octave construction. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.