RelaxedPaths.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.Pairings.constantLabels line 8
Source documentation
The fixed labels at either external vertex.
```
def constantLabels {α : Type*} (a : α) : Labels α := ⟨a, a, a, a⟩
…
```
Mentions: OAI.Problem335.Pairings.Labels
theorem OAI.Problem335.Pairings.respects_constantLabels line 11
def OAI.Problem335.Pairings.zipLabels line 16
Source documentation
Coordinates of the four paths in one layer are pairs of adjacent vertex labels.
```
def zipLabels {α β : Type*} (x : Labels α) (y : Labels β) : Labels (α × β) :=
…
```
Mentions: OAI.Problem335.Pairings.Labels
theorem OAI.Problem335.Pairings.respects_zipLabels line 20
def OAI.Problem335.Pairings.closePaths line 25
Source documentation
Add the two fixed external vertices to four paths specified by their internal labels.
```
def closePaths {α : Type*} {L : ℕ} (a : α) (x : Fin L → Labels α) :
    Fin (L + 2) → Labels α :=
…
```
Mentions: OAI.Problem335.Pairings.Labels
theorem OAI.Problem335.Pairings.closePaths_zero line 30
theorem OAI.Problem335.Pairings.closePaths_last line 34
theorem OAI.Problem335.Pairings.closePaths_internal line 39

theorem OAI.Problem335.Pairings.closePaths_compatible_iff line 45

Source documentation

Layer constraints are exactly the independent constraints at internal vertices.

theorem closePaths_compatible_iff {α : Type*} {L : ℕ}
    (a : α) (τ : Fin (L + 1) → Kind) (x : Fin L → Labels α) :
    (∀ t : Fin (L + 1), Respects (τ t)
      (zipLabels (closePaths a x t.castSucc) (closePaths a x t.succ))) ↔
    ∀ i : Fin L, Respects (τ i.castSucc) (x i) ∧ Respects (τ i.succ) (x i) := by
…

Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.Respects, OAI.Problem335.Pairings.zipLabels, OAI.Problem335.Pairings.closePaths

abbrev OAI.Problem335.Pairings.RelaxedPaths line 66
Source documentation
Four endpoint-fixed paths respecting a prescribed relaxed pairing in every layer.
```
abbrev RelaxedPaths (α : Type*) {L : ℕ} (a : α) (τ : Fin (L + 1) → Kind) :=
…
```
Mentions: OAI.Problem335.Pairings.Kind
def OAI.Problem335.Pairings.relaxedPathsEquivAssignments line 71
Source documentation
The explicit product decomposition used in the second trace count.
```
def relaxedPathsEquivAssignments (α : Type*) {L : ℕ}
    (a : α) (τ : Fin (L + 1) → Kind) :
    RelaxedPaths α a τ ≃ Assignments α τ where
…
```
Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.RelaxedPaths, OAI.Problem335.Pairings.Assignments
theorem OAI.Problem335.Pairings.card_relaxedPaths line 81
Source documentation
Exact count of relaxed quadruples with fixed endpoints.
```
theorem card_relaxedPaths (α : Type*) [Fintype α] [DecidableEq α]
    {L : ℕ} (a : α) (τ : Fin (L + 1) → Kind) :
    Fintype.card (RelaxedPaths α a τ) =
      Fintype.card α ^ (2 * L - adjacentSwitches τ) :=
…
```
Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.RelaxedPaths, OAI.Problem335.Pairings.adjacentSwitches
theorem OAI.Problem335.Pairings.card_relaxedPaths_bool line 88
Source documentation
Boolean-word form of the count, with false = normal and true = diagonal.
```
theorem card_relaxedPaths_bool (α : Type*) [Fintype α] [DecidableEq α]
    {L : ℕ} (a : α) (τ : Fin (L + 1) → Bool) :
    Fintype.card (RelaxedPaths α a (fun i => boolKindEquiv (τ i))) =
      Fintype.card α ^ (2 * L - adjacentSwitches τ) := by
…
```
Mentions: OAI.Problem335.Pairings.RelaxedPaths, OAI.Problem335.Pairings.boolKindEquiv, OAI.Problem335.Pairings.adjacentSwitches