PublishedRecognitionInputs.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Explicit published hypotheses for the recognition theorem

The hypotheses are elementary-amenable finiteness and polynomial-growth recognition. The geometric height bounds, unimodularity, reduced cohomology, and lattice realization are established independently.

structure OAI.PolycyclicRecognition.PublishedRecognitionInputs line 43
Source documentation
The cited theorem families, specialized by the proof to its chosen models. Gromov is retained solely as the polynomial-growth theorem.
```
structure PublishedRecognitionInputs : Prop where
…
```
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.dekimpe line 49
Source documentation
Nilpotent kernel completion and the invariant graph prove the required connected solvable lattice realization, including nonsplit extensions.
```
theorem PublishedRecognitionInputs.dekimpe (_h : PublishedRecognitionInputs) :
    DekimpeLatticeRealizationInput := dekimpeLatticeRealizationInput
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.DekimpeLatticeRealizationInput, OAI.PolycyclicRecognition.dekimpeLatticeRealizationInput
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.triangulable line 55
Source documentation
The compact rotational modification and its analytic triangular realization supply all three proper cocompact comparison arrows.
```
theorem PublishedRecognitionInputs.triangulable (_h : PublishedRecognitionInputs) :
    CornulierTesseraModelInput := cornulierTesseraModelInput
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.CornulierTesseraModelInput, OAI.PolycyclicRecognition.cornulierTesseraModelInput
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.liFiniteness line 59
Source documentation
Controlled cycle fillings and finite projective covers prove FP transfer.
```
theorem PublishedRecognitionInputs.liFiniteness (_h : PublishedRecognitionInputs) :
    LiFinitenessInput := liFinitenessInput
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.LiFinitenessInput, OAI.PolycyclicRecognition.liFinitenessInput
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.liDuality line 63
Source documentation
Controlled cochains and finite-resolution truncation prove duality transfer.
```
theorem PublishedRecognitionInputs.liDuality (_h : PublishedRecognitionInputs) :
    LiDualityInput := liDualityInput
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.LiDualityInput, OAI.PolycyclicRecognition.liDualityInput
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.bieriDuality line 67
Source documentation
Rational top classes and integral finiteness prove the solvable PD endgame.
```
theorem PublishedRecognitionInputs.bieriDuality (_h : PublishedRecognitionInputs) :
    BieriDualityInput := bieriDualityInput
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.BieriDualityInput, OAI.PolycyclicRecognition.bieriDualityInput
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.farbWeinberger line 72
Source documentation
The required solvable-lattice polycyclicity is proved using lifted complex adjoint weights and the discrete nilpotent kernel, including rotational factors.
```
theorem PublishedRecognitionInputs.farbWeinberger (_h : PublishedRecognitionInputs) :
    FarbWeinbergerLatticeInput := isPolycyclic_uniformLattice_solvableLieGroup
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.FarbWeinbergerLatticeInput, OAI.PolycyclicRecognition.isPolycyclic_uniformLattice_solvableLieGroup
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.nilpotent line 76
Source documentation
The finite BCH, nilpotent model, integration and Haar inputs are proved.
```
theorem PublishedRecognitionInputs.nilpotent (_h : PublishedRecognitionInputs) :
    NilpotentPublishedInputs := nilpotentPublishedInputs
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.NilpotentPublishedInputs, OAI.PolycyclicRecognition.nilpotentPublishedInputs
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.remez line 80
Source documentation
Interpolation and slicing give the fixed-power polynomial estimate.
```
theorem PublishedRecognitionInputs.remez (_h : PublishedRecognitionInputs) :
    RemezPolynomialInput := remezPolynomialInput
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.RemezPolynomialInput, OAI.PolycyclicRecognition.remezPolynomialInput
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.differential line 84
Source documentation
The actual matrix Lie derivative is constructed from continuity.
```
theorem PublishedRecognitionInputs.differential (_h : PublishedRecognitionInputs) :
    MatrixLieDifferentialInput := matrixLieDifferentialInput
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.MatrixLieDifferentialInput, OAI.PolycyclicRecognition.matrixLieDifferentialInput
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.torsionFree line 88
Source documentation
Cyclic-series induction proves the finite-index torsion-free comparison.
```
theorem PublishedRecognitionInputs.torsionFree (_h : PublishedRecognitionInputs) :
    PolycyclicTorsionFreeIndexInput := polycyclicTorsionFreeIndexInput
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.PolycyclicTorsionFreeIndexInput, OAI.PolycyclicRecognition.polycyclicTorsionFreeIndexInput
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.metric line 92
Source documentation
Compatible proper chain metrics are constructed from compact generation.
```
theorem PublishedRecognitionInputs.metric (_h : PublishedRecognitionInputs) :
    GeodesicMetricExistenceInput := geodesicMetricExistenceInput
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.GeodesicMetricExistenceInput, OAI.PolycyclicRecognition.geodesicMetricExistenceInput
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.riemannian line 96
Source documentation
The invariant Riemannian metric, minimizing paths and coordinate bounds are constructed.
```
theorem PublishedRecognitionInputs.riemannian (_h : PublishedRecognitionInputs) :
    LieRiemannianMetricInput := lieRiemannianMetricInput
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.LieRiemannianMetricInput, OAI.PolycyclicRecognition.lieRiemannianMetricInput
theorem OAI.PolycyclicRecognition.PublishedRecognitionInputs.linearRealization line 101
Source documentation
The intrinsic height kernel gives the inducing triangular realization without an exponential-chart hypothesis.
```
theorem PublishedRecognitionInputs.linearRealization (_h : PublishedRecognitionInputs)
    (R : SimplyConnectedSolvableLieModel) (d : ProperChainMetric R.carrier) :
    letI := d.compatibleMetric
…
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.ProperChainMetric