Helper for Theorem 6.8: a global fixed-point-or-antipode-equality principle on
continuous self-maps of S² implies the global fixed/anti-fixed existence principle.
Helper for Theorem 6.8: existence of a continuous counterexample to the fixed/anti-fixed witness is equivalent to existence of a continuous counterexample to the fixed-point-or-antipode-equality disjunction.
Helper for Theorem 6.8: a global fixed/anti-fixed existence principle is equivalent to nonexistence of a continuous counterexample to that principle.
Helper for Theorem 6.8: a global fixed-point-or-antipode-equality principle is equivalent to nonexistence of a continuous counterexample to that principle.
Upstream helper for Theorem 6.8 in part4:
an antipodal-equality principle on S² → ℝ² implies the odd-zero principle on
continuous odd maps S² → ℝ².
Upstream helper for Theorem 6.8 in part4:
the antipodal-equality principle and the odd-zero principle on S² → ℝ² are equivalent.
Upstream helper for Theorem 6.8 in part4:
an antipodal-equality principle on S² → ℝ² yields a common zero for every pair
of continuous odd real-valued maps on S².
Upstream helper for Theorem 6.8 in part4:
a common-zero principle for continuous odd real-valued pairs on S² implies the
odd-zero principle on continuous odd maps S² → ℝ².
Upstream helper for Theorem 6.8 in part4:
a common-zero principle for continuous odd real-valued pairs on S² implies the
antipodal-equality principle on continuous maps S² → ℝ².
Upstream helper for Theorem 6.8 in part4:
on maps S² → ℝ², the odd-real-pair common-zero principle is equivalent to the
antipodal-equality principle.
On S², every point has ambient Euclidean norm 1.
If two unit vectors in ℝ^3 are linearly dependent, they are equal or antipodal.
Coercion of a point on S² to Fin 3 → ℝ is nonzero.
In ℝ^3, x × y = 0 implies that y is a scalar multiple of nonzero x.
If x × p = (-x) × q, then p + q is parallel to x.
Non-antipodal and non-identical unit vectors in ℝ^3 have nonzero cross product.
For a self-map with no fixed/anti-fixed point, every point has nonzero cross product with its image.
A common-zero source for odd real pairs produces a point where the first two
coordinates of c x - c (-x) vanish, for any continuous c : S² → ℝ^3.
In ℝ^3, if the first two coordinates of d vanish and x ⬝ d = 0, then
d = 0 whenever the third coordinate of x is nonzero.
Specialized form for d = (x × g x) - ((-x) × g(-x)): if its first two
coordinates vanish and x₂ ≠ 0, then the two cross-product terms are equal.
If the first two coordinates of
(x × p) - ((-x) × q) vanish and x₂ = 0, then (p + q)₂ = 0.
Rewriting identity for the cross-difference field used in the part4 reduction:
x × g(x) - ((-x) × g(-x)) = x × (g(x) + g(-x)).
The scalar map x ↦ x · (g x + g(-x)) is continuous on S².
The scalar map x ↦ x · (g x + g(-x)) is odd on S².
Upstream odd-zero consequence used in the long-line part4 reduction:
there exists a point where x · (g x + g(-x)) = 0.
Common-zero bridge (coordinate 0 + dot-sum) for the cross-difference field in part4.
Common-zero bridge (coordinate 1 + dot-sum) for the cross-difference field in part4.
Independent upstream bridge for Theorem 6.8.
This theorem is intentionally placed in section06_part4 (strictly earlier than
section06_part5/section06_part6) so downstream files can consume it without
forming a declaration-order cycle.
Non-circularity contract:
- Do not prove this by using any declaration from
section06_part6. - Future completion should use genuinely upstream ingredients only.
Core upstream Borsuk-Ulam source required by Theorem 6.8 in the part4 stage.