TraceObstruction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Matrix trace separation in the congruence quotients

The elementary p-adic separation result is connected here to the actual SL₃ matrices and to the closed-walk holonomy identity.

theorem OAI.CoarseAssembly.Congruence.trace_holonomy_pow line 17
Source documentation
The finite matrix trace is the reduction of the p-adic Laurent trace.
```
theorem trace_holonomy_pow (t : ℤ_[2]ˣ) (k m : ℕ) :
    Matrix.trace ((holonomy t k ^ m : Quotient k) : Matrix (Fin 3) (Fin 3) (ZMod (2 ^ k))) =
      PadicInt.toZModPow k (diagonalTrace t m) := by
…
```
Mentions: OAI.CoarseAssembly.Congruence.holonomy, OAI.CoarseAssembly.Congruence.Quotient, OAI.CoarseAssembly.diagonalTrace
theorem OAI.CoarseAssembly.Congruence.trace_holonomy_natAbs line 25
Source documentation
The two nontrivial diagonal entries are exchanged when the charge is negated, so the trace only depends on its absolute value.
```
theorem trace_holonomy_natAbs (t : ℤ_[2]ˣ) (k : ℕ) (m : ℤ) :
    Matrix.trace ((holonomy t k ^ m : Quotient k) : Matrix (Fin 3) (Fin 3) (ZMod (2 ^ k))) =
    Matrix.trace ((holonomy t k ^ m.natAbs : Quotient k) :
      Matrix (Fin 3) (Fin 3) (ZMod (2 ^ k))) := by
…
```
Mentions: OAI.CoarseAssembly.Congruence.holonomy, OAI.CoarseAssembly.Congruence.Quotient

theorem OAI.CoarseAssembly.Congruence.matrix_trace_separation line 47

Source documentation

Simultaneous trace separation from a finite set of integral word traces, now stated for the actual finite special linear groups.

theorem matrix_trace_separation (t : ℤ_[2]ˣ)
    (ht : Transcendental ℤ (t : ℤ_[2])) (A : ℕ) (traces : Finset ℤ) :
    ∃ N : ℕ, 1 ≤ N ∧ ∀ k, N ≤ k → ∀ m ∈ Finset.Icc 1 A,
      ∀ w : ArithmeticGroup, Matrix.trace (w : Matrix (Fin 3) (Fin 3) ℤ) ∈ traces →
        Matrix.trace ((holonomy t k ^ m : Quotient k) : Matrix (Fin 3) (Fin 3) (ZMod (2 ^ k))) ≠
          Matrix.trace (reduce k w : Matrix (Fin 3) (Fin 3) (ZMod (2 ^ k))) := by
…

Mentions: OAI.CoarseAssembly.Congruence.ArithmeticGroup, OAI.CoarseAssembly.Congruence.holonomy, OAI.CoarseAssembly.Congruence.Quotient, OAI.CoarseAssembly.Congruence.reduce

theorem OAI.CoarseAssembly.Congruence.closed_walk_trace line 61
Source documentation
A closed word in a finite quotient forces equality of the concrete matrix traces. This is the contradiction paired with separation above.
```
theorem closed_walk_trace (t : ℤ_[2]ˣ) (k : ℕ) (z : Quotient k)
    (steps : List (Quotient k × ℤ))
    (hclosed : holonomyEndpoint (holonomy t k) steps z = z) :
    Matrix.trace ((holonomy t k ^ holonomyCharge steps : Quotient k) :
      Matrix (Fin 3) (Fin 3) (ZMod (2 ^ k))) =
    Matrix.trace (((holonomyWord steps)⁻¹ : Quotient k) : Matrix (Fin 3) (Fin 3) (ZMod (2 ^ k))) :=
…
```
Mentions: OAI.CoarseAssembly.Congruence.Quotient, OAI.CoarseAssembly.holonomyEndpoint, OAI.CoarseAssembly.Congruence.holonomy, OAI.CoarseAssembly.holonomyCharge, OAI.CoarseAssembly.holonomyWord