Fresh maximizing coordinates and signs for the finite resisting construction.

def V7.Stage5AboveTwoLowerS5A2Envelope.horizonCoordinates (d T : ℕ) (hTd : T ≤ d) : Finset (Fin d)

The first T coordinates of the ambient dimension.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.horizonCoordinates d T hTd = Finset.image (⇑(Fin.castLEEmb hTd)) Finset.univ

theorem V7.Stage5AboveTwoLowerS5A2Envelope.horizonCoordinates_card (d T : ℕ) (hTd : T ≤ d) : (horizonCoordinates d T hTd).card = T

theorem V7.Stage5AboveTwoLowerS5A2Envelope.mem_horizonCoordinates_iff {d T : ℕ} (hTd : T ≤ d) (j : Fin d) : j ∈ horizonCoordinates d T hTd ↔ ↑j < T

theorem V7.Stage5AboveTwoLowerS5A2Envelope.exists_unused_max_coordinate {d T t : ℕ} (hTd : T ≤ d) (ht : t < T) (sigma : ℕ → Fin d) (q : Point d) : ∃ (j : Fin d), ↑j < T ∧ (∀ s < t, sigma s ≠ j) ∧ ∀ (k : Fin d), ↑k < T → (∀ s < t, sigma s ≠ k) → |q k| ≤ |q j|

At every chronological stage t<T, fewer than T previously selected coordinates leave a nonempty legal horizon set; compact finiteness then gives an unused coordinate maximizing the current absolute coordinate.

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.resistingSign (a : ℝ) : ℝ

A sign whose product with the input is its absolute value, choosing one at zero.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.resistingSign a = if 0 ≤ a then 1 else -1

theorem V7.Stage5AboveTwoLowerS5A2Envelope.resistingSign_spec (a : ℝ) : (resistingSign a = 1 ∨ resistingSign a = -1) ∧ resistingSign a * a = |a|