Helper for Theorem 6.8: an antipodal-equality source on maps S² → ℝ²,
together with a non-circular antipodal-to-self-map reduction, yields the packaged
common-zero-plus-reduction upstream prerequisite.
Helper for Theorem 6.8: a common-zero principle for continuous odd real-valued
pairs on S² implies the antipodal-equality principle for continuous maps
S² → ℝ².
Helper for Theorem 6.8: the common-zero principle for odd real-valued pairs
on S² is equivalent to the antipodal-equality principle for continuous maps
S² → ℝ².
Helper for Theorem 6.8: the packaged common-zero-plus-reduction prerequisite is equivalent to the packaged antipodal-equality-plus-reduction prerequisite.
Helper for Theorem 6.8: any packaged antipodal-equality source and non-circular reduction package can be transported to the equivalent packaged common-zero-plus-reduction form.
Helper for Theorem 6.8: any packaged common-zero-plus-reduction source can be transported to the equivalent packaged antipodal-equality-plus-reduction form.
Helper for Theorem 6.8: the packaged common-zero-plus-reduction prerequisite is equivalent to the packaged odd-zero-plus-reduction prerequisite.
Helper for Theorem 6.8: an antipodal-equality source on S² → ℝ²
implies the odd-zero component of the packaged odd-zero-plus-reduction prerequisite.
Helper for Theorem 6.8: any non-circular antipodal-equality-to-self-map reduction implies the reduction component of the packaged odd-zero-plus-reduction prerequisite.
Helper for Theorem 6.8: a packaged upstream prerequisite consisting of
an odd-zero principle on continuous odd maps S² → ℝ² together with an
odd-zero-to-self-map fixed/anti-fixed reduction principle on S².
Helper for Theorem 6.8: any packaged odd-zero-plus-reduction source yields
the corresponding upstream antipodal-equality source on continuous maps S² → ℝ².
Helper for Theorem 6.8: any packaged odd-zero-plus-reduction source yields the corresponding non-circular antipodal-equality-to-self-map reduction.
Helper for Theorem 6.8: any packaged common-zero-plus-reduction source on S²
can be converted directly into the packaged odd-zero-plus-reduction source.
Helper for Theorem 6.8: an upstream antipodal-equality-plus-reduction package on S²
simultaneously yields the packaged odd-zero-plus-reduction and
common-zero-plus-reduction prerequisites used downstream.
Helper for Theorem 6.8: an unconditional upstream antipodal-equality source and
non-circular reduction package on S² directly yields the unconditional packaged
odd-zero-plus-reduction prerequisite on S².
Helper for Theorem 6.8: converting a packaged antipodal-equality source and
non-circular reduction on S² into the corresponding packaged odd-zero-plus-
reduction prerequisite.
Helper for Theorem 6.8: the unconditional odd-zero-plus-reduction package on S²
follows from nonemptiness of the upstream antipodal-equality-plus-reduction package.
Helper for Theorem 6.8: packaging a concrete antipodal-equality-plus-reduction
witness directly yields the corresponding Nonempty source.
Helper for Theorem 6.8: explicit antipodal-equality and non-circular reduction components package into the corresponding nonempty upstream source.
Helper for Theorem 6.8: for this packaged upstream proposition, Nonempty is
equivalent to giving the witness package itself.
Helper for Theorem 6.8: if the codomain proposition is nonempty, then the corresponding implication proposition is nonempty.
Helper for Theorem 6.8: reducing the packaged nonempty upstream goal to the corresponding pair of nonempty component goals.
Helper for Theorem 6.8: if one has the upstream package consisting of a common-zero
principle for odd real pairs on S² and a non-circular antipodal-to-self-map reduction,
then one can extract both concrete component goals on S² (antipodal equality and
fixed/anti-fixed existence for continuous self-maps).
Independent upstream bridge for Theorem 6.8.
This declaration is intentionally placed before the package chain that starts at
helperForTheorem_6_8_upstream_nonempty_antipodal_and_selfMap_component_goals_on_S2.
Its only role is to provide an acyclic source for:
A: antipodal equality on continuous mapsS² → ℝ²;R: a reductionA →fixed/anti-fixed existence on continuous self-mapsS².
Non-circular proof contract:
- The future proof here must not use any theorem whose dependency graph contains
helperForTheorem_6_8_upstream_nonempty_antipodal_and_selfMap_component_goals_on_S2(or the downstream chain built from it). - Preferred path: import/hoist truly upstream results for
AandR, then return⟨hA, hR⟩directly.
Bridge theorem for Theorem 6.8 pipeline: expose the two concrete component goals
early (antipodal-equality source on S² → ℝ² and global fixed/anti-fixed witnesses
for continuous self-maps of S²).
This theorem is intentionally placed before the package theorem to provide a stable, acyclic planning target in the direct-item pipeline.
Anti-cycle rule (hard):
- When proving this theorem, do not use any declaration that depends on this theorem.
- In particular, avoid the known cycle
533 -> 567 -> 623 -> 639 -> 655 -> (822, 934) -> ... -> 533. - So
helperForTheorem_6_8_continuous_map_unitSphereTwo_to_euclideanTwo_exists_antipodal_equalandhelperForTheorem_6_8_antipodal_equality_to_selfMap_fixed_or_antifixed_reductionare valid targets to expose for future upstream import/hoist, but not valid local prerequisites if they are still downstream in this file order.
Detailed non-cyclic proof method:
- Method A (preferred): use one imported/hoisted upstream theorem (declared in an earlier file or before line 533) that already provides antipodal equality and/or the reduction map.
- Method B (if A is unavailable): first create a new earlier bridge declaration in an upstream part file, then return here and instantiate this theorem.
- In both methods, this theorem must be proved by DAG order only:
upstream inputs ->
hA->hB := hR hA->⟨hA, hB⟩. - Never use any theorem whose reverse-dependency contains this theorem or line 567.
Lean-level skeleton for the acyclic script:
have hA : ∀ g, Continuous g -> ∃ x, g x = g (-x) := ...(upstream source)have hR : (∀ g, Continuous g -> ∃ x, g x = g (-x)) -> ∀ g, Continuous g -> ∃ x, g x = x ∨ (g x).1 = -x.1 := ...(upstream source)have hB : ∀ g, Continuous g -> ∃ x, g x = x ∨ (g x).1 = -x.1 := hR hAexact ⟨hA, hB⟩
Helper for Theorem 6.8: nonemptiness of the packaged upstream antipodal-equality
source and non-circular reduction principle on S².
Helper for Theorem 6.8: the odd-zero-plus-reduction package follows directly
from an upstream nonempty antipodal-equality-plus-reduction package on S².
Helper for Theorem 6.8: a packaged upstream prerequisite consisting of
an odd-zero principle on continuous odd maps S² → ℝ² together with an
odd-zero-to-self-map fixed/anti-fixed reduction principle on S².
Helper for Theorem 6.8: a packaged upstream prerequisite consisting of
the common-zero principle for continuous odd real pairs on S² and a
non-circular reduction from antipodal equality to fixed/anti-fixed witnesses
for continuous self-maps of S².
Helper for Theorem 6.8: upstream dependency source packaging a Borsuk-Ulam
antipodal-equality principle on S² → ℝ² together with a reduction from
antipodal equality to fixed/anti-fixed witnesses for self-maps of S².
Helper for Theorem 6.8: from a packaged upstream antipodal-equality source and
reduction map, one obtains the global fixed/anti-fixed witness principle for continuous
self-maps of S².
Helper for Theorem 6.8: a packaged upstream antipodal-equality-and-reduction
source gives a local fixed/anti-fixed witness for any continuous self-map of S².
Helper for Theorem 6.8: the packaged upstream dependency source yields the
upstream odd-zero principle on continuous odd maps S² → ℝ².
Helper for Theorem 6.8: upstream odd-zero existence principle for continuous odd
maps S² → ℝ².
Helper for Theorem 6.8: an upstream odd-zero principle on continuous odd maps
S² → ℝ² yields the corresponding upstream antipodal-equality principle.
Helper for Theorem 6.8: upstream reduction from odd-zero existence on continuous odd
maps S² → ℝ² to fixed/anti-fixed existence for continuous self-maps of S².
Helper for Theorem 6.8: a packaged upstream pair consisting of an odd-zero principle
and an odd-zero-to-self-map reduction immediately yields global fixed/anti-fixed existence
for continuous self-maps of S².
Helper for Theorem 6.8: a packaged odd-zero-plus-reduction upstream hypothesis
immediately yields the local fixed/anti-fixed witness for any continuous self-map of S².
Helper for Theorem 6.8: an upstream odd-zero principle yields the corresponding
upstream antipodal-equality principle on continuous maps S² → ℝ².
Helper for Theorem 6.8: combining an upstream odd-zero principle with an explicit antipodal-equality-to-self-map reduction yields global fixed/anti-fixed witnesses.
Helper for Theorem 6.8: upstream Borsuk-Ulam antipodal-equality principle for
continuous maps S² → ℝ².
Helper for Theorem 6.8: combining an antipodal-equality principle with an antipodal-equality-to-self-map reduction yields fixed/anti-fixed witnesses for continuous self-maps via the no-counterexample fixed-or-negation route.
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: an odd-zero principle on continuous odd maps
S² → ℝ² yields the corresponding antipodal-equality principle for continuous
maps S² → ℝ².
Helper for Theorem 6.8: on continuous maps S² → ℝ², the odd-zero and
antipodal-equality principles are equivalent.
Helper for Theorem 6.8: if a reduction from antipodal equality on S² → ℝ² to
fixed/anti-fixed existence on continuous self-maps of S² is available, then any
odd-zero principle on S² → ℝ² yields the global fixed/anti-fixed existence principle.
Helper for Theorem 6.8: upstream reduction from antipodal equality on
continuous maps S² → ℝ² to fixed/anti-fixed existence for continuous self-maps of S².
Helper for Theorem 6.8: once the two concrete S² components are available
(S² → ℝ² antipodal equality and antipodal-to-self-map reduction), they package
into the corresponding nonempty upstream source.
Helper for Theorem 6.8: once the upstream antipodal-equality-to-self-map reduction
is available, the odd-zero principle on S² → ℝ² gives fixed/anti-fixed witnesses for
continuous self-maps of S².
Helper for Theorem 6.8: an odd-zero principle on continuous odd maps
S² → ℝ², together with an antipodal-equality-to-self-map reduction, yields the
corresponding odd-zero-to-self-map reduction principle.
Helper for Theorem 6.8: upstream reduction from odd-zero existence for continuous odd
maps S² → ℝ² to fixed/anti-fixed existence for continuous self-maps of S².
Helper for Theorem 6.8: upstream reduction from antipodal equality on
continuous maps S² → ℝ² to fixed/anti-fixed existence for continuous self-maps of S².
Helper for Theorem 6.8: prerequisite global fixed-point-or-negation principle for
continuous self-maps of S².
Helper for Theorem 6.8: the prerequisite global fixed-point-or-negation principle implies the corresponding no-counterexample statement.
Helper for Theorem 6.8: prerequisite no-counterexample fixed-point-or-negation
statement for continuous self-maps of S².