Non-circular audit of the κ = 1 stationary-exclusion step

This file deliberately does not import or reproduce Equation1053RemainderCertificate. It proves the explicit-adjoint rational identities and reduces a stationary candidate to the one strict real integral inequality that the current hypotheses still do not prove.

The reduction also exposes an interface mismatch: the first-crossing argument in C2Lemma1028FirstCrossing433 produces only the equality normalizedMinusBase R ξ s = c. The usual proof of (10.53), however, first uses that the weighted envelope on [s-1,s] is bounded by its value at s. That window-maximum fact is not a consequence of the bare equality and is not present in Equation1053MinusExclusion's premises.

noncomputable def Section10Equation1053NonCircular.explicitKappaOneAdjointPlus (s : ℝ) : ℝ

Equations

• Section10Equation1053NonCircular.explicitKappaOneAdjointPlus s = s ^ 2 - 2 * s + 1 / 2

theorem Section10Equation1053NonCircular.explicitKappaOneAdjointPlus_pos {s : ℝ} (hs : 2 ≤ s) : 0 < explicitKappaOneAdjointPlus s

theorem Section10Equation1053NonCircular.explicitKappaOneAdjointPlus_dde (s : ℝ) : HasDerivAt (fun (u : ℝ) => u * explicitKappaOneAdjointPlus u) (2 * explicitKappaOneAdjointPlus s + explicitKappaOneAdjointPlus (s + 1)) s

noncomputable def Section10Equation1053NonCircular.kappaOneLogSlope (s : ℝ) : ℝ

Equations

• Section10Equation1053NonCircular.kappaOneLogSlope s = 4 * s / (2 * s ^ 2 - 1)

theorem Section10Equation1053NonCircular.kappaOne_adjoint_logSlope_exact {s : ℝ} (hs : 1 ≤ s) : (explicitKappaOneAdjointPlus (s + 1) + explicitKappaOneAdjointPlus (s + 2)) / ((s + 1) * explicitKappaOneAdjointPlus (s + 1)) = kappaOneLogSlope s

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

theorem Section10Equation1053NonCircular.kappaOneLogSlope_hasDerivAt {s : ℝ} (hs : 1 ≤ s) : HasDerivAt kappaOneLogSlope (-4 * (2 * s ^ 2 + 1) / (2 * s ^ 2 - 1) ^ 2) s

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

theorem Section10Equation1053NonCircular.stationary_candidate_is_logEnvelope_stationary {R ξ : ℝ → ℝ} {β c s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hξ : Section10Lemma1028.Proposition1020Xi ξ) (hsβ : β < s) (hstat : Section10Lemma1028FirstCrossing.normalizedMinusBase R ξ s = c) : HasDerivAt (Section10Lemma1028.logEnvelopeMinus R ξ c) 0 s

A stationary equality is exactly a zero derivative of the logarithmic minus envelope. This uses only the genuine DDE and positivity.

theorem Section10Equation1053NonCircular.explicit_pairing_weighted_identity {R ξ : ℝ → ℝ} {β c s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = explicitKappaOneAdjointPlus) (hsβ : β < s) (hs2 : 2 ≤ s) : s * explicitKappaOneAdjointPlus s * R s = ∫ (t : ℝ) in s - 1..s, Section10Equation1053.envelopeMinus R ξ c t * Real.exp (-Section10Equation1053.psiMinus explicitKappaOneAdjointPlus ξ c t)

The exact pairing equality in the explicit κ=1 weighted variables.

theorem Section10Equation1053NonCircular.stationary_candidate_impossible_of_strict_remainder_bound {R ξ : ℝ → ℝ} {β s₀ C c s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hadj : h.adjoint = explicitKappaOneAdjointPlus) (_hξ : Section10Lemma1028.Proposition1020Xi ξ) (hsβ : β < s) (hs2 : 2 ≤ s) (_hs₀ : s₀ ≤ s) (_hc : C ≤ c) (_hstat : Section10Lemma1028FirstCrossing.normalizedMinusBase R ξ s = c) (hstrict : ∫ (t : ℝ) in s - 1..s, Section10Equation1053.envelopeMinus R ξ c t * Real.exp (-Section10Equation1053.psiMinus explicitKappaOneAdjointPlus ξ c t) < s * explicitKappaOneAdjointPlus s * R s) : False

Non-circular endpoint reduction. hstrict is a single scalar real inequality, not a stationary-exclusion field or a same-typed certificate. It is exactly the first still-unproved (10.53) remainder inequality: all terms on its two sides are fixed by the genuine pairing data.