Equation (10.53): source-correct first-crossing reduction

This file corrects the endpoint orientation of the minus first-crossing window. It proves the pairing-to-kernel inequality with the left endpoint s-1, and records the unique earliest scalar inequality still needed for the strict (10.56) contradiction. No stationary exclusion or strict kernel bound is a record field or theorem premise.

structure Section10Equation1053KernelExpansion.MinusFirstCrossingCandidate (R ξ : ℝ → ℝ) (c : ℝ) : Type

The exact data supplied by a source-correct minus first crossing. For a decreasing preceding history the window maximum is at s-1, not at s.

• s : ℝ
• stationary : Section10Lemma1028FirstCrossing.normalizedMinusBase R ξ self.s = c
• window_upper (t : ℝ) : t ∈ Set.Icc (self.s - 1) self.s → Section10Equation1053.envelopeMinus R ξ c t ≤ Section10Equation1053.envelopeMinus R ξ c (self.s - 1)

theorem Section10Equation1053KernelExpansion.explicit_adjoint_window_pos {s t : ℝ} (hs : 2 ≤ s) (ht : t ∈ Set.Icc (s - 1) s) : 0 < Section10Equation1053NonCircular.explicitKappaOneAdjointPlus (t + 1)

Explicit κ=1 adjoint positivity on the complete shifted unit window.

theorem Section10Equation1053KernelExpansion.pairing_le_leftEndpoint_kernel {R ξ : ℝ → ℝ} {β c : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = Section10Equation1053NonCircular.explicitKappaOneAdjointPlus) (w : MinusFirstCrossingCandidate R ξ c) (hβs : β < w.s) (hs2 : 2 ≤ w.s) (hprodInt : IntervalIntegrable (fun (t : ℝ) => Section10Equation1053.envelopeMinus R ξ c t * Real.exp (-Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)) MeasureTheory.volume (w.s - 1) w.s) (hkernelInt : IntervalIntegrable (fun (t : ℝ) => Real.exp (-Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)) MeasureTheory.volume (w.s - 1) w.s) : w.s * Section10Equation1053NonCircular.explicitKappaOneAdjointPlus w.s * R w.s ≤ Section10Equation1053.envelopeMinus R ξ c (w.s - 1) * ∫ (t : ℝ) in w.s - 1..w.s, Real.exp (-Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)

Source-correct normalized pairing step preceding (10.56). Notice the factor W₋(s-1) on the right.

noncomputable def Section10Equation1053KernelExpansion.equation1056ScalarRatio (ξ : ℝ → ℝ) (c s : ℝ) : ℝ

The exact scalar ratio occurring after the source-correct pairing step. At stationarity its prefactor is the (10.45) quantity A = ξ(s)-c-2/s; proving this ratio < 1 is precisely the first unresolved scalar inequality. It is declared as an object, not assumed by any record.

Equations

• Section10Equation1053KernelExpansion.equation1056ScalarRatio ξ c s = ((ξ s - c - 2 / s) * ∫ (t : ℝ) in s - 1..s, Real.exp (-Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c t)) / Real.exp (-Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus ξ c (s - 1))

def Section10Equation1053KernelExpansion.Equation1053EarliestScalarInequality (ξ : ℝ → ℝ) (c s : ℝ) : Prop

Unique earliest scalar frontier left by the source audit. A complete internalization of (10.47)--(10.53) must prove this at a sufficiently large explicit c and cutoff, from canonical ξ bounds and the explicit rational adjoint estimates.

Equations

• Section10Equation1053KernelExpansion.Equation1053EarliestScalarInequality ξ c s = (Section10Equation1053KernelExpansion.equation1056ScalarRatio ξ c s < 1)

theorem Section10Equation1053KernelExpansion.explicit_adjoint_1041 {s : ℝ} (hs : 2 ≤ s) : |Section10Equation1053NonCircular.kappaOneLogSlope s - 2 / s| ≤ 2 / s ^ 3

The explicit adjoint input to (10.47) is already internal: its shifted logarithmic slope differs from 2/s by at most 2/s³.

theorem Section10Equation1053KernelExpansion.explicit_adjoint_1042 {s : ℝ} (hs : 2 ≤ s) : |-4 * (2 * s ^ 2 + 1) / (2 * s ^ 2 - 1) ^ 2 + 2 / s ^ 2| ≤ 4 / s ^ 4

Likewise the differentiated rational bound used in (10.51).