TraceSeparation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Trace separation for the congruence-fiber construction

These are elementary ingredients of Lemma 3.1 of A counterexample to the coarse Novikov conjecture (September 23, 2026). No analytic index theorem or property (T) is assumed here. The actual reduction maps are the existing PadicInt.toZModPow maps.

def OAI.CoarseAssembly.diagonalTrace line 24
Source documentation
The trace of diag(t^n,t^(-n),1), expressed using a unit so that the inverse is available in an arbitrary commutative ring.
```
def diagonalTrace (t : Rˣ) (n : ℕ) : R :=
…
```
theorem OAI.CoarseAssembly.diagonalTrace_ne_int line 29
Source documentation
An integral trace would make the positive power of the unit a root of X² + (1-c)X + 1. Thus a transcendental unit has no such trace.
```
theorem diagonalTrace_ne_int (t : Rˣ) (ht : Transcendental ℤ (t : R))
    {n : ℕ} (hn : 0 < n) (c : ℤ) : diagonalTrace t n ≠ (c : R) := by
…
```
Mentions: OAI.CoarseAssembly.diagonalTrace
theorem OAI.CoarseAssembly.reduction_ne_of_le line 56
Source documentation
Once two p-adic integers differ modulo p^m, they differ at every deeper level. This is the compatibility needed by the short-loop argument.
```
theorem reduction_ne_of_le {x y : ℤ_[p]} {m n : ℕ} (hmn : m ≤ n)
    (hxy : PadicInt.toZModPow m x ≠ PadicInt.toZModPow m y) :
    PadicInt.toZModPow n x ≠ PadicInt.toZModPow n y := by
…
```

theorem OAI.CoarseAssembly.exists_reduction_ne line 64

Source documentation

Distinct p-adic integers are separated by some finite quotient.

theorem exists_reduction_ne {x y : ℤ_[p]} (hxy : x ≠ y) :
    ∃ n : ℕ, PadicInt.toZModPow n x ≠ PadicInt.toZModPow n y := by
…

theorem OAI.CoarseAssembly.finite_uniform_reduction_separation line 72

Source documentation

A finite collection of unequal p-adic pairs has one common positive level above which every pair remains separated.

theorem finite_uniform_reduction_separation {ι : Type*} (s : Finset ι)
    (x y : ι → ℤ_[p]) (hxy : ∀ i ∈ s, x i ≠ y i) :
    ∃ N : ℕ, 1 ≤ N ∧ ∀ n, N ≤ n → ∀ i ∈ s,
      PadicInt.toZModPow n (x i) ≠ PadicInt.toZModPow n (y i) := by
…

theorem OAI.CoarseAssembly.finite_trace_separation line 94
Source documentation
The specialization used in the paper: for finitely many integral word traces and a bounded positive exponent, every sufficiently deep congruence quotient separates the diagonal holonomy trace from all the word traces.
For a nonzero signed charge, use its positive absolute value; the diagonal trace is unchanged by reversing the sign.
```
theorem finite_trace_separation (t : ℤ_[p]ˣ)
    (ht : Transcendental ℤ (t : ℤ_[p])) (A : ℕ) (traces : Finset ℤ) :
    ∃ N : ℕ, 1 ≤ N ∧ ∀ n, N ≤ n → ∀ m ∈ Finset.Icc 1 A, ∀ c ∈ traces,
      PadicInt.toZModPow n (diagonalTrace t m) ≠ (c : ZMod (p ^ n)) := by
…
```
Mentions: OAI.CoarseAssembly.diagonalTrace