Main.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ArnoldCounterexample.main line 14
Source documentation
The Hamiltonian counterexample, with the complete fixed set, the lower bound for all smooth functions, and a genuine nonzero quotient-tangent eigenvector.
Distinct definitions of this name: ComparatorChallenges/ArnoldCounterexample.lean:111 (same statement text; different proof or body). Qualify references as OAI.ArnoldCounterexample.main@path.
```
theorem main :
    ∃ φ : Q3 ≃ Q3, IsHamiltonian φ ∧ (fixedSet φ).encard = 3 ∧
      (3 : ℕ∞) < 4 ∧ 4 ≤ criticalNumber ∧ HasDegenerateFixedPoint φ := by
…
```
Mentions: OAI.ArnoldCounterexample.Q3, OAI.ArnoldCounterexample.IsHamiltonian, OAI.ArnoldCounterexample.fixedSet, OAI.ArnoldCounterexample.criticalNumber, OAI.ArnoldCounterexample.HasDegenerateFixedPoint