Internal source expansion for the plus case of (10.55)

The scalar expansion and its error absorption are proved here from the canonical inverse ξ, the explicit rational adjoint, and stationarity. The direct majorant constructor at the end has no expansion, remainder, or final-strict premise.

theorem Section10Equation1055SourceExpansion.psiPlus_kappaOne_hasDerivAt {c s : ℝ} (hs : 1 ≤ s) : HasDerivAt (Section10Lemma1028PlusAssembly.psiPlus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c) (Section10CanonicalXi.xi s + c - Section10Equation1053NonCircular.kappaOneLogSlope s) s

Exact derivative of the plus kernel phase for the explicit adjoint.

theorem Section10Equation1055SourceExpansion.one_div_le_xi_deriv {u : ℝ} (hu : 1 < u) : 1 / u ≤ deriv Section10CanonicalXi.xi u

The canonical derivative is at least the reciprocal derivative suggested by ξ(s) ~ log s (the error has an exact positive rational formula).

theorem Section10Equation1055SourceExpansion.xi_window_linear_lower {s t : ℝ} (hs : Real.exp 2 + 1 ≤ s) (ht : t ∈ Set.Icc (s - 1) s) : Section10CanonicalXi.xi t ≤ Section10CanonicalXi.xi s - (s - t) / s

Linear one-window lower increment for canonical ξ.

theorem Section10Equation1055SourceExpansion.two_div_lt_kappaOneLogSlope {s : ℝ} (hs : 1 ≤ s) : 2 / s < Section10Equation1053NonCircular.kappaOneLogSlope s

Explicit rational adjoint inequality needed in the plus expansion.

theorem Section10Equation1055SourceExpansion.psiPlus_secant_upper {c s t : ℝ} (hs : Real.exp 2 + 1 ≤ s) (ht : t ∈ Set.Icc (s - 1) s) : Section10Lemma1028PlusAssembly.psiPlus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c t - Section10Lemma1028PlusAssembly.psiPlus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c (s - 1) ≤ (Section10CanonicalXi.xi s + c - 2 / s) * (t - (s - 1)) - (t - (s - 1) - (t - (s - 1)) ^ 2 / 2) / s

Quadratic one-window upper expansion of the plus phase.

theorem Section10Equation1055SourceExpansion.plus_expansion_integral {A s : ℝ} (hA : A ≠ 0) (hs : s ≠ 0) : ∫ (t : ℝ) in s - 1..s, Real.exp (-A * (t - (s - 1))) * (1 + (t - (s - 1)) / (2 * s)) = (1 - Real.exp (-A)) / A + (1 - (A + 1) * Real.exp (-A)) / (2 * s * A ^ 2)

Closed form for the elementary first-order expansion integral.

theorem Section10Equation1055SourceExpansion.equation1055_internal_strict {c s : ℝ} (hc : 64 ≤ c) (hs : Real.exp 2 + 1 ≤ s) : 1 < Section10Lemma1028PlusAssembly.plusPairingScalarRatio Section10CanonicalXi.xi c s

Internalized plus (10.55): the positive first-order correction absorbs the exponential tail uniformly for every c ≥ 64 beyond one fixed cutoff.

noncomputable def Section10Equation1055SourceExpansion.section10_plus_commonMajorant_internal {R : ℝ → ℝ} {β S₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = Section10Equation1053NonCircular.explicitKappaOneAdjointPlus) (hβ : β ≤ 3) (hS : Real.exp 2 + 1 ≤ S₀) (hcompact : ∃ (B : ℝ), ∀ u ∈ Set.Icc β S₀, -Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi u ≤ B) : Section10Lemma1028PlusAssembly.Section10PlusCommonMajorant R

Direct plus majorant. Its only source-side input is boundedness on the fixed initial segment; no source structure carries expansion/remainder data.

Equations

• Section10Equation1055SourceExpansion.section10_plus_commonMajorant_internal h hadj hβ hS hcompact = { cPlus := max 64 (max 1 (Classical.choose hcompact + 1)), cutoff := S₀, one_le_cPlus := ⋯, four_le_cutoff := ⋯, envelope_slope_nonneg := ⋯ }