Pairings.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Four-path pairing identities for the mixed-operator moment argument.

theorem OAI.Problem335.Pairings.coordinate_difference_eq_iff line 13

Source documentation

Equality of differences of coordinate vectors has only the two pairing patterns.

theorem coordinate_difference_eq_iff {α : Type*} (p q r s : α) :
    (Finsupp.single p (1 : ℤ) - Finsupp.single q 1 =
      Finsupp.single r 1 - Finsupp.single s 1) ↔
    (p = q ∧ r = s) ∨ (p = r ∧ q = s) := by
…

theorem OAI.Problem335.Pairings.coordinate_difference_eq_iff_exclusive line 40

Source documentation

The two cases become disjoint when the all-equal case is assigned to normal pairing.

theorem coordinate_difference_eq_iff_exclusive {α : Type*} (p q r s : α) :
    (Finsupp.single p (1 : ℤ) - Finsupp.single q 1 =
      Finsupp.single r 1 - Finsupp.single s 1) ↔
    (p = q ∧ r = s) ∨ (p = r ∧ q = s ∧ p ≠ q) := by
…

inductive OAI.Problem335.Pairings.Kind line 56
Source documentation
Pairing patterns at a layer, with the inequality omitted in the diagonal case.
```
inductive Kind where
…
```
abbrev OAI.Problem335.Pairings.Kind.enumList line 61
theorem OAI.Problem335.Pairings.Kind.enumList_getElem?_ctorIdx_eq line 63
theorem OAI.Problem335.Pairings.Kind.enumList_nodup line 67
instance OAI.Problem335.Pairings.(instance at line 69) line 69
def OAI.Problem335.Pairings.boolKindEquiv line 75
Source documentation
Boolean words use false for the normal pairing and true for the diagonal pairing.
```
def boolKindEquiv : Bool ≃ Kind where
…
```
Mentions: OAI.Problem335.Pairings.Kind
theorem OAI.Problem335.Pairings.boolKindEquiv_false line 83
theorem OAI.Problem335.Pairings.boolKindEquiv_true line 84
structure OAI.Problem335.Pairings.Labels line 88
Source documentation
The four labels contributed by the four paths at a single vertex.
```
structure Labels (α : Type*) where
…
```
def OAI.Problem335.Pairings.Respects line 95
instance OAI.Problem335.Pairings.(instance at line 99) line 99
def OAI.Problem335.Pairings.ExactRespects line 104
Source documentation
The exact (disjoint) pairing classes before relaxing the diagonal inequality.
```
def ExactRespects {α : Type*} : Kind → Labels α → Prop
  | .normal, x => x.p = x.q ∧ x.r = x.s
  | .diagonal, x => x.p = x.r ∧ x.q = x.s ∧ x.p ≠ x.q
```
Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Labels
theorem OAI.Problem335.Pairings.ExactRespects.respects line 108
theorem OAI.Problem335.Pairings.exactRespects_unique line 115
Source documentation
No compatible coordinate quadruple belongs to both exact pairing classes.
```
theorem exactRespects_unique {α : Type*} {τ σ : Kind} {x : Labels α}
    (hτ : ExactRespects τ x) (hσ : ExactRespects σ x) : τ = σ := by
…
```
Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.ExactRespects
theorem OAI.Problem335.Pairings.coordinate_difference_eq_iff_existsUnique line 120
Source documentation
Every compatible coordinate quadruple has a unique exact pairing type.
```
theorem coordinate_difference_eq_iff_existsUnique {α : Type*} (x : Labels α) :
    (Finsupp.single x.p (1 : ℤ) - Finsupp.single x.q 1 =
      Finsupp.single x.r 1 - Finsupp.single x.s 1) ↔
    ∃! τ : Kind, ExactRespects τ x := by
…
```
Mentions: OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.ExactRespects
abbrev OAI.Problem335.Pairings.Vertex line 135
Source documentation
Labels allowed by both adjacent layers.
```
abbrev Vertex (α : Type*) (τ σ : Kind) :=
…
```
Mentions: OAI.Problem335.Pairings.Kind
def OAI.Problem335.Pairings.normalVertexEquiv line 138
def OAI.Problem335.Pairings.diagonalVertexEquiv line 147
def OAI.Problem335.Pairings.mixedVertexEquiv line 156
def OAI.Problem335.Pairings.swapVertexEquiv line 165
theorem OAI.Problem335.Pairings.card_vertex line 172
Source documentation
Equal pairings give two independent labels; different pairings give one.
```
theorem card_vertex (α : Type*) [Fintype α] [DecidableEq α] (τ σ : Kind) :
    Fintype.card (Vertex α τ σ) =
      Fintype.card α ^ (if τ = σ then 2 else 1) := by
…
```
Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Vertex
def OAI.Problem335.Pairings.adjacentSwitches line 183
Source documentation
Number of interfaces at which a word changes its letter.
```
def adjacentSwitches {β : Type*} [DecidableEq β] {L : ℕ}
    (τ : Fin (L + 1) → β) : ℕ :=
…
```

theorem OAI.Problem335.Pairings.adjacentSwitches_comp_injective line 188

Source documentation

Relabeling letters injectively preserves the number of switches.

theorem adjacentSwitches_comp_injective {β γ : Type*} [DecidableEq β] [DecidableEq γ]
    {L : ℕ} (τ : Fin (L + 1) → β) (f : β → γ) (hf : Function.Injective f) :
    adjacentSwitches (fun i => f (τ i)) = adjacentSwitches τ := by
…

Mentions: OAI.Problem335.Pairings.adjacentSwitches

theorem OAI.Problem335.Pairings.free_label_exponent line 198

Source documentation

Each unchanged interface has two free labels, and each changed interface has one.

theorem free_label_exponent {β : Type*} [DecidableEq β] {L : ℕ}
    (τ : Fin (L + 1) → β) :
    (∑ i : Fin L, if τ i.castSucc = τ i.succ then 2 else 1) =
      2 * L - adjacentSwitches τ := by
…

Mentions: OAI.Problem335.Pairings.adjacentSwitches

abbrev OAI.Problem335.Pairings.Assignments line 215
Source documentation
The relaxed four-path assignments factor as a product over internal vertices.
```
abbrev Assignments (α : Type*) {L : ℕ} (τ : Fin (L + 1) → Kind) :=
…
```
Mentions: OAI.Problem335.Pairings.Kind
theorem OAI.Problem335.Pairings.card_assignments line 219
Source documentation
Exact unweighted count of relaxed assignments for a fixed pairing word.
```
theorem card_assignments (α : Type*) [Fintype α] [DecidableEq α]
    {L : ℕ} (τ : Fin (L + 1) → Kind) :
    Fintype.card (Assignments α τ) =
      Fintype.card α ^ (2 * L - adjacentSwitches τ) := by
…
```
Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Assignments, OAI.Problem335.Pairings.adjacentSwitches