SeedPacking.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

The metric counting step of the restricted packing bound

Padded surviving seeds lie near two short paths, giving a cardinality estimate without a doubling assumption.

lemma OAI.PlanarL1.Packing.same_bucket_close line 14

theorem OAI.PlanarL1.Packing.two_intervals_count line 29

Source documentation

Points on two parameter intervals, separated by at least ε on each interval, have cardinality at most 2 + 2*L/ε.

theorem two_intervals_count {S : Type*} [Fintype S] {L ε : ℝ}
    (hε : 0 < ε) (hL : 0 ≤ L) (side : S → Fin 2) (time : S → ℝ)
    (ht : ∀ i, 0 ≤ time i ∧ time i ≤ L)
    (hsep : ∀ i j, i ≠ j → side i = side j → ε ≤ |time i - time j|) :
    (Fintype.card S : ℝ) ≤ 2 + 2 * L / ε := by
…

theorem OAI.PlanarL1.Packing.near_two_paths_count line 54

Source documentation

The two-path packing calculation, valid in any metric space. No bound on all cells or all balls is asserted: the hypotheses refer only to the selected, padded seeds and their explicitly assigned nearby path points.

theorem near_two_paths_count {X S : Type*} [PseudoMetricSpace X] [Fintype S]
    {L b ρ : ℝ} (hb : 0 < b) (hL : 0 ≤ L) (hρ : ρ ≤ b / 4)
    (seed : S → X) (path : Fin 2 → ℝ → X) (side : S → Fin 2) (time : S → ℝ)
    (ht : ∀ i, 0 ≤ time i ∧ time i ≤ L)
    (hne : ∀ i j, i ≠ j → b ≤ dist (seed i) (seed j))
    (hnear : ∀ i, dist (seed i) (path (side i) (time i)) ≤ ρ)
    (hpath : ∀ a t u, dist (path a t) (path a u) ≤ |t - u|) :
    (Fintype.card S : ℝ) ≤ 2 + 4 * L / b := by
…

theorem OAI.PlanarL1.Packing.surviving_seed_number line 80

Source documentation

Substitution of the actual packing constants: each path has length 4R, padded seeds are 0.01g separated, and the source's near-path radius is at most one quarter of that separation.

theorem surviving_seed_number {X S : Type*} [PseudoMetricSpace X] [Fintype S]
    {R g ρ : ℝ} (hg : 0 < g) (hR : 0 ≤ R) (hρ : ρ ≤ (0.01 * g) / 4)
    (seed : S → X) (path : Fin 2 → ℝ → X) (side : S → Fin 2) (time : S → ℝ)
    (ht : ∀ i, 0 ≤ time i ∧ time i ≤ 4 * R)
    (hne : ∀ i j, i ≠ j → 0.01 * g ≤ dist (seed i) (seed j))
    (hnear : ∀ i, dist (seed i) (path (side i) (time i)) ≤ ρ)
    (hpath : ∀ a t u, dist (path a t) (path a u) ≤ |t - u|) :
    Fintype.card S ≤ 2 + ⌈1600 * R / g⌉₊ := by
…

def OAI.PlanarL1.Columns.Model.Path.AtTime line 111

Source documentation

A specified visit of a finite switching path, retaining its traveled arclength. Multiple visits of the same representative are not identified.

def AtTime : {i j : Fin n} → M.Path J i j → ℝ → ℝ → (Fin n × ℝ) → ℝ → Prop
  | i, _, .nil _, a, b, z, t => z.1 = i ∧ z.2 ∈ Set.uIcc a b ∧ t = |a-z.2|
  | i, _, .cons H _ _ p, a, b, z, t =>
      (z.1 = i ∧ z.2 ∈ Set.uIcc a H ∧ t = |a-z.2|) ∨ p.AtTime H b z (t-|a-H|)

lemma OAI.PlanarL1.Columns.Model.Path.trace_atTime line 116
lemma OAI.PlanarL1.Columns.Model.Path.atTime_split line 126
lemma OAI.PlanarL1.Columns.Model.Path.atTime_bounds line 143
lemma OAI.PlanarL1.Columns.Model.Path.vertical_offset line 148
lemma OAI.PlanarL1.Columns.Model.Path.between_atTime line 165
Source documentation
Subpaths between actual arclength visits have no greater length than the arclength difference. This is proved on the finite words, without assuming an unconstructed continuous parametrization.
```
lemma between_atTime {i j : Fin n} (p : M.Path J i j) {a b t u : ℝ} {z w : Fin n × ℝ}
    (hz : p.AtTime a b z t) (hw : p.AtTime a b w u) :
    ∃ q : M.Path J z.1 w.1, q.length z.2 w.2 ≤ |t-u| := by
…
```
lemma OAI.PlanarL1.Columns.Model.Path.dist_atTime line 223

theorem OAI.PlanarL1.Columns.Model.near_two_traces_count line 238

Source documentation

The source's two-path packing bound for the actual finite switching paths, including all their vertical representatives and repeated visits.

theorem near_two_traces_count {S : Type*} [Fintype S] {L b ρ : ℝ}
    (hJI : J ⊆ I) (hb : 0 < b) (hL : 0 ≤ L) (hρ : ρ ≤ b/4)
    (start finish : Fin 2 → Fin n) (p : ∀ a, M.Path J (start a) (finish a))
    (A B : Fin 2 → ℝ) (hp : ∀ a, (p a).length (A a) (B a) ≤ L)
    (seed near : S → M.Point I root) (side : S → Fin 2)
    (htrace : ∀ i, ((near i).column,(near i).height) ∈
      (p (side i)).trace (A (side i)) (B (side i)))
    (hne : ∀ i j, i ≠ j → b ≤ dist (seed i) (seed j))
    (hnear : ∀ i, dist (seed i) (near i) ≤ ρ) :
    (Fintype.card S : ℝ) ≤ 2+4*L/b := by
…

theorem OAI.PlanarL1.Columns.Model.surviving_seed_traces_number line 268

Source documentation

Direct substitution of the manuscript constants, with no abstract Lipschitz path or externally supplied parametrization.

theorem surviving_seed_traces_number {S : Type*} [Fintype S] {R g ρ : ℝ}
    (hJI : J ⊆ I) (hg : 0 < g) (hR : 0 ≤ R) (hρ : ρ ≤ (0.01*g)/4)
    (start finish : Fin 2 → Fin n) (p : ∀ a, M.Path J (start a) (finish a))
    (A B : Fin 2 → ℝ) (hp : ∀ a, (p a).length (A a) (B a) ≤ 4*R)
    (seed near : S → M.Point I root) (side : S → Fin 2)
    (htrace : ∀ i, ((near i).column,(near i).height) ∈
      (p (side i)).trace (A (side i)) (B (side i)))
    (hne : ∀ i j, i ≠ j → 0.01*g ≤ dist (seed i) (seed j))
    (hnear : ∀ i, dist (seed i) (near i) ≤ ρ) :
    Fintype.card S ≤ 2+⌈1600*R/g⌉₊ := by
…

lemma OAI.PlanarL1.ColumnOrder.gap_of_chord line 292

Source documentation

A connected low set lying on the far side of a chord has no vertex in its open interval, provided neither endpoint belongs to that set.

lemma gap_of_chord {n : ℕ} {G : SimpleGraph (Fin n)} (hnc : Noncrossing G)
    {S : Set (Fin n)} (hS : (G.induce S).Preconnected) {a b c : Fin n}
    (hab : G.Adj a b) (ha : a ∉ S) (hb : b ∉ S) (hc : c ∈ S)
    (hcside : c < a ∨ b < c) : ∀ v ∈ S, v < a ∨ b < v := by
…

Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

lemma OAI.PlanarL1.Columns.not_consecutive_of_between line 315
lemma OAI.PlanarL1.Columns.Model.Path.trace_start line 325
lemma OAI.PlanarL1.Columns.Model.Path.trace_end line 331
lemma OAI.PlanarL1.Columns.Model.Path.trace_on_column line 337

lemma OAI.PlanarL1.Columns.Model.Path.dart_on_trace line 353

Source documentation

Every dart of the word is an actual switch at a height visited on both of its representatives by the original path.

lemma dart_on_trace {i j : Fin n} (p : M.Path J i j) (a b : ℝ)
    (e : (M.activeGraph J).Dart) (he : e ∈ p.word.darts) :
    ∃ H ∈ J, H ∈ M.heights e.fst e.snd ∧
      (e.fst,H) ∈ p.trace a b ∧ (e.snd,H) ∈ p.trace a b := by
…

lemma OAI.PlanarL1.Columns.Model.Point.dist_to_tip line 378

Source documentation

Vertical transfer to either representative of a switch costs at most the width of the band, even if the two representatives are not equal as structures.

lemma dist_to_tip (e v : M.Point J root) {b : Fin n} {a : ℝ}
    (hs : e.height ∈ M.heights e.column b)
    (hw : ∀ s ∈ J, ∀ t ∈ J, |s-t| ≤ a) (hv : v.column = e.column ∨ v.column = b) :
    dist v e ≤ a := by
…

structure OAI.PlanarL1.Columns.Model.Field.Descent line 396
Source documentation
Descending paths are actual attained shortest switching paths, with the manuscript's length domain and endpoint deficit, not assumed rays in a quotient.
```
structure Descent (F : M.Field J 1) (x : M.Point J root) (ε : ℝ) where
…
```
lemma OAI.PlanarL1.Columns.Model.Field.Descent.column_prefix line 410
Source documentation
A visited column supplies an actual prefix point with both the total length control and the almost-unit descending scalar estimate.
```
lemma column_prefix (D : F.Descent x ε) {v : Fin n} (hv : v ∈ D.path.word.support) :
    ∃ z : M.Point J root, z.column = v ∧ dist x z ≤ (1:ℝ)/50 ∧
      F.eval z ≤ F.eval x-dist x z+ε := by
…
```

lemma OAI.PlanarL1.Columns.Model.Field.Descent.near_tip line 427

Source documentation

Basic reach-to-tip bound used to show that a witness partner cannot lie on the skipped side of a chord.

lemma near_tip (D : F.Descent x ε) (e : M.Point J root) {b : Fin n} {a : ℝ}
    (hs : e.height ∈ M.heights e.column b)
    (hw : ∀ s ∈ J, ∀ t ∈ J, |s-t| ≤ a)
    (hx : e.column < x.column ∧ x.column < b)
    (hz : D.target.column < e.column ∨ b < D.target.column) :
    dist x e ≤ (1:ℝ)/50+a := by
…

lemma OAI.PlanarL1.Columns.Model.Field.Descent.near_tip_of_not_low line 444

Source documentation

The quantitative skipped-seed estimate pack:near-path: the absence of a low separating tip truncates the actual descending prefix at j+ε+a.

lemma near_tip_of_not_low (D : F.Descent x ε) (hJ : IsClosed J)
    (e : M.Point J root) {b : Fin n} {a j : ℝ}
    (hs : e.height ∈ M.heights e.column b)
    (hw : ∀ s ∈ J, ∀ t ∈ J, |s-t| ≤ a)
    (hx : e.column < x.column ∧ x.column < b)
    (hz : D.target.column < e.column ∨ b < D.target.column)
    (hlow : F.eval x-j ≤ F.eval e) : dist x e ≤ j+ε+2*a := by
…

lemma OAI.PlanarL1.Columns.Model.Field.partner_outside_tip line 468

Source documentation

The partner of a seed skipped by an extreme short path must be strictly outside the chord. Boundary representatives are also excluded quantitatively.

lemma partner_outside_tip {F : M.Field J 1} {ε a A : ℝ}
    (x y e : M.Point J root) (D : F.Descent y ε) {b : Fin n}
    (hs : e.height ∈ M.heights e.column b)
    (hw : ∀ s ∈ J, ∀ t ∈ J, |s-t| ≤ a)
    (hz : D.target.column < e.column ∨ b < D.target.column)
    (hxy : 1 ≤ dist x y) (hxe : dist x e ≤ A) (hsmall : (1:ℝ)/50+a+A < 1) :
    y.column < e.column ∨ b < y.column := by
…

lemma OAI.PlanarL1.ColumnOrder.visits_or_skips_left line 501
lemma OAI.PlanarL1.ColumnOrder.extreme_words line 524
Source documentation
The two extremal words cover every intermediate column by a visit or a strictly skipping dart. No connectedness of the seed set is asserted.
```
lemma extreme_words {n : ℕ} {G : SimpleGraph (Fin n)} {l r c w : Fin n}
    (p : G.Walk c l) (q : G.Walk c r) (hl : l ≤ w) (hr : w ≤ r) :
    (w ∈ p.support ∨ JumpsAcross w p) ∨ (w ∈ q.support ∨ JumpsAcross w q) := by
…
```
Mentions: OAI.PlanarL1.ColumnOrder.JumpsAcross
lemma OAI.PlanarL1.Columns.Model.Point.dist_le_trace_length line 548

lemma OAI.PlanarL1.Columns.Model.Point.point_on_trace line 560

Source documentation

Every actual trace representative is an intrinsic point of the same larger-band component as the start, not an assumed representative choice.

lemma point_on_trace (hJI : J ⊆ I) (c : M.Point I root) {v k : Fin n}
    (p : M.Path J c.column v) {H T : ℝ} (hT : T ∈ J)
    (ht : (k,T) ∈ p.trace c.height H) :
    ∃ e : M.Point I root, e.column = k ∧ e.height = T ∧ dist c e ≤ p.length c.height H := by
…

def OAI.PlanarL1.Columns.Model.Field.TipSeparates line 574
Source documentation
Strict separation of representatives by the chord, with an arbitrary linear cut outside its first open arc.
```
def TipSeparates (a b x y : Fin n) : Prop :=
…
```
def OAI.PlanarL1.Columns.Model.Field.NoLowTip line 579
Source documentation
Complement of the main procedure's barrier-drop exclusion. Both endpoint thresholds are tested, exactly as in pack:barrier and pack:retained-data.
```
def NoLowTip (F : M.Field I 1) (x y : M.Point I root) (J : Set ℝ) (j : ℝ) : Prop :=
…
```

lemma OAI.PlanarL1.Columns.Model.Field.skipped_seed_near_trace line 589

Source documentation

A single skipping dart of an extreme path puts its seed near the actual trace. Connected low columns, witness descent and the barrier exclusion are used here, not replaced by the desired near-path conclusion.

lemma skipped_seed_near_trace (F : M.Field I 1) (hI : IsClosed I)
    {S : Set (Fin n)} (hS : (M.link.induce S).Preconnected)
    {cut : Fin n} (hcut : cut ∈ S) (hmin : ∀ v, cut ≤ v)
    (hJI : J ⊆ I) {a A j ε : ℝ} (hw : ∀ s ∈ I, ∀ t ∈ I, |s-t| ≤ a)
    (c x y : M.Point I root) (Dx : F.Descent x ε) (Dy : F.Descent y ε)
    (hxS : Dx.target.column ∈ S) (hyS : Dy.target.column ∈ S)
    (hxy : 1 ≤ dist x y) (hcx : dist c x ≤ A) (hA : 2*A ≤ 1)
    (hsmall : (1:ℝ)/50+a+2*A < 1) (hretain : F.NoLowTip x y J j)
    {v : Fin n} (p : M.Path J c.column v) {H : ℝ} (hp : p.length c.height H ≤ A)
    (havoid : ∀ k ∈ p.word.support, k ∉ S) (hskip : ColumnOrder.JumpsAcross x.column p.word) :
    ∃ e : M.Point I root, (e.column,e.height) ∈ p.trace c.height H ∧
      dist x e ≤ j+ε+2*a := by
…

Mentions: OAI.PlanarL1.ColumnOrder.JumpsAcross

lemma OAI.PlanarL1.Columns.Model.Field.visited_seed_near_trace line 643

Source documentation

A visited seed column is vertically near a point of the original trace; leaving the individual radial cell is allowed throughout.

lemma visited_seed_near_trace (hJI : J ⊆ I) {a : ℝ}
    (hw : ∀ s ∈ I, ∀ t ∈ I, |s-t| ≤ a) (c x : M.Point I root)
    (hc : c.height ∈ J) {v : Fin n} (p : M.Path J c.column v) {H : ℝ}
    (hx : x.column ∈ p.word.support) :
    ∃ e : M.Point I root, (e.column,e.height) ∈ p.trace c.height H ∧ dist x e ≤ a := by
…

theorem OAI.PlanarL1.Columns.Model.Field.restricted_packing line 658

Source documentation

The restricted packing geometry, before the final substitution of fixed constants. The two extremal paths are selected from the actual center paths. The low set may be absent from most columns; no doubling or ambient ball packing hypothesis occurs.

theorem restricted_packing {K : Type*} [Fintype K]
    (F : M.Field I 1) (hI : IsClosed I)
    {S : Set (Fin n)} (hS : (M.link.induce S).Preconnected)
    {cut : Fin n} (hcut : cut ∈ S) (hmin : ∀ v, cut ≤ v)
    (hJI : J ⊆ I) {a A j ε b : ℝ} (hw : ∀ s ∈ I, ∀ t ∈ I, |s-t| ≤ a)
    (hA₀ : 0 ≤ A) (hA : 2*A ≤ 1) (hsmall : (1:ℝ)/50+a+2*A < 1)
    (hb : 0 < b) (hpad : j+ε+2*a ≤ b/4) (hvisit : a ≤ j+ε+2*a)
    (c : M.Point I root) (hc : c.height ∈ J) (hcS : c.column ∉ S)
    (seed partner : K → M.Point I root)
    (Dx : ∀ w, F.Descent (seed w) ε) (Dy : ∀ w, F.Descent (partner w) ε)
    (hxS : ∀ w, (Dx w).target.column ∈ S) (hyS : ∀ w, (Dy w).target.column ∈ S)
    (hxy : ∀ w, 1 ≤ dist (seed w) (partner w))
…

theorem OAI.PlanarL1.Columns.Model.Field.restricted_packing_number line 734

Source documentation

The source packing number after the restricted geometric argument, with A=4R and padded distinct cells separated by 0.01g.

theorem restricted_packing_number {K : Type*} [Fintype K]
    (F : M.Field I 1) (hI : IsClosed I)
    {S : Set (Fin n)} (hS : (M.link.induce S).Preconnected)
    {cut : Fin n} (hcut : cut ∈ S) (hmin : ∀ v, cut ≤ v)
    (hJI : J ⊆ I) {a R j ε g : ℝ} (hw : ∀ s ∈ I, ∀ t ∈ I, |s-t| ≤ a)
    (hR₀ : 0 ≤ R) (hR : 8*R ≤ 1) (hsmall : (1:ℝ)/50+a+8*R < 1)
    (hg : 0 < g) (hpad : j+ε+2*a ≤ (0.01*g)/4) (hvisit : a ≤ j+ε+2*a)
    (c : M.Point I root) (hc : c.height ∈ J) (hcS : c.column ∉ S)
    (seed partner : K → M.Point I root)
    (Dx : ∀ w, F.Descent (seed w) ε) (Dy : ∀ w, F.Descent (partner w) ε)
    (hxS : ∀ w, (Dx w).target.column ∈ S) (hyS : ∀ w, (Dy w).target.column ∈ S)
    (hxy : ∀ w, 1 ≤ dist (seed w) (partner w))
…