Main.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform congruence homology vanishing and the complete bounded-degree coboundary-expander theorem.

theorem OAI.CoboundaryExpanders.uniform_u_homology line 19

Source documentation

A single prime threshold supplies all the finitely many ambient U-ranks needed in an inductive homology argument.

theorem uniform_u_homology (N : ℕ) :
    ∃ Q : ℕ, ∀ (p : ℕ) [Fact p.Prime], Odd p → Q < p →
      ∀ a : ℕ, 4 ≤ a → a ≤ N → ∀ j : ℕ, 0 < j → j < a-2 →
        IsZero (groupHomology (Rep.trivial (ZMod 2) (U p a) (ZMod 2)) j) := by
…

theorem OAI.CoboundaryExpanders.gamma_vanishing_of_u line 42

Source documentation

The actual congruence-group vanishing follows by induction on homological degree, using the ordinary partial-basis edge argument and odd-index transfer. This does not assume integral pro-stability or a stability theorem.

theorem gamma_vanishing_of_u (p N : ℕ) [Fact p.Prime] (hp : Odd p)
    (hU : ∀ a : ℕ, 4 ≤ a → a ≤ N → ∀ j : ℕ, 0 < j → j < a-2 →
      IsZero (groupHomology (Rep.trivial (ZMod 2) (U p a) (ZMod 2)) j)) :
    ∀ j : ℕ, 0 < j → ∀ a : ℕ, 2*j+2 ≤ a → a ≤ N →
      ∀ m : ℕ, 1 ≤ m →
        IsZero (groupHomology (Rep.trivial (ZMod 2) (Gamma p a m) (ZMod 2)) j) := by
…

theorem OAI.CoboundaryExpanders.uniform_gamma_vanishing line 63

Source documentation

Consequently, for sufficiently large odd primes the literal congruence homology vanishes simultaneously in the finite rank window required by d.

theorem uniform_gamma_vanishing (N : ℕ) :
    ∃ Q : ℕ, ∀ (p : ℕ) [Fact p.Prime], Odd p → Q < p →
      ∀ j : ℕ, 0 < j → ∀ a : ℕ, 2*j+2 ≤ a → a ≤ N →
        ∀ m : ℕ, 1 ≤ m →
          IsZero (groupHomology (Rep.trivial (ZMod 2) (Gamma p a m) (ZMod 2)) j) := by
…

theorem OAI.CoboundaryExpanders.proZero_of_target_vanishing line 73
Source documentation
Zero target homology makes every actual stabilization cokernel zero, including its literal transition map.
```
theorem proZero_of_target_vanishing (p a j : ℕ)
    (hz : ∀ m : ℕ, 1 ≤ m →
      IsZero (groupHomology (Rep.trivial (ZMod 2) (Gamma p (a+1) m) (ZMod 2)) j)) :
    CongruenceCokernels.ProZero p a j := by
…
```
Mentions: OAI.CoboundaryExpanders.CongruenceCokernels.ProZero
theorem OAI.CoboundaryExpanders.main line 88
Source documentation
The manuscript's full theorem, with one positive weighted coboundary expansion constant in ALL degrees below d and all members of the family.
Distinct definitions of this name: ComparatorChallenges/CoboundaryExpanders.lean:91 (same statement text; different proof or body). Qualify references as OAI.CoboundaryExpanders.main@path.
```
theorem main : MainStatement := by
…
```
Mentions: OAI.CoboundaryExpanders.MainStatement