PairingShifts.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.Pairings.layerShift line 12
Source documentation
A signed coordinate in every layer, as used by the mixed IMM operator.
```
def layerShift {ι α : Type*} [Fintype ι]
    (sign : ι → ℤ) (coordinate : ι → α) : (ι × α) →₀ ℤ :=
…
```
theorem OAI.Problem335.Pairings.layerShift_apply line 17
theorem OAI.Problem335.Pairings.layerShift_injective line 24
Source documentation
Nonzero signed layer coordinates determine the entire coordinate sequence.
```
theorem layerShift_injective {ι α : Type*} [Fintype ι]
    (sign : ι → ℤ) (hsign : ∀ i, sign i ≠ 0) :
    Function.Injective (layerShift (α := α) sign) := by
…
```
Mentions: OAI.Problem335.Pairings.layerShift

theorem OAI.Problem335.Pairings.weighted_coordinate_difference_eq_iff line 35

Source documentation

A common nonzero signed coefficient does not change the pairing classification.

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

def OAI.Problem335.Pairings.layerProjection line 46
Source documentation
Restrict a finitely supported coordinate vector to one matrix layer.
```
def layerProjection {ι α : Type*} (i : ι) : ((ι × α) →₀ ℤ) →+ (α →₀ ℤ) :=
…
```
theorem OAI.Problem335.Pairings.layerProjection_layerShift line 51

theorem OAI.Problem335.Pairings.layerShift_difference_eq_iff line 61

Source documentation

The four-shift compatibility condition holds independently in every layer.

theorem layerShift_difference_eq_iff {ι α : Type*} [Fintype ι]
    (sign : ι → ℤ) (hsign : ∀ i, sign i ≠ 0) (p q r s : ι → α) :
    (layerShift sign p - layerShift sign q = layerShift sign r - layerShift sign s) ↔
    ∀ i, (p i = q i ∧ r i = s i) ∨ (p i = r i ∧ q i = s i) := by
…

Mentions: OAI.Problem335.Pairings.layerShift

def OAI.Problem335.Pairings.edgeCoordinates line 78
Source documentation
Edges of a path with at least one edge.
```
def edgeCoordinates {α : Type*} {L : ℕ} (P : Fin (L + 2) → α)
    (i : Fin (L + 1)) : α × α :=
…
```
theorem OAI.Problem335.Pairings.edgeCoordinates_injective line 83
Source documentation
The coordinates in all layers determine all vertices of the path.
```
theorem edgeCoordinates_injective {α : Type*} {L : ℕ} :
    Function.Injective (edgeCoordinates (α := α) (L := L)) := by
…
```
Mentions: OAI.Problem335.Pairings.edgeCoordinates
theorem OAI.Problem335.Pairings.pathShift_injective line 94
Source documentation
Distinct paths produce distinct signed shifts, regardless of the V/U schedule.
```
theorem pathShift_injective {α : Type*} {L : ℕ}
    (sign : Fin (L + 1) → ℤ) (hsign : ∀ i, sign i ≠ 0) :
    Function.Injective (fun P : Fin (L + 2) → α =>
      layerShift sign (edgeCoordinates P)) :=
…
```
Mentions: OAI.Problem335.Pairings.layerShift, OAI.Problem335.Pairings.edgeCoordinates