Finitely many spherical orthogonality loci pass through a positive plane

PeriodDomain.neg_of_mem_orthogonal makes Q negative definite on Wᗮ for every positive plane W of a space of signature (2, n - 2). The reusable continuity and coercivity results now live in Continuous.lean and Bounds.lean; this file spends them on spherical classes and lattice walls.

Main results

• PeriodDomain.finite_sphericalOrthogonal_inter — for a lattice Λ, only finitely many spherical classes of Λ are orthogonal to a given positive plane, i.e. finite_orthogonalityLoci_through: finitely many spherical orthogonality loci contain a given positive plane.

What is not proved here, and why it is not an oversight

The region-wise statement — finitely many walls meet a family of positive planes — does not follow. The coercivity constant of -Q on Wᗮ depends on W and degrades to 0 as the plane approaches the boundary of the positive-plane locus, so a bounded family of planes does not by itself supply a uniform constant. This is one of the two gaps in Bridgeland's own §11 argument. The other chart already answers it the honest way: Walls/Spherical/Finiteness.lean makes coercivity an explicit field of BoundedRegion rather than deriving it. A region-wise route (A) statement must do the same, and is deliberately left to its own change.

Everything below is about an arbitrary real quadratic space and its lattices; Λ is the ℤ-span of an ℝ-basis and is not asserted to be N(X), in the discipline of LinearAlgebra/Lattice/Mukai/Basic.lean.

def PeriodDomain.sphericalOrthogonal {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] (Q : QuadraticForm ℝ M) (W : Submodule ℝ M) : Set M

The spherical classes orthogonal to W. By mem_orthogonalityLocus_iff_mem_orthogonal these are exactly the classes whose orthogonalityLocus passes through W.

Equations

• PeriodDomain.sphericalOrthogonal Q W = {δ : M | PeriodDomain.IsSphericalClass Q δ ∧ δ ∈ PeriodDomain.orthogonal Q W}

theorem PeriodDomain.isBounded_sphericalOrthogonal {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} {W : Submodule ℝ M} (hsig : HasSignatureTwo Q) (hW : IsPositivePlane Q W) : Bornology.IsBounded (sphericalOrthogonal Q W)

The spherical classes orthogonal to a positive plane form a bounded set.

Q is negative definite on Wᗮ, so -Q is a positive definite form there and -Q δ = 1 confines δ to a level set, which is bounded.

theorem PeriodDomain.finite_sphericalOrthogonal_inter {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} {W : Submodule ℝ M} (hsig : HasSignatureTwo Q) (hW : IsPositivePlane Q W) {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℝ M) : (sphericalOrthogonal Q W ∩ ↑(Submodule.span ℤ (Set.range ⇑b))).Finite

Only finitely many spherical classes of a lattice are orthogonal to a given positive plane.

Bounded by isBounded_sphericalOrthogonal, and a lattice meets a bounded set finitely. Λ is the ℤ-span of an ℝ-basis; nothing identifies it with a geometric lattice.

theorem PeriodDomain.finite_orthogonalityLoci_through {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} {W : Submodule ℝ M} (hsig : HasSignatureTwo Q) (hW : IsPositivePlane Q W) {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℝ M) : {δ : M | IsSphericalClass Q δ ∧ W ∈ orthogonalityLocus Q δ ∧ δ ∈ ↑(Submodule.span ℤ (Set.range ⇑b))}.Finite

Finitely many spherical orthogonality loci contain a positive plane.

The same statement as finite_sphericalOrthogonal_inter, said in walls: this is what a local-finiteness argument for route (A) starts from, and the pointwise case is unconditional where the region-wise case is not.