RecognitionLatticeAssembly.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Recognition from bounded-height hypotheses

Metric comparison with the virtually polycyclic group supplies the invariant mean and the cohomological coarse comparison.

The conditional recognition theorems retain polynomial bounded-height packing and a uniform affine height estimate as explicit geometric hypotheses.

def OAI.PolycyclicRecognition.MetricQuasiEquivalence.groupCoarseEquivalence line 31
Source documentation
Finite metric balls turn the specified coarse inverse maps into the finite-difference comparison required by the cohomological inputs.
```
def groupCoarseEquivalence (e : MetricQuasiEquivalence P H)
    (hPfinite : ∀ R : ℝ, (Metric.closedBall (1 : P) R).Finite)
    (hHfinite : ∀ R : ℝ, (Metric.closedBall (1 : H) R).Finite) :
    GroupCoarseEquivalence P H where
…
```
Mentions: OAI.PolycyclicRecognition.MetricQuasiEquivalence, OAI.PolycyclicRecognition.GroupCoarseEquivalence
theorem OAI.PolycyclicRecognition.MetricQuasiEquivalence.invariantMean_of_virtuallyPolycyclic line 52
Source documentation
Amenability is derived from the original comparison group and the actual metric comparison, rather than assumed for the recognized group.
```
theorem invariantMean_of_virtuallyPolycyclic
    [DiscreteTopology H] [ProperSpace H]
    [MeasurableSpace H] [BorelSpace H] [MeasurableMul H]
    (e : MetricQuasiEquivalence P H) (hP : IsVirtuallyPolycyclic P)
    (hPfinite : ∀ R : ℝ, (Metric.closedBall (1 : P) R).Finite) :
    Nonempty (ThompsonNonamenability.InvariantMean H) := by
…
```
Mentions: OAI.PolycyclicRecognition.MetricQuasiEquivalence, OAI.ThompsonNonamenability.InvariantMean
theorem OAI.PolycyclicRecognition.MetricQuasiEquivalence.virtuallyPolycyclic_of_elementaryAmenable line 66
Source documentation
Once geometry has supplied elementary amenability, the actual metric comparison supplies all comparison data in the published duality endgame.
```
theorem virtuallyPolycyclic_of_elementaryAmenable
    [Group.FG P] [Group.FG H]
    (liFP : LiFinitenessInput) (eaFP : ElementaryAmenableFinitenessInput)
    (liPD : LiDualityInput) (bieri : BieriDualityInput)
    (e : MetricQuasiEquivalence P H) (hP : IsVirtuallyPolycyclic P)
    (hPfinite : ∀ R : ℝ, (Metric.closedBall (1 : P) R).Finite)
    (hHfinite : ∀ R : ℝ, (Metric.closedBall (1 : H) R).Finite)
    (hEA : IsElementaryAmenable H) : IsVirtuallyPolycyclic H :=
…
```
Mentions: OAI.PolycyclicRecognition.LiFinitenessInput, OAI.PolycyclicRecognition.ElementaryAmenableFinitenessInput, OAI.PolycyclicRecognition.LiDualityInput, OAI.PolycyclicRecognition.BieriDualityInput, OAI.PolycyclicRecognition.MetricQuasiEquivalence, OAI.PolycyclicRecognition.IsElementaryAmenable

theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_corrected_height line 83

Source documentation

The corrected height, including its possibly infinitely generated kernel, gives both algebraic conclusions once its geometric packing bound is available. No arbitrary Poincaré-duality comparison group is assumed.

theorem recognition_and_lattice_of_corrected_height
    (dekimpe : DekimpeLatticeRealizationInput)
    (liFP : LiFinitenessInput) (eaFP : ElementaryAmenableFinitenessInput)
    (liPD : LiDualityInput) (bieri : BieriDualityInput)
    {P H : Type} [Group P] [Group H] [MetricSpace P] [MetricSpace H]
    [IsIsometricSMul P P] [IsIsometricSMul H H] [Group.FG P] [Group.FG H]
    (e : MetricQuasiEquivalence P H) (hP : IsVirtuallyPolycyclic P)
    (hPfinite : ∀ R : ℝ, (Metric.closedBall (1 : P) R).Finite)
    (hHfinite : ∀ R : ℝ, (Metric.closedBall (1 : H) R).Finite)
    {X W : Type} [PseudoMetricSpace X] [DecidableEq X] [NormedAddCommGroup W]
    (H₀ : Subgroup H) [H₀.FiniteIndex] (τ : H₀ →* Multiplicative W)
    (gromov : ∀ (J : Subgroup τ.ker) [DecidableEq J], GromovPolynomialGrowthInput J)
…

Mentions: OAI.PolycyclicRecognition.DekimpeLatticeRealizationInput, OAI.PolycyclicRecognition.LiFinitenessInput, OAI.PolycyclicRecognition.ElementaryAmenableFinitenessInput, OAI.PolycyclicRecognition.LiDualityInput, OAI.PolycyclicRecognition.BieriDualityInput, OAI.PolycyclicRecognition.MetricQuasiEquivalence, OAI.PolycyclicRecognition.GromovPolynomialGrowthInput

theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_affine_height line 115

Source documentation

The same conclusion directly from the affine-height interface. The specified metric coarse inverses provide all transfer maps and estimates; amenable correction, the height kernel, finiteness and duality are proved in the invoked supporting theorems. The affine estimate and packing remain the two explicit geometric obligations.

theorem recognition_and_lattice_of_affine_height
    (dekimpe : DekimpeLatticeRealizationInput)
    (liFP : LiFinitenessInput) (eaFP : ElementaryAmenableFinitenessInput)
    (liPD : LiDualityInput) (bieri : BieriDualityInput)
    {P H : Type} [Group P] [Group H] [MetricSpace P] [MetricSpace H]
    [IsIsometricSMul P P] [IsIsometricSMul H H] [Group.FG P] [Group.FG H]
    [DiscreteTopology H] [ProperSpace H]
    [MeasurableSpace H] [BorelSpace H] [MeasurableMul H]
    (e : MetricQuasiEquivalence P H) (hP : IsVirtuallyPolycyclic P)
    (hPfinite : ∀ R : ℝ, (Metric.closedBall (1 : P) R).Finite)
    {X W : Type} [PseudoMetricSpace X] [DecidableEq X]
    [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
…