kernel_mono_in_a
plain-language theorem explainer
The ILG kernel increases monotonically with scale factor a for fixed positive wave number k and positive exponent alpha, once a exceeds 0.01 times k times the reference time tau0. Researchers deriving coercivity bounds or scale-dependent gravity models in the CPM framework would cite this monotonicity to control kernel growth. The proof unfolds the kernel, verifies the max operator selects the ratio term via positivity and division lemmas, then applies add_le_add_right together with Real.rpow_le_rpow on the positive base and exponent.
Claim. For a kernel parameter set with positive exponent $alpha$, positive amplitude $C$, and positive reference time $tau_0$, and for wave number $k>0$ and scale factors $a_1,a_2$ satisfying $0.01 k tau_0 leq a_1 leq a_2$, the kernel $w(k,a)=1+C(a/(k tau_0))^alpha$ obeys $w(k,a_1)leq w(k,a_2)$.
background
The ILG kernel is defined as $w(k,a)=1+C(a/(k tau_0))^alpha$ where the exponent $alpha$ equals $(1-1/phi)/2$ from the self-similar fixed point. The parameter bundle collects this exponent, the amplitude $C$, and the reference time $tau_0$ together with its positivity proof; $tau_0$ is the fundamental tick duration imported from Constants. This lemma belongs to the ILG.Kernel module, which formalizes the infra-luminous gravity kernel for CPM coercivity estimates as described in the module documentation and the referenced LaTeX derivation document.
proof idea
The tactic proof first unfolds the kernel definition. It establishes positivity of $k tau_0$ via mul_pos, shows the max equals the ratio term for both $a_1$ and $a_2$ using le_div_iff_0, max_eq_right, and div_le_div_of_nonneg_right, then rewrites. The inequality reduces to add_le_add_right followed by mul_le_mul_of_nonneg_left and Real.rpow_le_rpow, with the base comparison supplied by div_le_div_of_nonneg_right and the exponent positivity from the hypothesis.
why it matters
This monotonicity result is listed among the main results in the ILG.Kernel module documentation and supports coercivity constant derivations in CPM/LawOfExistence. It rests on the RS-derived alpha from the phi-ladder and the eight-tick octave structure. With zero current downstream uses, the lemma supplies a foundational property for future kernel bounds in scale-dependent models; it touches no open scaffolding since the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.