Equation (10.56): eventual strict scalar absorption

theorem Section10Equation1056ScalarAbsorption.kappaOneLogSlope_antitoneOn : AntitoneOn Section10Equation1053NonCircular.kappaOneLogSlope (Set.Ici 2)

theorem Section10Equation1056ScalarAbsorption.psiMinus_kappaOne_hasDerivAt_local {c s : ℝ} (hs : 1 ≤ s) : HasDerivAt (Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c) (Section10CanonicalXi.xi s - c - Section10Equation1053NonCircular.kappaOneLogSlope s) s

theorem Section10Equation1056ScalarAbsorption.psiMinus_secant_lower {c s t : ℝ} (hs : 3 ≤ s) (ht : t ∈ Set.Icc (s - 1) s) : (Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)) * (t - (s - 1)) ≤ Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c t - Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c (s - 1)

theorem Section10Equation1056ScalarAbsorption.normalized_kernel_le {c s : ℝ} (hs : 3 ≤ s) (hm : 0 < Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)) : (∫ (t : ℝ) in s - 1..s, Real.exp (-Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c t)) / Real.exp (-Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c (s - 1)) ≤ (1 - Real.exp (-(Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)))) / (Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1))

theorem Section10Equation1056ScalarAbsorption.scalar_absorption_of_elementary_bounds {c s : ℝ} (hs : 3 ≤ s) (hm : 0 < Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)) (hA : 0 < Section10CanonicalXi.xi s - c - 2 / s) (hgap : Section10CanonicalXi.xi s - c - 2 / s - (Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)) < (Section10CanonicalXi.xi s - c - 2 / s) * Real.exp (-(Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)))) : Section10Equation1053KernelExpansion.Equation1053EarliestScalarInequality Section10CanonicalXi.xi c s

theorem Section10Equation1056ScalarAbsorption.xi_nonneg (s : ℝ) : 0 ≤ Section10CanonicalXi.xi s

theorem Section10Equation1056ScalarAbsorption.xi_tendsto_atTop_local : Filter.Tendsto Section10CanonicalXi.xi Filter.atTop Filter.atTop

theorem Section10Equation1056ScalarAbsorption.xi_unit_increment_le {s : ℝ} (hs : 4 ≤ s) (hx : 2 ≤ Section10CanonicalXi.xi (s - 1)) : Section10CanonicalXi.xi s - Section10CanonicalXi.xi (s - 1) ≤ 2 / (s - 1)

theorem Section10Equation1056ScalarAbsorption.kappaOneLogSlope_nonneg {u : ℝ} (hu : 2 ≤ u) : 0 ≤ Section10Equation1053NonCircular.kappaOneLogSlope u

theorem Section10Equation1056ScalarAbsorption.kappaOneLogSlope_le_three_div {u : ℝ} (hu : 2 ≤ u) : Section10Equation1053NonCircular.kappaOneLogSlope u ≤ 3 / u

theorem Section10Equation1056ScalarAbsorption.eventual_elementary_absorption (c : ℝ) (hc : 1152 ≤ c) : ∃ (S : ℝ), ∀ (s : ℝ), S ≤ s → 3 ≤ s ∧ 0 < Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1) ∧ 0 < Section10CanonicalXi.xi s - c - 2 / s ∧ Section10CanonicalXi.xi s - c - 2 / s - (Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)) < (Section10CanonicalXi.xi s - c - 2 / s) * Real.exp (-(Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)))

theorem Section10Equation1056ScalarAbsorption.equation1056_eventually_strict (c : ℝ) (hc : 1152 ≤ c) : ∃ (S : ℝ), ∀ (s : ℝ), S ≤ s → Section10Equation1053KernelExpansion.Equation1053EarliestScalarInequality Section10CanonicalXi.xi c s

Final source-(10.56) scalar absorption: for every fixed c ≥ 1152, the canonical ξ makes the normalized scalar product strictly less than one for all sufficiently large s.

theorem Section10Equation1056ScalarAbsorption.equation1056_eventually_contradiction (c : ℝ) (hc : 1152 ≤ c) : ∃ (S : ℝ), ∀ (s : ℝ), S ≤ s → 1 ≤ Section10Equation1053KernelExpansion.equation1056ScalarRatio Section10CanonicalXi.xi c s → False

The literal final contradiction in (10.56): the source-side lower bound 1 ≤ ratio is incompatible with the eventual strict absorption.