Recognition.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Unconditional quasi-isometric recognition of virtually polycyclic groups

The geometric height theorem, finiteness and duality endgame, and solvable lattice realization combine with Gromov's polynomial-growth theorem to yield virtual polycyclicity and a finite-index uniform-lattice model.

theorem OAI.PolycyclicRecognition.group_recognition line 24
Source documentation
The main group recognition theorem and its uniform-lattice realization.
Distinct definitions of this name: ComparatorChallenges/PolycyclicRecognition.lean:209 (same statement text; different proof or body). Qualify references as OAI.PolycyclicRecognition.group_recognition@path.
```
theorem group_recognition
    {P J : Type} [Group P] [Group J] [Group.FG P] [Group.FG J]
    (e : GroupCoarseEquivalence P J) (hP : IsVirtuallyPolycyclic P) :
    IsVirtuallyPolycyclic J ∧
      ∃ Γ : Subgroup J, Γ.FiniteIndex ∧
        ∃ (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier),
          IsUniformLattice Λ ∧ Nonempty (Γ ≃* Λ) :=
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel
theorem OAI.PolycyclicRecognition.uniform_lattice_recognition line 36
Source documentation
A group quasi-isometric to a uniform solvable Lie lattice is virtually isomorphic to a uniform lattice in a connected simply connected solvable Lie group. The new ambient Lie group is allowed to differ from the original one.
```
theorem uniform_lattice_recognition
    (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)
    (hΛ : IsUniformLattice Λ)
    {J : Type} [Group J] [Group.FG J] (e : GroupCoarseEquivalence Λ J) :
    ∃ Γ : Subgroup J, Γ.FiniteIndex ∧
      ∃ (R : SimplyConnectedSolvableLieModel) (Δ : Subgroup R.carrier),
        IsUniformLattice Δ ∧ Nonempty (Γ ≃* Δ) :=
…
```
Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.GroupCoarseEquivalence

theorem OAI.PolycyclicRecognition.recognition_and_lattice line 46

Source documentation

The metric formulation, retaining the concrete proper word-metric data.

theorem recognition_and_lattice
    {P J : Type} [Group P] [Group J] [MetricSpace P] [MetricSpace J]
    [IsIsometricSMul P P] [IsIsometricSMul J J] [Group.FG P] [Group.FG J]
    [DiscreteTopology J] [ProperSpace J]
    [MeasurableSpace J] [BorelSpace J] [MeasurableMul J]
    (e : MetricQuasiEquivalence P J) (hP : IsVirtuallyPolycyclic P)
    (CP : LinearMetricChains P)
    (hPfinite : ∀ r : ℝ, (Metric.closedBall (1 : P) r).Finite) :
    IsVirtuallyPolycyclic J ∧
      ∃ Γ : Subgroup J, Γ.FiniteIndex ∧
        ∃ (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier),
          IsUniformLattice Λ ∧ Nonempty (Γ ≃* Λ) :=
…

Mentions: OAI.PolycyclicRecognition.MetricQuasiEquivalence, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel

theorem OAI.PolycyclicRecognition.lattice_recognition line 63
Source documentation
The full finite-covolume lattice corollary. Finite generation of the source lattice follows from the given coarse equivalence. The existing discrete subgroup theorem then supplies its polycyclicity, without a uniformity input.
Distinct definitions of this name: ComparatorChallenges/PolycyclicRecognition.lean:236 (same statement text; different proof or body). Qualify references as OAI.PolycyclicRecognition.lattice_recognition@path.
```
theorem lattice_recognition
    (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)
    (hΛ : IsFiniteCovolumeLattice Λ)
    {J : Type} [Group J] [Group.FG J] (e : GroupCoarseEquivalence Λ J) :
    ∃ Γ : Subgroup J, Γ.FiniteIndex ∧
      ∃ (R : SimplyConnectedSolvableLieModel) (Δ : Subgroup R.carrier),
        IsUniformLattice Δ ∧ Nonempty (Γ ≃* Δ) := by
…
```
Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.IsFiniteCovolumeLattice, OAI.PolycyclicRecognition.GroupCoarseEquivalence

theorem OAI.PolycyclicRecognition.main_uniform_bounded_height line 80

Source documentation

The standalone geometric main theorem of the paper.

Distinct definitions of this name: ComparatorChallenges/PolycyclicRecognition.lean:219 (same statement text; different proof or body). Qualify references as OAI.PolycyclicRecognition.main_uniform_bounded_height@path.

theorem main_uniform_bounded_height
    (R : SimplyConnectedSolvableLieModel) (d : ProperChainMetric R.carrier)
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier) a)
    (huni : ModelIsUnimodular R)
    {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
    (q : HeightSpace T.character ≃ₗ[ℝ] W)
    (Exp : GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier → R.carrier)
    (hExp : IsGroupExponential Exp) (π : R.carrier →* Multiplicative W)
    (hπExp : ∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x)) :
    letI := d.compatibleMetric
…

Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.ProperChainMetric, OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.ModelIsUnimodular, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection