freyd_conjecture

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Freyd's conjecture (Peter Freyd): In the stable homotopy category, a map from a finite complex to itself induces the zero map on homology if and only if it is phantom. Related to the generating hypothesis that π*(S) detects all stable maps between finite complexes. Open.

Why this node was retired

The posted statement is

import Mathlib

theorem freyd_conjecture :
    ∀ (f : (EuclideanSpace ℝ (Fin 3)) → (EuclideanSpace ℝ (Fin 3))),
      Continuous f →
      (∀ x : EuclideanSpace ℝ (Fin 3), ‖x‖ = 1 → ‖f x‖ = 1) →
      (∀ x : EuclideanSpace ℝ (Fin 3), ‖x‖ = 1 → f (f x) = x ∧ f x ≠ x) →
      ∃ x : EuclideanSpace ℝ (Fin 3), ‖x‖ = 1 ∧ f x = x := by
  sorry

A fixed-point statement on the sphere substitutes for a stable-homotopy generating hypothesis and even assumes absence of fixed points there.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Freyd’s generating hypothesis: for a map f:X→Y between finite spectra, if π_k(f)=0 for every integer k, then f=0 in the stable homotopy category. The current sphere-involution formula should be replaced wholesale; ordinary homology is not the required stable homotopy invariant.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.