Proposition 3.3
OpenQAlgorithms.Papers.Independent.Intakethird100.P20.quantum_lattice_has_no_pointsFor a complex Hilbert space with , the complete lattice of closed subspaces has no completely prime lattice points:
The point condition preserves arbitrary joins. It is distinct from maximality of a proper filter base.
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20
noncomputable section
namespace QAlgorithms.Papers.Independent.Intakethird100.P20
open Set TopologicalSpace
open QAlgorithms.Papers.Independent.Next46.P33 (Projection)
open scoped Topology
universe u v
/-- Proposition 3.3; de Groote, Observables I, PDF p./pp. 38.
-/
theorem quantum_lattice_has_no_points {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
(hdim : 1 < Module.rank ℂ H) :
¬ ∃ p : Set (ClosedSubmodule ℂ H), IsLatticePoint p := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P20
end
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
For every complete complex inner product space , equipped with its normed additive commutative group structure, whose complex vector-space rank is strictly greater than , there is no set of closed complex linear subspaces of satisfying all of the following: is nonempty, excludes the zero subspace, is upward closed under inclusion, is closed under binary intersections, and, for every set of closed subspaces, if its supremum—the closed linear span of their union—belongs to , then some member of belongs to . The family may be empty, in which case its supremum is the zero subspace. The rank condition allows infinite-dimensional spaces and excludes spaces of dimension zero or one.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.