OAI.Problem340.exists_C1_entropy_counterexample
OpenThe theorem states that there exists a positive integer q and a self-map f of the manifold M_q = S¹ × (S²)^(q+1), the product of the unit circle in ℝ² with q+1 copies of the unit sphere in ℝ³, such that f is C¹ and the following hold. Here C¹ means f is continuous and, around each point x, there is an open set U in the ambient space ℝ² × (ℝ³)^(q+1) containing the image of x under the coordinate embedding of M_q, together with a map F that is continuously differentiable on U and agrees with f, in the embedding coordinates, on all points of M_q whose embedding lies in U. The topological entropy of f, in the cover-entropy sense over the whole space, equals 0 in the extended reals. Singular homology with real coefficients in degree 2 has a nonzero class v with f_(v) = 2v. Also log 2 > 0 and log 2 ≤ log of the total real-homology spectral radius of f, where that radius is the supremum, over all degrees n, real pairs (a,b) and classes u, v in degree n not both zero satisfying f_(u) = a u − b v and f_*(v) = b u + a v, of √(a²+b²). Finally f is not bijective, and 5 ≤ 2q+3, the manifold dimension condition.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/C1EntropyCounterexample.lean; bytes 2274..2802 -- 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_C1EntropyCounterexample namespace OAI noncomputable section open CategoryTheory namespace Problem340
theorem exists_C1_entropy_counterexample :
∃ q : ℕ, 0 < q ∧ ∃ f : CounterexampleManifold q → CounterexampleManifold q, ∃ hf : IsC1SelfMap q f, Dynamics.coverEntropy f (Set.univ : Set (CounterexampleManifold q)) = (0 : EReal) ∧ (∃ v : RealSingularHomology 2 (CounterexampleManifold q), v ≠ 0 ∧ realHomologyMap 2 f hf.1 v = (2 : ℝ) • v) ∧ 0 < Real.log (2 : ℝ) ∧ Real.log (2 : ℝ) ≤ Real.log (totalRealHomologySpectralRadius f hf.1) ∧ ¬ Function.Bijective f ∧ 5 ≤ 2 * q + 3 := by
sorry
end Problem340
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.