arnold_conjecture_torus

⚠️ Retired — specification defect

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

Arnold conjecture for tori: A Hamiltonian diffeomorphism of a symplectic manifold has at least as many fixed points as the minimum number of critical points of a smooth function. For the torus T^n, the bound is 2^n (Morse theory bound). Proved for many cases; general symplectic case via Floer theory.

Why this node was retired

The posted statement is

import Mathlib

theorem arnold_conjecture_torus (n : ℕ) (hn : 1 ≤ n)
    (phi : (Fin n → AddCircle (1 : ℝ)) → (Fin n → AddCircle (1 : ℝ)))
    (hphi : Continuous phi)
    (hhom : ∀ x y : Fin n → AddCircle (1 : ℝ),
      phi (x + y) = phi x + phi y) :
    ∃ x : Fin n → AddCircle (1 : ℝ), phi x = x := by
  sorry

The map is merely an additive torus endomorphism, so zero is fixed. Hamiltonian dynamics and the fixed-point-count conclusion are missing.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

For a Hamiltonian diffeomorphism of the standard symplectic torus T^(2n), assert at least 2n+1 fixed points; if every fixed point is nondegenerate, assert at least 2^(2n). Include the symplectic structure and Hamiltonian-isotopy condition.

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.