ConditionalRecognition.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quasi-isometric recognition from precisely stated published inputs

Geometric height bounds, smoothing, finite labels, and finiteness/duality transfer reduce recognition to the elementary-amenable finiteness and polynomial-growth hypotheses of PublishedRecognitionInputs.

theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_published_inputs line 29

Source documentation

The recognition and finite-index lattice conclusions for metrics comparable to word metrics. Only the original comparison group needs an explicit linear-chain witness; the target's given quasi-equivalence is used directly.

theorem recognition_and_lattice_of_published_inputs
    (inputs : PublishedRecognitionInputs)
    {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),
…

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