PairingLabels.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Disjoint labels for the pairing test

The cycle classes of one perfect matching index disjoint label pools. This isolates that matching while allowing the labels of same-side pairs to vary.

abbrev OAI.KadisonSimilarity.PerfectMatching line 18
Source documentation
A perfect matching represented by its fixed-point-free involution.
```
abbrev PerfectMatching (ι : Type*) :=
…
```
instance OAI.KadisonSimilarity.perfectMatchingFintype line 21
theorem OAI.KadisonSimilarity.sameCycle_perfectMatching_iff line 25
Source documentation
A cycle of a matching has exactly its two paired vertices.
```
theorem sameCycle_perfectMatching_iff (P : PerfectMatching ι) (i j : ι) :
    P.1.SameCycle i j ↔ j = i ∨ j = P.1 i := by
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching
def OAI.KadisonSimilarity.pairingLabelKernel line 44
Source documentation
On orthonormal labels, a pairing contraction is the product of equality indicators along its pairs. Repeating an indicator has no effect.
```
def pairingLabelKernel {J : Type*} [DecidableEq J]
    (P : PerfectMatching ι) (labels : ι → J) : ℂ :=
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching

theorem OAI.KadisonSimilarity.pairingLabelKernel_isolate line 49

Source documentation

Labels identifying exactly the pairs of P kill every other matching.

theorem pairingLabelKernel_isolate {J : Type*} [DecidableEq J]
    (P Q : PerfectMatching ι) (labels : ι → J)
    (hlabels : ∀ i j, labels i = labels j ↔ j = i ∨ j = P.1 i) :
    pairingLabelKernel Q labels = if Q = P then 1 else 0 := by
…

Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.pairingLabelKernel

def OAI.KadisonSimilarity.IsSourcePairClass line 75
Source documentation
A pair is entirely in the source precisely when its cycle contains no test slot.
```
def IsSourcePairClass (P : PerfectMatching (Fin k ⊕ Fin l))
    (q : PermutationCycles P.1) : Prop :=
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.PermutationCycles
def OAI.KadisonSimilarity.IsTestPairClass line 80
Source documentation
A pair is entirely in the test precisely when its cycle contains no source slot.
```
def IsTestPairClass (P : PerfectMatching (Fin k ⊕ Fin l))
    (q : PermutationCycles P.1) : Prop :=
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.PermutationCycles
abbrev OAI.KadisonSimilarity.SourcePairClasses line 84
abbrev OAI.KadisonSimilarity.TestPairClasses line 87
instance OAI.KadisonSimilarity.sourcePairClassDecidable line 90
instance OAI.KadisonSimilarity.testPairClassDecidable line 93
instance OAI.KadisonSimilarity.sourcePairClassesFintype line 96
instance OAI.KadisonSimilarity.testPairClassesFintype line 99
def OAI.KadisonSimilarity.sourcePairLabels line 104
Source documentation
The source tuple uses a variable label on each source-source pair and a fixed label on each source-test pair. The cycle class separates the pools.
```
def sourcePairLabels (P : PerfectMatching (Fin k ⊕ Fin l)) {M : ℕ}
    (f : SourcePairClasses P → Fin M) (i : Fin k) : PermutationCycles P.1 × ℕ :=
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.SourcePairClasses, OAI.KadisonSimilarity.PermutationCycles
def OAI.KadisonSimilarity.testPairLabels line 110
Source documentation
The analogous tuple on the test side.
```
def testPairLabels (P : PerfectMatching (Fin k ⊕ Fin l)) {M : ℕ}
    (g : TestPairClasses P → Fin M) (j : Fin l) : PermutationCycles P.1 × ℕ :=
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.TestPairClasses, OAI.KadisonSimilarity.PermutationCycles
theorem OAI.KadisonSimilarity.sourcePairLabels_injective line 115
theorem OAI.KadisonSimilarity.testPairLabels_injective line 129
def OAI.KadisonSimilarity.allPairLabels line 143
theorem OAI.KadisonSimilarity.allPairLabels_source line 150
theorem OAI.KadisonSimilarity.allPairLabels_test line 156
theorem OAI.KadisonSimilarity.pairLabels_eq_iff line 163
Source documentation
The combined source and test tuples identify exactly the chosen pairs.
```
theorem pairLabels_eq_iff (P : PerfectMatching (Fin k ⊕ Fin l)) {M : ℕ}
    (f : SourcePairClasses P → Fin M) (g : TestPairClasses P → Fin M)
    (s t : Fin k ⊕ Fin l) :
    Sum.elim (sourcePairLabels P f) (testPairLabels P g) s =
        Sum.elim (sourcePairLabels P f) (testPairLabels P g) t ↔
      t = s ∨ t = P.1 s := by
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.SourcePairClasses, OAI.KadisonSimilarity.TestPairClasses, OAI.KadisonSimilarity.sourcePairLabels, OAI.KadisonSimilarity.testPairLabels
theorem OAI.KadisonSimilarity.sourcePairClass_of_source_pair line 183
Source documentation
A source-source pair supplies a source-only cycle class.
```
theorem sourcePairClass_of_source_pair (P : PerfectMatching (Fin k ⊕ Fin l))
    (i i' : Fin k) (hp : P.1 (Sum.inl i) = Sum.inl i') :
    IsSourcePairClass P (⟦Sum.inl i⟧ : PermutationCycles P.1) := by
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.IsSourcePairClass, OAI.KadisonSimilarity.PermutationCycles
theorem OAI.KadisonSimilarity.testPairClass_of_test_pair line 192
Source documentation
The analogous implication for a test-test pair.
```
theorem testPairClass_of_test_pair (P : PerfectMatching (Fin k ⊕ Fin l))
    (j j' : Fin l) (hp : P.1 (Sum.inr j) = Sum.inr j') :
    IsTestPairClass P (⟦Sum.inr j⟧ : PermutationCycles P.1) := by
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.IsTestPairClass, OAI.KadisonSimilarity.PermutationCycles
theorem OAI.KadisonSimilarity.isCrossPairing_of_no_same_side line 201
Source documentation
If there are no same-side cycle classes, every pair crosses the two sides.
```
theorem isCrossPairing_of_no_same_side (P : PerfectMatching (Fin k ⊕ Fin l))
    (hS : Fintype.card (SourcePairClasses P) = 0)
    (hT : Fintype.card (TestPairClasses P) = 0) : IsCrossPairing P.1 := by
…
```
Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.SourcePairClasses, OAI.KadisonSimilarity.TestPairClasses, OAI.KadisonSimilarity.IsCrossPairing