causalityBoundsCert
plain-language theorem explainer
The causalityBoundsCert definition constructs an instance of the master CausalityBoundsCert structure for the ILG kernel by assembling its eight clauses from positivity, boundedness, background equality, and stationarity lemmas. Researchers formalizing Infra-Luminous Gravity or citing the Beltracchi 2026 resolution would reference it to confirm the perturbation respects causality and produces no cumulative growth. The construction is a direct record builder that references the supporting kernel results without further derivation.
Claim. Let $w(k,a)=1+C(a/(kτ_0))^α$ be the ILG kernel with $α=(1-1/φ)/2$. The structure CausalityBoundsCert is inhabited by the clauses: perturbation positive and ≥1 for any KernelParams, IR-bounded above by its value at $k=k_{min}$, Hubble-saturated kernel bounded at $k=aH$, background identically 1, mode partitions homogeneous, dynamical-time kernel positive, and stationary (no cumulative growth).
background
The ILG.Kernel module formalizes the perturbation kernel $w(k,a)=1+C·(a/(kτ_0))^α$ with α derived from self-similarity. The CausalityBoundsCert structure collects the eight properties required for the causality-bound layer: positivity and lower bound of the perturbation term, IR boundedness (kernel ≤ value at cutoff for k_min>0, a>0), Hubble boundedness, background equality to 1, homogeneous partitions, positive dynamical time, and no cumulative growth under stationary orbits.
proof idea
This is a definition that builds the CausalityBoundsCert record by direct field assignment: pert_pos to kernel_perturbation_pos, pert_ge_one to kernel_perturbation_ge_one, IR_bounded to a lambda wrapping kernel_perturbation_bounded_above, Hubble_bounded to kernel_with_Hubble_bounded_above, background_eq_one to kernel_background_eq_one, partition_homogeneous to mode_partition_homogeneous, dyn_pos to kernel_dynamical_time_pos, and no_cumulative_growth to kernel_dynamical_time_stationary.
why it matters
This definition inhabits the master certificate for the causality-bound ILG kernel layer (Beltracchi 2026 resolution) as stated in the module documentation. It assembles the kernel properties that confirm causality constraints and resolve stationarity concerns for stable orbits. It completes the ILG formalization in this module, aligning with the Recognition Composition Law through the J-cost minimum on the homogeneous background, though no downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.