Columns.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Finite switching paths in the manuscript's column models

A switch retains height and has zero cost. Between switches a path travels vertically; its length is the sum of all vertical variations. The band argument below does not identify an ambient distance with a band distance.

def OAI.PlanarL1.Columns.Consecutive line 15
Source documentation
Neighbors in the cyclic order, including the wrap-around edge.
```
def Consecutive {n : ℕ} (i j : Fin n) : Prop :=
…
```
structure OAI.PlanarL1.Columns.Model line 21
Source documentation
The data and standing hypotheses of a column model. Only the actual prescribed switch heights identify columns.
```
structure Model (n : ℕ) where
…
```
def OAI.PlanarL1.Columns.Model.activeGraph line 37
Source documentation
A link is active in a band exactly when it has an allowed height there.
```
def activeGraph (J : Set ℝ) : SimpleGraph (Fin n) where
…
```
lemma OAI.PlanarL1.Columns.Model.active_subgraph line 48
lemma OAI.PlanarL1.Columns.Model.active_noncrossing line 52

inductive OAI.PlanarL1.Columns.Model.Path line 59

Source documentation

A finite column word with an allowed band-switch height at every step. Endpoint heights are supplied separately; the nil word is a vertical segment.

inductive Path (J : Set ℝ) : Fin n → Fin n → Type
  | nil (i : Fin n) : Path J i i
  | cons {i j k : Fin n} (H : ℝ) (inBand : H ∈ J)
      (switch : H ∈ M.heights i j) (tail : Path J j k) : Path J i k

namespace Path

variable {M} {J : Set ℝ} {i j k : Fin n}

/-- Source length: sum of the lengths of vertical segments, with switches free. -/

def OAI.PlanarL1.Columns.Model.Path.length line 69

Source documentation

Source length: sum of the lengths of vertical segments, with switches free.

def length : {i j : Fin n} → M.Path J i j → ℝ → ℝ → ℝ
  | _, _, .nil _, a, b => |a - b|
  | _, _, .cons H _ _ p, a, b => |a - H| + p.length H b

/-- The associated walk in the active column graph, used for planar separation. -/

def OAI.PlanarL1.Columns.Model.Path.word line 74

Source documentation

The associated walk in the active column graph, used for planar separation.

def word : {i j : Fin n} → M.Path J i j → (M.activeGraph J).Walk i j
  | _, _, .nil _ => .nil
  | _, _, .cons H hH hs p => .cons ⟨H, hH, hs⟩ p.word

lemma OAI.PlanarL1.Columns.Model.Path.length_nonneg line 78
lemma OAI.PlanarL1.Columns.Model.Path.height_change_le line 83
lemma OAI.PlanarL1.Columns.Model.Path.length_end_le line 92
Source documentation
Moving just the final endpoint vertically changes a path length by at most that vertical distance. The intermediate switch heights stay unchanged.
```
lemma length_end_le (p : M.Path J i j) (a b c : ℝ) :
    p.length a c ≤ p.length a b + |b - c| := by
…
```
lemma OAI.PlanarL1.Columns.Model.Path.length_start_le line 100
def OAI.PlanarL1.Columns.Model.Path.append line 110
Source documentation
Concatenate switching words. Any redundant final/initial vertical detour at the common column is removed, so length can only decrease.
```
def append : {i j k : Fin n} → M.Path J i j → M.Path J j k → M.Path J i k
  | _, _, _, .nil _, q => q
  | _, _, _, .cons H hH hs p, q => .cons H hH hs (p.append q)
```
lemma OAI.PlanarL1.Columns.Model.Path.length_append_le line 114

def OAI.PlanarL1.Columns.Model.Path.snoc line 123

Source documentation

Adjoin one final switch at height H.

def snoc (p : M.Path J i j) (H : ℝ) (hH : H ∈ J) (hs : H ∈ M.heights j k) :
    M.Path J i k := p.append (.cons H hH hs (.nil k))

lemma OAI.PlanarL1.Columns.Model.Path.length_snoc line 126

def OAI.PlanarL1.Columns.Model.Path.reverse line 137

Source documentation

Reverse the column word and all its zero-cost switches.

def reverse : {i j : Fin n} → M.Path J i j → M.Path J j i
  | _, _, .nil _ => .nil _
  | _, _, .cons H hH hs p => p.reverse.snoc H hH (by rwa [M.symm] at hs)

lemma OAI.PlanarL1.Columns.Model.Path.length_reverse line 141
lemma OAI.PlanarL1.Columns.Model.Path.exists_word line 153
Source documentation
Every walk in the active graph really is a switching path: one chooses an available height independently for each prescribed switch.
```
lemma exists_word (p : (M.activeGraph J).Walk i j) :
    ∃ q : M.Path J i j, q.word = p := by
…
```

lemma OAI.PlanarL1.Columns.Model.Path.split_at_column line 164

Source documentation

A visit in a column word admits a genuine length-exact split at a height in the band. This keeps paths that leave an individual radial cell available.

lemma split_at_column (p : M.Path J i j) {a b : ℝ} (ha : a ∈ J) (_hb : b ∈ J)
    {v : Fin n} (hv : v ∈ p.word.support) :
    ∃ H ∈ J, ∃ (q : M.Path J i v) (r : M.Path J v j),
      q.length a H + r.length H b = p.length a b := by
…

lemma OAI.PlanarL1.Columns.Model.Path.vertical_split line 186
Source documentation
Split a vertical segment at a prescribed traveled length, remaining in its closed interval. This is valid for every interval band in the paper.
```
lemma vertical_split (hJ : Set.OrdConnected J) {a b ℓ : ℝ}
    (ha : a ∈ J) (hb : b ∈ J) (hℓ : 0 ≤ ℓ) (hbound : ℓ ≤ |a - b|) :
    ∃ T ∈ J, |a - T| = ℓ ∧ |T - b| = |a - b| - ℓ := by
…
```

lemma OAI.PlanarL1.Columns.Model.Path.split_at_length line 202

Source documentation

Every intermediate arclength is attained on a switching path in an interval band, by actual finite prefix and suffix paths. No abstract length space or geodesicity hypothesis is added.

lemma split_at_length (hJ : Set.OrdConnected J) (p : M.Path J i j)
    {a b ℓ : ℝ} (ha : a ∈ J) (hb : b ∈ J) (hℓ : 0 ≤ ℓ)
    (hbound : ℓ ≤ p.length a b) :
    ∃ (k : Fin n) (T : ℝ), T ∈ J ∧
      ∃ (q : M.Path J i k) (r : M.Path J k j),
        q.length a T = ℓ ∧ r.length T b = p.length a b - ℓ := by
…

lemma OAI.PlanarL1.Columns.Model.Path.crosses_set line 232

Source documentation

A finite switching word from outside a column set to inside it has a crossing switch. The decomposition retains the exact metric length, including both endpoint vertical segments.

lemma crosses_set (p : M.Path J i j) (S : Set (Fin n)) (hi : i ∉ S) (hj : j ∈ S)
    (a b : ℝ) :
    ∃ (u v : Fin n) (H : ℝ) (_hH : H ∈ J) (_hs : H ∈ M.heights u v),
      u ∉ S ∧ v ∈ S ∧ ∃ (q : M.Path J i u) (r : M.Path J v j),
        q.length a H + r.length H b = p.length a b := by
…

lemma OAI.PlanarL1.Columns.Model.Path.suffix_at_column line 250
Source documentation
Deleting a prefix up to a visited column cannot increase vertical variation, even when the new initial height is the old initial height.
```
lemma suffix_at_column (p : M.Path J i j) (a b : ℝ) {v : Fin n}
    (hv : v ∈ p.word.support) :
    ∃ r : M.Path J v j, r.word.support.Sublist p.word.support ∧
      r.length a b ≤ p.length a b := by
…
```
lemma OAI.PlanarL1.Columns.Model.Path.simple_replacement line 271
Source documentation
Loop erasure with its essential metric estimate: replacing a detour by vertical travel never increases length. The resulting word has no repeated column, so the later minimization is over finitely many words.
```
lemma simple_replacement (p : M.Path J i j) (a b : ℝ) :
    ∃ q : M.Path J i j, q.word.IsPath ∧ q.length a b ≤ p.length a b := by
…
```
lemma OAI.PlanarL1.Columns.Model.Path.zero_length_identifies line 289
Source documentation
Zero length is possible only at one common height, through switches all available at exactly that height.
```
lemma zero_length_identifies (p : M.Path J i j) (a b : ℝ)
    (h : p.length a b = 0) :
    a = b ∧ (M.activeGraph {a}).Reachable i j := by
…
```
lemma OAI.PlanarL1.Columns.Model.Path.exists_zero_path line 309

def OAI.PlanarL1.Columns.Model.Schedule line 326

Source documentation

A schedule specifies one allowed height for each edge of a fixed word. This recursive finite product carries its usual compact topology when the band is closed.

def Schedule (J : Set ℝ) : {i j : Fin n} → (M.activeGraph J).Walk i j → Type
  | _, _, .nil => PUnit
  | _, _, @SimpleGraph.Walk.cons _ _ i k _ _ p =>
      ↥(M.heights i k ∩ J) × Schedule J p

namespace Schedule

variable {M} {J : Set ℝ} {i j : Fin n}

instance OAI.PlanarL1.Columns.Model.Schedule.topology line 335
lemma OAI.PlanarL1.Columns.Model.Schedule.compactSpace line 343

def OAI.PlanarL1.Columns.Model.Schedule.toPath line 354

Source documentation

Realize a schedule as the literal switching path of the fixed word.

def toPath : {i j : Fin n} → {w : (M.activeGraph J).Walk i j} →
    M.Schedule J w → M.Path J i j
  | i, _, .nil, _ => .nil i
  | _, _, .cons _ _, s => .cons s.1.val s.1.property.2 s.1.property.1 (toPath s.2)

lemma OAI.PlanarL1.Columns.Model.Schedule.word_toPath line 359
def OAI.PlanarL1.Columns.Model.Schedule.ofPath line 367
lemma OAI.PlanarL1.Columns.Model.Schedule.toPath_ofPath line 371

lemma OAI.PlanarL1.Columns.Model.Schedule.continuous_length line 379

Source documentation

Length is a continuous function of all endpoint and switch heights.

lemma continuous_length {T : Type*} [TopologicalSpace T]
    (w : (M.activeGraph J).Walk i j) (a b : T → ℝ) (s : T → M.Schedule J w)
    (ha : Continuous a) (hb : Continuous b) (hs : Continuous s) :
    Continuous (fun t => (toPath (s t)).length (a t) (b t)) := by
…

Mentions: OAI.PlanarL1.Columns.Model.Schedule.toPath

structure OAI.PlanarL1.Columns.Model.Point line 392
Source documentation
Points before quotienting, in one component of the intrinsic band.
```
structure Point (J : Set ℝ) (root : Fin n) where
…
```