mode_partition_homogeneous
The theorem establishes that the ILG mode partition returns exactly the background density when the density perturbation vanishes. Cosmologists working on homogeneous backgrounds in modified gravity frameworks would cite this to confirm absence of spurious enhancement in the unperturbed sector. The proof is a one-line wrapper that rewrites the mode partition definition and applies ring simplification.
claimFor ILG kernel parameters $P$, minimum wave number $k_0$, wave number $k$, scale factor $a$, and background density $ρ_0$, the mode partition at zero perturbation satisfies mode_partition$(P, k_0, k, a, ρ_0, 0) = ρ_0$.
background
The ILG kernel takes the form $w(k,a)=1+C(a/(kτ_0))^α$ with $α=(1-1/φ)/2$, amplitude $C$, and reference tick $τ_0$. KernelParams is the structure bundling $α$, $C$, $τ_0$ together with the positivity condition $0<τ_0$ and nonnegativity of $α$. The module ILG.Kernel formalizes this kernel for galactic and cosmological applications, eliminating cumulative-time integrals in favor of dynamical time $T_dyn$. Upstream results supply the RS-native tick $τ_0=1$ and the BIT kernel families that reduce to the constant kernel when the perturbation vanishes.
proof idea
The proof is a one-line wrapper that rewrites via mode_partition_eq and then applies the ring tactic to obtain the required equality with the background density.
why it matters in Recognition Science
This result is invoked inside causalityBoundsCert to certify that perturbations remain positive and bounded while the homogeneous mode stays unmodified. It completes the homogeneous case in the ILG kernel formalization, ensuring consistency with the Recognition Science forcing chain (T5 J-uniqueness through T8 $D=3$) and the Recognition Composition Law that fixes the self-similar exponent $α$. No open scaffolding remains on this specific equality.
scope and limits
- Does not address nonzero density perturbations.
- Does not derive the explicit functional form of mode_partition.
- Does not extend to time-dependent or cumulative integrals.
- Does not claim validity outside the positivity constraints on KernelParams.
Lean usage
example (P : KernelParams) (k_min k a ρ_bar : ℝ) : mode_partition P k_min k a ρ_bar 0 = ρ_bar := mode_partition_homogeneous P k_min k a ρ_barformal statement (Lean)
378theorem mode_partition_homogeneous (P : KernelParams) (k_min k a ρ_bar : ℝ) :
379 mode_partition P k_min k a ρ_bar 0 = ρ_bar := by
proof body
Term-mode proof.
380 rw [mode_partition_eq]; ring
381
382/-! ### Dynamical-time form (no cumulative-time integration)
383
384The companion form for galactic systems is parameterized by the dynamical
385time `T_dyn` of the orbit, never by cumulative cosmic time `t`. This
386eliminates the literal Riemann–Liouville integral and resolves
387Beltracchi's concern (1).
388-/
389
390/-- The dynamical-time ILG kernel: depends only on the local orbital
391period `T_dyn`, the recognition tick `τ₀`, the lag amplitude `C`, and the
392self-similarity exponent `α`. For a stationary orbit `T_dyn` is constant,
393so the enhancement is constant, and the acceleration on an isolated mass
394does not grow in time. -/