Topological producer for a genuine minus first crossing

The crossing is the least point of the nonempty compact set on which the normalized minus slope reaches c.

theorem Section10MinusFirstCrossingProducer.normalizedMinusBase_continuousAt {R : ℝ → ℝ} {β s : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hβs : β < s) : ContinuousAt (Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi) s

The normalized minus base is continuous at every point strictly to the right of the apparatus threshold.

theorem Section10MinusFirstCrossingProducer.minusFirstCrossing_of_reaches {R : ℝ → ℝ} {β c S v : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hβS : β < S) (hβoneS : β + 1 ≤ S) (hinitial : ∀ u ∈ Set.Icc β S, Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi u < c) (hSv : S ≤ v) (hv : c ≤ Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi v) : ∃ (w : Section10Equation1053MinusFirstCrossing.MinusFirstCrossing R Section10CanonicalXi.xi c β S), S ≤ w.s

If the normalized base starts strictly below c and reaches c by v, the least point of the closed crossing set is a genuine first crossing.

hDDEβ is the endpoint derivative required literally by the current MinusFirstCrossing.hasDeriv field. The apparatus itself supplies the DDE only for β < u, so this one endpoint cannot be inferred from that interface.

theorem Section10MinusFirstCrossingProducer.producesMinusFirstCrossing {R : ℝ → ℝ} {β c S : ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β) (hβS : β < S) (hβoneS : β + 1 ≤ S) (hinitial : ∀ u ∈ Set.Icc β S, Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi u < c) (v : ℝ) : S ≤ v → c ≤ Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi v → ∃ (w : Section10Equation1053MinusFirstCrossing.MinusFirstCrossing R Section10CanonicalXi.xi c β S), S ≤ w.s

Pointwise crossing production, in the exact shape consumed by ProducesMinusFirstCrossing after unfolding that definition.