theorem helperForTheorem_6_8_continuous_odd_euclideanTwo_coordinate_exists_zero (h : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)) (hcont : Continuous h) (hodd : ∀ (x : UnitSphereTwo), h (-x) = -h x) (i : Fin 2) : ∃ (x : UnitSphereTwo), (h x).ofLp i = 0

Helper for Theorem 6.8: for an odd continuous map S² → ℝ², each coordinate function has a zero.

theorem helperForTheorem_6_8_euclideanTwo_eq_zero_of_proj_zero {v : EuclideanSpace ℝ (Fin 2)} (h0 : (EuclideanSpace.proj 0) v = 0) (h1 : (EuclideanSpace.proj 1) v = 0) : v = 0

Helper for Theorem 6.8: in ℝ², vanishing of both coordinate projections implies the vector is zero.

theorem helperForTheorem_6_8_exists_antipodal_equal_of_continuous_of_odd_zero_principle (hoddZero : ∀ (h : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous h → (∀ (x : UnitSphereTwo), h (-x) = -h x) → ∃ (x : UnitSphereTwo), h x = 0) (g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)) (hg : Continuous g) : ∃ (x : UnitSphereTwo), g x = g (-x)

Helper for Theorem 6.8: an odd-zero principle for continuous maps S² → ℝ² implies antipodal equality for continuous maps S² → ℝ².

theorem helperForTheorem_6_8_global_exists_fixed_or_antifixed_of_odd_zero_pipeline (hoddZero : ∀ (h : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous h → (∀ (x : UnitSphereTwo), h (-x) = -h x) → ∃ (x : UnitSphereTwo), h x = 0) (hreduction : (∀ (g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous g → ∃ (x : UnitSphereTwo), g x = g (-x)) → ∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x) (g : UnitSphereTwo → UnitSphereTwo) : Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x

Helper for Theorem 6.8: combining a S² → ℝ² odd-zero principle with a reduction from antipodal equality to self-map fixed/anti-fixed alternatives yields the global fixed/anti-fixed existence principle on S².

theorem helperForTheorem_6_8_exists_fixed_or_antifixed_of_continuous_of_odd_zero_pipeline (hoddZero : ∀ (h : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous h → (∀ (x : UnitSphereTwo), h (-x) = -h x) → ∃ (x : UnitSphereTwo), h x = 0) (hreduction : (∀ (g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous g → ∃ (x : UnitSphereTwo), g x = g (-x)) → ∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x) (f : UnitSphereTwo → UnitSphereTwo) (hcont : Continuous f) : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Helper for Theorem 6.8: an odd-zero principle on S² → ℝ², together with a reduction from antipodal equality to self-map fixed/anti-fixed alternatives, yields the local fixed/anti-fixed witness for any given continuous self-map of S².

theorem helperForTheorem_6_8_fixed_or_fixed_eq_antipode_of_continuous_of_odd_zero_pipeline (hoddZero : ∀ (h : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous h → (∀ (x : UnitSphereTwo), h (-x) = -h x) → ∃ (x : UnitSphereTwo), h x = 0) (hreduction : (∀ (g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous g → ∃ (x : UnitSphereTwo), g x = g (-x)) → ∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x) (f : UnitSphereTwo → UnitSphereTwo) (hcont : Continuous f) : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: an odd-zero-plus-reduction pipeline gives the local fixed-point/antipode-equality alternative for continuous self-maps of S².