CongruenceFibers.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The uniform bound on successive congruence fibers

A residue modulo 2^(k+1) is determined by its residue modulo 2^k and one binary digit. Applying this to the nine matrix entries bounds every fiber of the special-linear reduction by 2^9, including k=0. No surjectivity or formula for the order of the group is needed.

def OAI.CoarseAssembly.Congruence.topBit line 15
theorem OAI.CoarseAssembly.Congruence.residue_topBit_injective line 19
def OAI.CoarseAssembly.Congruence.matrixTopBits line 34
theorem OAI.CoarseAssembly.Congruence.quotient_fiber_code_injective line 37
theorem OAI.CoarseAssembly.Congruence.card_quotient_fiber_le line 47
Source documentation
Every shallow fiber has at most 512 children.
```
theorem card_quotient_fiber_le (k : ℕ) (q : Quotient k) :
    Fintype.card {x : Quotient (k + 1) // quotientMap (Nat.le_succ k) x = q} ≤ 2 ^ 9 := by
…
```
Mentions: OAI.CoarseAssembly.Congruence.Quotient, OAI.CoarseAssembly.Congruence.quotientMap