Uniform stationary exclusion and non-circular minus-parameter selection

The key input from source Lemma 10.27 is kept as an adjacent-value comparison, not as the desired scalar inequality. Division by the positive s * R s and the stationary equation give (10.46), namely ξ(s)-c-2/s = R(s-1)/(sR(s)) ≥ 1-K/s. Consequently the cutoff below depends on the comparison constants (and hence on R) but not on c.

structure Section10Equation1056UniformStationary.Lemma1027AdjointRComparison (R : ℝ → ℝ) : Type

Source Lemma 10.27 in the precise comparison form used here. The adjoint argument in the source produces this estimate for R; no scalar kernel bound, stationary exclusion, or conclusion of (10.56) is stored in this packet.

• K : ℝ
• cutoff : ℝ
• K_nonneg : 0 ≤ self.K
• comparison (s : ℝ) : self.cutoff ≤ s → (1 - self.K / s) * (s * R s) ≤ R (s - 1)

structure Section10Equation1056UniformStationary.QhatMinusMajorant (R : ℝ → ℝ) : Type

The cutoff-aware minus majorant produced after the single compact choice. This is the same six-field contract consumed by the cutoff-corrected Section-13 ratio argument.

• cMinus : ℝ
• cutoff : ℝ
• A : ℝ
• four_le_cutoff : 4 ≤ self.cutoff
• one_le_A : 1 ≤ self.A
• majorizes_log (s : ℝ) : self.cutoff ≤ s → 1 / self.A * Real.log (Real.exp 1 * s) ≤ Section10CanonicalXi.xi s - self.cMinus - 2 / s
• envelope_slope_nonpos (s : ℝ) : self.cutoff ≤ s → -R (s - 1) + s * (Section10CanonicalXi.xi s - self.cMinus - 2 / s) * R s ≤ 0

noncomputable def Section10Equation1056UniformStationary.stationaryCutoff {R : ℝ → ℝ} (h27 : Lemma1027AdjointRComparison R) : ℝ

A fixed cutoff depending only on the Lemma-10.27 comparison constants.

Equations

• Section10Equation1056UniformStationary.stationaryCutoff h27 = max h27.cutoff (max (2 * h27.K + 2) (Real.exp 2 + 21))

theorem Section10Equation1056UniformStationary.stationaryCutoff_ge_comparison {R : ℝ → ℝ} (h27 : Lemma1027AdjointRComparison R) : h27.cutoff ≤ stationaryCutoff h27

theorem Section10Equation1056UniformStationary.stationaryCutoff_ge_K {R : ℝ → ℝ} (h27 : Lemma1027AdjointRComparison R) : 2 * h27.K + 2 ≤ stationaryCutoff h27

theorem Section10Equation1056UniformStationary.stationaryCutoff_ge_numeric {R : ℝ → ℝ} (h27 : Lemma1027AdjointRComparison R) : Real.exp 2 + 21 ≤ stationaryCutoff h27

theorem Section10Equation1056UniformStationary.equation1046_of_stationary_and_comparison {R : ℝ → ℝ} {β c s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hβ : β ≤ 3) (h27 : Lemma1027AdjointRComparison R) (hs : stationaryCutoff h27 ≤ s) (hstat : Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi s = c) : 1 - h27.K / s ≤ Section10CanonicalXi.xi s - c - 2 / s

The literal (10.46) bridge: stationary equality plus the source's adjacent-value comparison.

theorem Section10Equation1056UniformStationary.stationary_prefactor_ge_half {R : ℝ → ℝ} {β c s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hβ : β ≤ 3) (h27 : Lemma1027AdjointRComparison R) (hs : stationaryCutoff h27 ≤ s) (hstat : Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi s = c) : 1 / 2 ≤ Section10CanonicalXi.xi s - c - 2 / s

theorem Section10Equation1056UniformStationary.exp_parameter_dominates (c : ℝ) (hc : 1152 ≤ c) : 20 * c + 40 < Real.exp c

theorem Section10Equation1056UniformStationary.scalarRatio_lt_one_of_stationary {R : ℝ → ℝ} {β c s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hβ : β ≤ 3) (h27 : Lemma1027AdjointRComparison R) (hc : 1152 ≤ c) (hs : stationaryCutoff h27 ≤ s) (hstat : Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi s = c) : Section10Equation1053KernelExpansion.Equation1053EarliestScalarInequality Section10CanonicalXi.xi c s

Uniform form of the strict scalar estimate. Its cutoff is independent of c; the only source-side premise is (10.46)'s adjacent-value comparison.

theorem Section10Equation1056UniformStationary.minusFirstCrossing_scalarRatio_ge_one_local {R : ℝ → ℝ} {β c s₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = Section10Equation1053NonCircular.explicitKappaOneAdjointPlus) (w : Section10Equation1053MinusFirstCrossing.MinusFirstCrossing R Section10CanonicalXi.xi c β s₀) : 1 ≤ Section10Equation1053KernelExpansion.equation1056ScalarRatio Section10CanonicalXi.xi c w.s

The pairing comparison gives the opposite half of (10.56) at a genuine first crossing. This is derived here (rather than imported from the older assembly) with the shifted adjoint positivity rewritten explicitly.

theorem Section10Equation1056UniformStationary.no_uniform_minusFirstCrossing {R : ℝ → ℝ} {β c s₀ : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = Section10Equation1053NonCircular.explicitKappaOneAdjointPlus) (h27 : Lemma1027AdjointRComparison R) (hβ : β ≤ 3) (hc : 1152 ≤ c) (w : Section10Equation1053MinusFirstCrossing.MinusFirstCrossing R Section10CanonicalXi.xi c β s₀) (hs : stationaryCutoff h27 ≤ w.s) : False

No genuine stationary first-crossing candidate survives past the fixed R-dependent cutoff, simultaneously for every c ≥ 1152.

theorem Section10Equation1056UniformStationary.canonical_eventual_log_lower_local (c : ℝ) : ∃ (T : ℝ), ∀ (s : ℝ), T ≤ s → 1 / 2 * Real.log (Real.exp 1 * s) ≤ Section10CanonicalXi.xi s - c - 2 / s

noncomputable def Section10Equation1056UniformStationary.qhatMinusMajorant_of_uniform_stationary {R : ℝ → ℝ} {β : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = Section10Equation1053NonCircular.explicitKappaOneAdjointPlus) (h27 : Lemma1027AdjointRComparison R) (hβ : β ≤ 3) (hcompact : ContinuousOn (Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi) (Set.Icc β (stationaryCutoff h27))) : QhatMinusMajorant R

One compact choice of c after the uniform cutoff has been frozen. The compact premise is initial data only; it contains neither a scalar-ratio bound nor a majorant.

Equations

• Section10Equation1056UniformStationary.qhatMinusMajorant_of_uniform_stationary h hadj h27 hβ hcompact = { cMinus := max 1152 (Classical.choose ⋯ + 1), cutoff := max 4 (Classical.choose ⋯), A := 2, four_le_cutoff := ⋯, one_le_A := Section10Equation1056UniformStationary.qhatMinusMajorant_of_uniform_stationary._proof_15, majorizes_log := ⋯, envelope_slope_nonpos := ⋯ }