SwitchRestoration.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.SwitchRestoration.switchCount line 14
Source documentation
Switches in a Boolean labeling along a finite collection of oriented edges.
```
def switchCount (edges : Finset (ι × ι)) (w : ι → Bool) : ℕ :=
…
```
def OAI.Problem335.SwitchRestoration.endpointDegree line 18
Source documentation
The number of edge endpoints at a vertex, counting both ends of a loop.
```
def endpointDegree (edges : Finset (ι × ι)) (i : ι) : ℕ :=
…
```
theorem OAI.Problem335.SwitchRestoration.edge_switch_restore line 21

theorem OAI.Problem335.SwitchRestoration.switchCount_restore_eq line 36

Source documentation

Restoring an independent subset of all-true neighborhoods creates one switch per incident edge.

theorem switchCount_restore_eq (edges : Finset (ι × ι)) (S : Finset ι) (y : ι → Bool)
    (hnear : ∀ e ∈ edges, e.1 ∈ S ∨ e.2 ∈ S → y e.1 = true ∧ y e.2 = true)
    (hind : ∀ e ∈ edges, ¬ (e.1 ∈ S ∧ e.2 ∈ S)) :
    switchCount edges (fun i => if i ∈ S then false else y i) =
      switchCount edges y + ∑ i ∈ S, endpointDegree edges i := by
…

Mentions: OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.SwitchRestoration.endpointDegree

theorem OAI.Problem335.SwitchRestoration.switchCount_restore_eq_add_twice_card line 55

Source documentation

Every restored interior vertex of a path creates exactly two switches.

theorem switchCount_restore_eq_add_twice_card
    (edges : Finset (ι × ι)) (S : Finset ι) (y : ι → Bool)
    (hnear : ∀ e ∈ edges, e.1 ∈ S ∨ e.2 ∈ S → y e.1 = true ∧ y e.2 = true)
    (hind : ∀ e ∈ edges, ¬ (e.1 ∈ S ∧ e.2 ∈ S))
    (hdegree : ∀ i ∈ S, endpointDegree edges i = 2) :
    switchCount edges (fun i => if i ∈ S then false else y i) =
      switchCount edges y + 2 * S.card := by
…

Mentions: OAI.Problem335.SwitchRestoration.endpointDegree, OAI.Problem335.SwitchRestoration.switchCount

def OAI.Problem335.SwitchRestoration.pathEdges line 71
Source documentation
Edges of the path with n+1 vertices.
```
def pathEdges (n : ℕ) : Finset (Fin (n + 1) × Fin (n + 1)) :=
…
```
theorem OAI.Problem335.SwitchRestoration.path_edge_injective line 74
theorem OAI.Problem335.SwitchRestoration.switchCount_pathEdges line 81
Source documentation
This switch count agrees with the usual adjacent-position sum.
```
theorem switchCount_pathEdges (n : ℕ) (w : Fin (n + 1) → Bool) :
    switchCount (pathEdges n) w =
      ∑ i : Fin n, if w i.castSucc ≠ w i.succ then 1 else 0 := by
…
```
Mentions: OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.SwitchRestoration.pathEdges
theorem OAI.Problem335.SwitchRestoration.endpointDegree_pathEdges_interior line 88

theorem OAI.Problem335.SwitchRestoration.path_switchCount_restore_eq line 130

Source documentation

The path specialization states all hypotheses directly on neighboring indices.

theorem path_switchCount_restore_eq {n : ℕ} (S : Finset (Fin (n + 1)))
    (y : Fin (n + 1) → Bool)
    (hinterior : ∀ i ∈ S, 0 < i.val ∧ i.val < n)
    (hnear : ∀ j : Fin n, j.castSucc ∈ S ∨ j.succ ∈ S →
      y j.castSucc = true ∧ y j.succ = true)
    (hind : ∀ j : Fin n, ¬ (j.castSucc ∈ S ∧ j.succ ∈ S)) :
    switchCount (pathEdges n) (fun i => if i ∈ S then false else y i) =
      switchCount (pathEdges n) y + 2 * S.card := by
…

Mentions: OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.SwitchRestoration.pathEdges

theorem OAI.Problem335.SwitchRestoration.trueVertices_restore_eq_sdiff line 149

Source documentation

Restoring false symbols removes exactly the chosen true symbols.

theorem trueVertices_restore_eq_sdiff (V S : Finset ι) (y : ι → Bool) :
    (V.filter fun i => (if i ∈ S then false else y i) = true) =
      (V.filter fun i => y i = true) \ S := by
…

theorem OAI.Problem335.SwitchRestoration.trueVertices_restore_card_add line 156

Source documentation

Cardinal form without truncated subtraction, suitable for exponent arithmetic.

theorem trueVertices_restore_card_add (V S : Finset ι) (y : ι → Bool)
    (hS : S ⊆ V) (hy : ∀ i ∈ S, y i = true) :
    (V.filter fun i => (if i ∈ S then false else y i) = true).card + S.card =
      (V.filter fun i => y i = true).card := by
…