KazhdanInput.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The fixed published spectral-gap input

The elementary matrices below and their inverses give a fixed finite symmetric generating set of SL3(Z), with the identity included. The input used in the conditional development is exactly the uniform lazy-averaging estimate on the finite congruence quotients, with the standard ample coefficient space. It is the specialization of Bekka–de la Harpe–Valette (2008), Proposition 1.3.2 and Example 1.7.4, explained in manuscript §5.2.

No proof of that published input is asserted during the conditional phase. The spatial Roe transfer itself is proved from it below.

theorem OAI.CoarseAssembly.elementaryMoves_nonempty line 25
theorem OAI.CoarseAssembly.elementaryMoves_symmetric line 28
def OAI.CoarseAssembly.PublishedKazhdanInput line 31
theorem OAI.CoarseAssembly.roe_transfer_of_published_gap line 35
Source documentation
The transfer in manuscript §5 for the fixed graph family, conditional only on its identified published spectral-gap input.
```
theorem roe_transfer_of_published_gap (hgap : PublishedKazhdanInput) :
    letI : MetricSpace VertexUnion := vertexUnionMetric elementaryMoves chosenHolonomyUnit
…
```
Mentions: OAI.CoarseAssembly.PublishedKazhdanInput, OAI.CoarseAssembly.VertexUnion, OAI.CoarseAssembly.vertexUnionMetric, OAI.CoarseAssembly.elementaryMoves