InvariantCycles.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Removing centered singleton cycles

A fixed point contributes the trace of its matrix argument. Factorization of the coordinate contraction shows that vanishing on centered singleton tails does not require an additional invariant-theory input.

def OAI.KadisonSimilarity.fixedPointComplement line 21

Source documentation

A permutation fixing i preserves the complement of i.

def fixedPointComplement (π : Equiv.Perm ι) (i : ι) (hi : π i = i)
    (j : {j : ι // j ≠ i}) : {j : ι // j ≠ i} :=
…

def OAI.KadisonSimilarity.fixedPointRemainder line 26
Source documentation
The contraction over all slots except a distinguished fixed point.
```
def fixedPointRemainder (π : Equiv.Perm ι) (i : ι) (hi : π i = i)
    (v : ι → Matrix α α ℂ) : ℂ :=
…
```
theorem OAI.KadisonSimilarity.permutationContraction_fixedPoint line 32
Source documentation
A fixed point contributes precisely an unnormalized trace factor.
```
theorem permutationContraction_fixedPoint (π : Equiv.Perm ι) (i : ι) (hi : π i = i)
    (v : ι → Matrix α α ℂ) :
    permutationContraction π v = Matrix.trace (v i) * fixedPointRemainder π i hi v := by
…
```
Mentions: OAI.KadisonSimilarity.permutationContraction, OAI.KadisonSimilarity.fixedPointRemainder

theorem OAI.KadisonSimilarity.permutationContraction_eq_zero_of_fixed_centered line 52

Source documentation

Any singleton cycle on a centered variable vanishes identically.

theorem permutationContraction_eq_zero_of_fixed_centered
    (π : Equiv.Perm ι) (i : ι) (hi : π i = i)
    (v : ι → Matrix α α ℂ) (hcenter : Matrix.trace (v i) = 0) :
    permutationContraction π v = 0 := by
…

Mentions: OAI.KadisonSimilarity.permutationContraction

theorem OAI.KadisonSimilarity.normalizedPermutationContraction_eq_zero_of_fixed_centered line 59

Source documentation

The same deletion holds for the normalized cycle forms.

theorem normalizedPermutationContraction_eq_zero_of_fixed_centered
    (π : Equiv.Perm ι) (i : ι) (hi : π i = i)
    (v : ι → Matrix α α ℂ) (hcenter : Matrix.trace (v i) = 0) :
    normalizedPermutationContraction π v = 0 := by
…

Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction

theorem OAI.KadisonSimilarity.invariant_expansion_remove_centered_singletons line 68

Source documentation

On centered tail variables, only permutations without a tail fixed point contribute. The endpoint slot is exempt from centering.

theorem invariant_expansion_remove_centered_singletons
    (i₀ : ι) (v : ι → Matrix α α ℂ)
    (hcenter : ∀ i, i ≠ i₀ → Matrix.trace (v i) = 0)
    (c : Equiv.Perm ι → ℂ) :
    (∑ π, c π * normalizedPermutationContraction π v) =
      ∑ π ∈ Finset.univ.filter (fun π => ∀ i, π i = i → i = i₀),
        c π * normalizedPermutationContraction π v := by
…

Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction

abbrev OAI.KadisonSimilarity.PermutationCycles line 91
Source documentation
The finite set of cycles of a permutation, including fixed points.
```
abbrev PermutationCycles (π : Equiv.Perm ι) :=
…
```
instance OAI.KadisonSimilarity.permutationCyclesFintype line 94
instance OAI.KadisonSimilarity.permutationCyclesDecidableEq line 97
abbrev OAI.KadisonSimilarity.CycleMembers line 101
Source documentation
The vertices in one cycle.
```
abbrev CycleMembers (π : Equiv.Perm ι) (q : PermutationCycles π) :=
…
```
Mentions: OAI.KadisonSimilarity.PermutationCycles
instance OAI.KadisonSimilarity.cycleMembersFintype line 104
theorem OAI.KadisonSimilarity.sum_cycleLengths line 109
Source documentation
Cycle lengths sum to the number of slots.
```
theorem sum_cycleLengths (π : Equiv.Perm ι) :
    (∑ q : PermutationCycles π, Fintype.card (CycleMembers π q)) = Fintype.card ι := by
…
```
Mentions: OAI.KadisonSimilarity.PermutationCycles, OAI.KadisonSimilarity.CycleMembers
theorem OAI.KadisonSimilarity.card_permutationCycles line 116
theorem OAI.KadisonSimilarity.cycleLength_pos line 121
theorem OAI.KadisonSimilarity.two_le_cycleLength line 128
Source documentation
A cycle containing no fixed point has at least two vertices.
```
theorem two_le_cycleLength (π : Equiv.Perm ι) (q : PermutationCycles π)
    (hfixed : ∀ i, (⟦i⟧ : PermutationCycles π) = q → π i ≠ i) :
    2 ≤ Fintype.card (CycleMembers π q) := by
…
```
Mentions: OAI.KadisonSimilarity.PermutationCycles, OAI.KadisonSimilarity.CycleMembers
theorem OAI.KadisonSimilarity.cycleLength_fixedPoint line 142
Source documentation
A fixed point forms a cycle of length one.
```
theorem cycleLength_fixedPoint (π : Equiv.Perm ι) (i : ι) (hi : π i = i) :
    Fintype.card (CycleMembers π (⟦i⟧ : PermutationCycles π)) = 1 := by
…
```
Mentions: OAI.KadisonSimilarity.CycleMembers, OAI.KadisonSimilarity.PermutationCycles
theorem OAI.KadisonSimilarity.cycle_threshold_fixes_endpoint line 151
Source documentation
The cycle threshold forces the distinguished endpoint to be fixed. The only other assumption is the already justified removal of tail singletons.
```
theorem cycle_threshold_fixes_endpoint (π : Equiv.Perm ι) (i₀ : ι)
    (hfixed : ∀ i, π i = i → i = i₀)
    (hcount : Fintype.card ι + 1 ≤ 2 * permutationCycleCount π) : π i₀ = i₀ := by
…
```
Mentions: OAI.KadisonSimilarity.permutationCycleCount
theorem OAI.KadisonSimilarity.sum_endpoint_weights line 170

theorem OAI.KadisonSimilarity.cycle_threshold_lengths line 187

Source documentation

At the threshold, every nondistinguished cycle has length two.

theorem cycle_threshold_lengths (π : Equiv.Perm ι) (i₀ : ι)
    (hfixed : ∀ i, π i = i → i = i₀)
    (hcount : Fintype.card ι + 1 ≤ 2 * permutationCycleCount π) :
    ∀ q : PermutationCycles π,
      Fintype.card (CycleMembers π q) = if q = ⟦i₀⟧ then 1 else 2 := by
…

Mentions: OAI.KadisonSimilarity.permutationCycleCount, OAI.KadisonSimilarity.PermutationCycles, OAI.KadisonSimilarity.CycleMembers

theorem OAI.KadisonSimilarity.involutive_of_cycleLengths_le_two line 220
Source documentation
If all permutation cycles have at most two elements, the permutation is an involution. This follows by putting three successive vertices in one fiber.
```
theorem involutive_of_cycleLengths_le_two (π : Equiv.Perm ι)
    (hsize : ∀ q : PermutationCycles π, Fintype.card (CycleMembers π q) ≤ 2) :
    Function.Involutive π := by
…
```
Mentions: OAI.KadisonSimilarity.PermutationCycles, OAI.KadisonSimilarity.CycleMembers

theorem OAI.KadisonSimilarity.cycle_threshold_pairing line 246

Source documentation

The surviving cycle structures are precisely an endpoint singleton and a fixed-point-free involution on the tail slots.

theorem cycle_threshold_pairing (π : Equiv.Perm ι) (i₀ : ι)
    (hfixed : ∀ i, π i = i → i = i₀)
    (hcount : Fintype.card ι + 1 ≤ 2 * permutationCycleCount π) :
    π i₀ = i₀ ∧ Function.Involutive π ∧ ∀ i, i ≠ i₀ → π i ≠ i := by
…

Mentions: OAI.KadisonSimilarity.permutationCycleCount

def OAI.KadisonSimilarity.EndpointPairing line 259
Source documentation
The cycle structure remaining after the endpoint and centering estimates.
```
def EndpointPairing (π : Equiv.Perm ι) (i₀ : ι) : Prop :=
…
```
instance OAI.KadisonSimilarity.endpointPairingDecidable line 262

theorem OAI.KadisonSimilarity.invariant_expansion_reduce_to_pairings line 270

Source documentation

Combining coefficient decay with centered-singleton deletion reduces the finite invariant expansion to pairings of all tail slots. The coefficient vanishing premise is supplied by the proved matrix-test limit theorem.

theorem invariant_expansion_reduce_to_pairings
    (i₀ : ι) (v : ι → Matrix α α ℂ)
    (hcenter : ∀ i, i ≠ i₀ → Matrix.trace (v i) = 0)
    (c : Equiv.Perm ι → ℂ)
    (hsmall : ∀ π, 2 * permutationCycleCount π < Fintype.card ι + 1 → c π = 0) :
    (∑ π, c π * normalizedPermutationContraction π v) =
      ∑ π ∈ Finset.univ.filter (fun π => EndpointPairing π i₀),
        c π * normalizedPermutationContraction π v := by
…

Mentions: OAI.KadisonSimilarity.permutationCycleCount, OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.EndpointPairing

def OAI.KadisonSimilarity.IsCrossPairing line 298
Source documentation
Every tail pair joins one source slot to one test slot.
```
def IsCrossPairing {k l : ℕ} (π : Equiv.Perm (Fin k ⊕ Fin l)) : Prop :=
…
```
def OAI.KadisonSimilarity.crossPairingEquiv line 303
Source documentation
A cross pairing determines the bijection indexing its contraction.
```
def crossPairingEquiv {k l : ℕ} (π : Equiv.Perm (Fin k ⊕ Fin l))
    (hπ : Function.Involutive π) (hcross : IsCrossPairing π) : Fin k ≃ Fin l where
…
```
Mentions: OAI.KadisonSimilarity.IsCrossPairing
theorem OAI.KadisonSimilarity.degrees_eq_of_crossPairing line 317
Source documentation
Cross pairings exist only when the source and test degrees coincide.
```
theorem degrees_eq_of_crossPairing {k l : ℕ} (π : Equiv.Perm (Fin k ⊕ Fin l))
    (hπ : Function.Involutive π) (hcross : IsCrossPairing π) : k = l := by
…
```
Mentions: OAI.KadisonSimilarity.IsCrossPairing