Quantitative endpoint selection in the activation step, equations (26)–(27).

theorem EulerDNSelection.positive_cross_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Λ : E →L[ℝ] E) (hΛ : Λ.IsPositive) (p q : E) : inner ℝ (Λ p) q ^ 2 ≤ inner ℝ (Λ p) p * inner ℝ (Λ q) q

theorem EulerDNSelection.select_endpoint (C ε a b d cpp cpq cqp cqq : ℝ) (hC : 1 ≤ C) (hε : 0 ≤ ε) (hsmall : 16 * (C + 1) * ε ≤ 1) (ha : 0 ≤ a) (had : b ^ 2 ≤ a * d) (hd : 0 ≤ d) (haC : a ≤ C) (hbC : |b| ≤ C) (hpp : cpp < 0) (hppε : |cpp| ≤ ε) (hpq : |cpq| ≤ ε) (hqp : |cqp| ≤ ε) (hqq : |cqq| ≤ ε) : ∃ (yp : ℝ) (yq : ℝ), (b - 1 - cqp) * yp + (d - cqq) * yq = 1 ∧ -8 * (C + 1) ≤ (a - cpp) * yp + (b - cpq) * yq ∧ (a - cpp) * yp + (b - cpq) * yq ≤ 0 ∧ |yp| + |yq| ≤ 8 * (C + 1)

A positive semidefinite endpoint matrix, perturbed by a unit shear and a small matrix with negative first diagonal entry, allows the required polarized output.

theorem EulerDNSelection.select_endpoint_scaled (C ε h a b d cpp cpq cqp cqq : ℝ) (hC : 1 ≤ C) (hε : 0 ≤ ε) (hsmall : 16 * (C + 1) * ε ≤ 1) (hh : 0 < h) (ha : 0 ≤ a) (had : b ^ 2 ≤ a * d) (hd : 0 ≤ d) (haC : a ≤ C * h) (hbC : |b| ≤ C * h) (hpp : cpp < 0) (hppε : |cpp| ≤ ε * h) (hpq : |cpq| ≤ ε * h) (hqp : |cqp| ≤ ε * h) (hqq : |cqq| ≤ ε * h) : ∃ (yp : ℝ) (yq : ℝ), (b - h - cqp) * yp + (d - cqq) * yq = 1 ∧ -8 * (C + 1) ≤ (a - cpp) * yp + (b - cpq) * yq ∧ (a - cpp) * yp + (b - cpq) * yq ≤ 0 ∧ |yp| + |yq| ≤ 8 * (C + 1) / h

The endpoint choice at an arbitrary positive shear scale h.

theorem EulerDNSelection.select_endpoint_hilbert {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Λ B : E →L[ℝ] E) (p q : E) (C ε h : ℝ) (hΛ : Λ.IsPositive) (hp : ‖p‖ = 1) (hq : ‖q‖ = 1) (hpq : inner ℝ p q = 0) (hC : 1 ≤ C) (hε : 0 ≤ ε) (hh : 0 < h) (hsmall : 16 * (C + 1) * ε ≤ 1) (hΛbound : ‖Λ‖ ≤ C * h) (hBbound : ‖B‖ ≤ ε * h) (hBpp : inner ℝ (B p) p < 0) : ∃ (yp : ℝ) (yq : ℝ), have Y := yp • p + yq • q; have w := Λ Y - B Y - (h * inner ℝ p Y) • q; inner ℝ w q = 1 ∧ -8 * (C + 1) ≤ inner ℝ w p ∧ inner ℝ w p ≤ 0 ∧ ‖Y‖ ≤ 8 * (C + 1) / h