OAI.ArnoldCounterexample.main
OpenThe theorem states that the complex projective quadric Q = {[z] ∈ ℂP⁴ : ∑ⱼ₌₀⁴ zⱼ² = 0} admits a Hamiltonian bijection φ with exactly three fixed points, whereas every smooth real-valued function on Q has at least four critical points, including functions with degenerate critical points; equivalently, 3 < 4 ≤ the infimum of their critical-set cardinalities, with infinite cardinalities recorded as ∞. Here Hamiltonian means that φ is the endpoint of an isotopy starting at the identity whose forward maps, inverse maps, and Hamiltonian have globally smooth extensions on ℝ × ℂ⁵. For times in [0,1], the maps preserve the unit quadric, are inverse there, and commute with multiplication by unit complex scalars; the Hamiltonian is invariant under these scalars. They satisfy ω(∂ₜFₜ(z),v) = dHₜ(Fₜ(z))[v] for every horizontal v at Fₜ(z), where ω(u,v) = 2 Im ∑ⱼ conjugate(uⱼ)vⱼ and horizontality at z means both ∑ⱼ conjugate(zⱼ)vⱼ = 0 and ∑ⱼ zⱼvⱼ = 0. Smooth functions on Q are those with smooth local extensions after pullback to the unit quadric, and criticality means that every such extension has zero derivative in all horizontal directions. Moreover, φ has a degenerate fixed point: some unit representative z and nonzero horizontal vector v admit a smooth local lift G of φ with G(z) = z and DG(z)v − v = a iz for some real a. Thus the induced derivative on the quotient tangent has a genuine nonzero eigenvector with eigenvalue 1.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/ArnoldCounterexample.lean; bytes 4702..5045 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_ArnoldCounterexample namespace OAI noncomputable section open scoped BigOperators ContDiff namespace ArnoldCounterexample
/-- The Hamiltonian counterexample, with the complete fixed set, the lower bound
for all smooth functions, and a genuine nonzero quotient-tangent eigenvector. -/
theorem main :
∃ φ : Q3 ≃ Q3, IsHamiltonian φ ∧ (fixedSet φ).encard = 3 ∧
(3 : ℕ∞) < 4 ∧ 4 ≤ criticalNumber ∧ HasDegenerateFixedPoint φ := by
sorry
end ArnoldCounterexample
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.