Helper for Theorem 6.8: nonexistence of continuous counterexamples to the fixed/anti-fixed statement is equivalent to nonexistence of continuous counterexamples to the fixed-point-or- antipode-equality statement.
Helper for Theorem 6.8: the fixed-point-or-antipode-equality no-counterexample statement is equivalent to the corresponding global existence principle.
Helper for Theorem 6.8: equality with -x in UnitSphereTwo is equivalent to equality
with the dedicated antipode map at x.
Helper for Theorem 6.8: a global fixed-point-or-negation principle on S²
immediately yields the fixed-point-or-antipode-equality principle used in this section.
Helper for Theorem 6.8: for a fixed self-map of S², the fixed-or-negation
disjunction is equivalent to the fixed-or-antipode-equality disjunction.
Helper for Theorem 6.8: globally on continuous self-maps of S², fixed-or-negation
and fixed-or-antipode-equality are equivalent principles.
Helper for Theorem 6.8: global fixed-point-or-negation is equivalent to nonexistence of a continuous counterexample in fixed-or-negation form.
Helper for Theorem 6.8: existence of a continuous fixed-point-or-negation
counterexample is equivalent to failure of the corresponding global principle on S².
Helper for Theorem 6.8: the no-counterexample formulations in fixed-or-negation and fixed-or-antipode-equality form are equivalent.
Helper for Theorem 6.8: a no-counterexample fixed-point-or-negation hypothesis
implies the corresponding global fixed-point-or-negation principle on S².
Helper for Theorem 6.8: a no-counterexample fixed-point-or-negation hypothesis
implies the corresponding global fixed-point-or-antipode-equality principle on S².
Helper for Theorem 6.8: failure of the global fixed-point-or-antipode-equality principle
forces failure of the global fixed-point-or-negation principle on S².
Helper for Theorem 6.8: if the global fixed-point-or-antipode-equality principle fails, there exists a continuous self-map counterexample in fixed-point-or-negation form.
Helper for Theorem 6.8: nonexistence of continuous fixed-point-or-negation
counterexamples is equivalent to the global fixed-point-or-antipode-equality
principle on S².
Helper for Theorem 6.8: a global fixed-point-or-negation principle on continuous
self-maps of S² implies the global fixed/anti-fixed witness principle.
Helper for Theorem 6.8: for a fixed self-map of S², a fixed-or-negation witness
directly yields a fixed/anti-fixed witness.
Helper for Theorem 6.8: if a global fixed-point-or-negation principle is available
for continuous self-maps of S², then any continuous self-map has a fixed or anti-fixed point.
Helper for Theorem 6.8: for a fixed self-map of S², a fixed/anti-fixed witness
directly yields a fixed-or-negation witness.
Helper for Theorem 6.8: for a fixed self-map of S², fixed/anti-fixed and
fixed-or-negation witness formulations are equivalent.
Helper for Theorem 6.8: no-counterexample formulations in fixed-or-negation and
fixed/anti-fixed forms are equivalent on continuous self-maps of S².
Helper for Theorem 6.8: a global fixed/anti-fixed witness principle on continuous
self-maps of S² implies the corresponding global fixed-or-negation principle.
Helper for Theorem 6.8: global fixed/anti-fixed existence and global fixed-or-negation
principles are equivalent for continuous self-maps of S².
Helper for Theorem 6.8: nonexistence of continuous fixed-point-or-negation
counterexamples implies the global fixed/anti-fixed alternative on S².
Helper for Theorem 6.8: a no-counterexample fixed-or-negation hypothesis yields the
local fixed-or-negation disjunction for any continuous self-map of S².
Helper for Theorem 6.8: under nonexistence of continuous fixed-point-or-negation
counterexamples, each continuous self-map of S² has a fixed or anti-fixed point.
Helper for Theorem 6.8: under nonexistence of continuous fixed-point-or-negation
counterexamples, each continuous self-map of S² has a fixed or anti-fixed point.
Helper for Theorem 6.8: a Borsuk-Ulam antipodal-equality principle on maps
S² → ℝ², together with a reduction from that principle to continuous self-maps of S²,
yields the global fixed-point-or-negation principle on continuous self-maps of S².
Helper for Theorem 6.8: a Borsuk-Ulam antipodal-equality principle on maps
S² → ℝ², together with a reduction from that principle to continuous self-maps of S²,
implies the no-counterexample fixed-point-or-negation statement.
Helper for Theorem 6.8: an odd-zero principle for continuous maps
S² → ℝ², together with a reduction from antipodal equality to the
fixed/anti-fixed alternative for continuous self-maps of S², yields the
global fixed-point-or-negation principle on continuous self-maps of S².
Helper for Theorem 6.8: an odd-zero principle for continuous maps
S² → ℝ², together with a reduction from antipodal equality to the
fixed/anti-fixed alternative for continuous self-maps of S², implies the
no-counterexample fixed-point-or-negation statement.
Helper for Theorem 6.8: a Borsuk-Ulam antipodal-equality principle on maps
S² → ℝ², together with a reduction from antipodal equality to the
fixed/anti-fixed alternative for continuous self-maps of S², implies
nonexistence of continuous fixed/anti-fixed counterexamples.
Helper for Theorem 6.8: an odd-zero principle on maps S² → ℝ²,
together with a reduction from antipodal equality to the fixed/anti-fixed
alternative for continuous self-maps of S², implies nonexistence of
continuous fixed/anti-fixed counterexamples.
Helper for Theorem 6.8: once a global fixed-point-or-negation principle for
continuous self-maps of S² is available, the corresponding no-counterexample
formulation follows immediately.
Helper for Theorem 6.8: a global fixed/anti-fixed existence principle on continuous
self-maps of S² implies the no-counterexample fixed-point-or-negation statement.
Helper for Theorem 6.8: a global fixed-point-or-negation principle on continuous
self-maps of S² implies nonexistence of continuous counterexamples in fixed/anti-fixed form.
Helper for Theorem 6.8: an antipodal-equality principle on continuous maps
S² → ℝ² implies the odd-zero principle on continuous odd maps S² → ℝ².
Helper for Theorem 6.8: a packaged upstream antipodal-equality source and reduction map imply the corresponding odd-zero package and odd-zero-to-self-map reduction package.
Helper for Theorem 6.8: a packaged odd-zero source and odd-zero-to-self-map reduction imply the corresponding antipodal-equality package and antipodal-to-self-map reduction.
Helper for Theorem 6.8: the packaged antipodal-equality dependency source is equivalent to the packaged odd-zero dependency source.
Helper for Theorem 6.8: a common-zero principle for two continuous odd real-valued
maps on S² yields the odd-zero principle for continuous odd maps S² → ℝ².
Helper for Theorem 6.8: a non-circular antipodal-equality-to-self-map reduction
upgrades any odd-zero principle on S² → ℝ² to fixed/anti-fixed existence for
continuous self-maps of S².
Helper for Theorem 6.8: an antipodal-equality principle on continuous maps
S² → ℝ² yields a common zero for any pair of continuous odd real-valued maps on S².
Helper for Theorem 6.8: a common-zero source for odd real pairs together with a non-circular antipodal-to-self-map reduction yields the packaged upstream antipodal dependency source.
Helper for Theorem 6.8: a packaged pair consisting of a common-zero principle
for odd real pairs on S² and a non-circular antipodal-to-self-map reduction
immediately yields the upstream antipodal dependency source package.
Independent upstream bridge for Theorem 6.8 (placed in section06_part5 to break
declaration-order cycles in downstream files).
Purpose:
- Provide an unconditional antipodal-equality source on
S² → ℝ²; - Provide an unconditional reduction from that source to fixed/anti-fixed witnesses on
continuous self-maps of
S².
Anti-cycle contract:
- This theorem should be proved from genuinely upstream facts only.
- Do not use any declaration whose dependency graph contains the downstream bridge node
in
section06_part6(or declarations built from it).
Natural-language proof blueprint (to replace sorry later):
- Build
hA:∀ g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2), Continuous g → ∃ x : UnitSphereTwo, g x = g (-x). - Build
hR:(∀ 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).1 = -x.1. - Return
⟨hA, hR⟩directly (no downstream packaging).
Independent upstream bridge for Theorem 6.8 exposed from section06_part5.