OAI/Combinatorics/PlanarL1/Bands.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.Columns.consecutive_rotate line 9
2. lemma OAI.PlanarL1.Columns.consecutive_iterate line 41
3. lemma OAI.PlanarL1.Columns.consecutive_cycle line 49
4. def OAI.PlanarL1.Columns.Model.relabel line 59

   Source documentation

   Relabelling columns does not change geometry. The two order conditions are explicit, so the construction never assumes invariance under an arbitrary permutation of the circular order.

   def relabel {n : ℕ} (M : Model n) (e : Equiv.Perm (Fin n))
       (hnc : ColumnOrder.Noncrossing (M.link.comap e))
       (hcon : ∀ i j, Consecutive (e i) (e j) ↔ Consecutive i j) : Model n where
   …

   Mentions: OAI.PlanarL1.Columns.Model, OAI.PlanarL1.ColumnOrder.Noncrossing, OAI.PlanarL1.Columns.Consecutive

5. def OAI.PlanarL1.Columns.Model.Path.unlabel line 78

   Source documentation

   Undo a column relabelling on actual finite switching paths.

   def Path.unlabel : {i j : Fin n} → (M.relabel e hnc hcon).Path J i j →
       M.Path J (e i) (e j)
     | _, _, .nil _ => .nil _
     | _, _, .cons H hH hs p => .cons H hH hs p.unlabel

   Mentions: OAI.PlanarL1.Columns.Model.Path

6. lemma OAI.PlanarL1.Columns.Model.Path.length_unlabel line 83
7. def OAI.PlanarL1.Columns.Model.Path.label line 89
8. lemma OAI.PlanarL1.Columns.Model.Path.length_label line 95
9. def OAI.PlanarL1.Columns.Model.Point.unlabel line 102

   Source documentation

   The point map keeps the height and moves only the column name.

   def Point.unlabel (x : (M.relabel e hnc hcon).Point J root) : M.Point J (e root) where
   …

   Mentions: OAI.PlanarL1.Columns.Model.Point

10. def OAI.PlanarL1.Columns.Model.Path.cast line 111
11. lemma OAI.PlanarL1.Columns.Model.Path.length_cast line 114
12. lemma OAI.PlanarL1.Columns.Model.Point.dist_unlabel line 118
13. def OAI.PlanarL1.Columns.Model.Point.widen line 146

    Source documentation

    Inclusion of intrinsic components into a larger band. No equality of the intrinsic metrics is asserted.

    def Point.widen (x : M.Point J root) (hJI : J ⊆ I) : M.Point I root where
    …

14. lemma OAI.PlanarL1.Columns.Model.Point.dist_widen_le line 155
15. lemma OAI.PlanarL1.Columns.Model.Path.tip_connection line 167

    Source documentation

    The vertical connection to a tip uses only the thin band, not the much wider old chart band where scalar distance fields are defined.

    lemma tip_connection {i l b : Fin n} {s H a : ℝ}
        (hsJ : s ∈ J) (hHJ : H ∈ J) (hs : H ∈ M.heights l b)
        (hw : ∀ s ∈ J, ∀ t ∈ J, |s-t| ≤ a) (hi : i = l ∨ i = b) :
        ∃ p : M.Path J i l, p.length s H ≤ a := by
    …

16. structure OAI.PlanarL1.Columns.Model.Field.BandDescent line 183

    Source documentation

    The source descent lives in the BROAD CURRENT band J, whereas the old comparison field and witnesses live in the OLD chart I, possibly in different J-components. The attaining condition refers to J, not to the larger band.

    structure BandDescent (F : M.Field I 1) (J : Set ℝ) (x : M.Point I root) (ε : ℝ) where
    …

17. lemma OAI.PlanarL1.Columns.Model.Field.BandDescent.column_prefix line 198
18. lemma OAI.PlanarL1.Columns.Model.Field.BandDescent.path_to_tip line 218

    Source documentation

    Actual bounded-length path to a separating tip, even when the witness's broad-band component was not known to be the seed's component beforehand.

    lemma path_to_tip (D : F.BandDescent J x ε) (hJI : J ⊆ I)
        (e : M.Point I root) {b : Fin n} {a : ℝ}
        (heJ : e.height ∈ 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) :
        ∃ p : M.Path J x.column e.column, p.length x.height e.height ≤ (1:ℝ)/50+a := by
    …

19. lemma OAI.PlanarL1.Columns.Model.Field.BandDescent.short_path_to_tip line 236

    Source documentation

    The fine near-tip bound is witnessed by a path in the CURRENT broad band. Only scalar evaluation, not path geometry, uses the old chart.

    lemma short_path_to_tip (D : F.BandDescent J x ε) (hJI : J ⊆ I)
        (e : M.Point I root) {b : Fin n} {a j : ℝ}
        (heJ : e.height ∈ 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) :
        ∃ p : M.Path J x.column e.column, p.length x.height e.height ≤ j+ε+2*a := by
    …

20. def OAI.PlanarL1.Columns.Model.Point.radialValue line 271

    Source documentation

    Actual distance field of an old chart. Outside its component we choose zero only to make a whole-band scalar function; radial sublevels retain the source's +infinity convention and never include those columns.

    noncomputable def radialValue (o : M.Point I root) (i : Fin n) (H : I) : ℝ := by
    …

21. lemma OAI.PlanarL1.Columns.Model.Point.radialValue_vertical line 276
22. lemma OAI.PlanarL1.Columns.Model.Point.radialValue_switch line 291
23. def OAI.PlanarL1.Columns.Model.Point.radialField line 308
24. lemma OAI.PlanarL1.Columns.Model.Point.radialField_eval line 313
25. lemma OAI.PlanarL1.Columns.Model.Point.sublevel_link_preconnected line 316
26. lemma OAI.PlanarL1.Columns.Model.Point.descent_target_low line 328

    Source documentation

    The actual target of each almost-descending broad-band path is a member of the old-distance low sublevel. Width is used only for the broad band J.

    lemma descent_target_low (o w x : M.Point I root) (hJI : J ⊆ I)
        {ε a B δ : ℝ} (D : o.radialField.BandDescent J x ε) {H : ℝ} (hHJ : H ∈ J)
        (hw : ∀ s ∈ J, ∀ t ∈ J, |s-t| ≤ a)
        (hclose : dist o x ≤ dist o w+B)
        (hsmall : B+ε+a < (1:ℝ)/100000-δ) :
        D.target.column ∈ o.sublevel H (hJI hHJ) (dist o w-δ) := by
    …

27. lemma OAI.PlanarL1.Columns.Model.Point.short_path_avoids_low line 348

    Source documentation

    The same old-distance sublevel misses EVERY visited column of a short center path. This establishes the manuscript's avoidance condition rather than postulating it of a chosen set.

    lemma short_path_avoids_low (o w c : M.Point I root) (hJI : J ⊆ I)
        {a A δ : ℝ} {H : ℝ} (hHJ : H ∈ J)
        (hw : ∀ s ∈ J, ∀ t ∈ J, |s-t| ≤ a)
        (hcJ : c.height ∈ J) (hcw : dist c w ≤ A) (hsmall : 2*A+a < δ)
        {v : Fin n} (p : M.Path J c.column v) {T : ℝ}
        (hp : p.length c.height T ≤ A) :
        ∀ k ∈ p.word.support, k ∉ o.sublevel H (hJI hHJ) (dist o w-δ) := by
    …

28. lemma OAI.PlanarL1.Columns.Model.Field.BandDescent.partner_outside_tip line 379
29. lemma OAI.PlanarL1.Columns.Model.Field.skipped_seed_broad_path line 409

    Source documentation

    The skipped-seed estimate keeps the old chart, broad current band and narrow center-path band distinct. Its conclusion contains an ACTUAL broad-band path to the trace, not just a distance in the larger old chart.

    lemma skipped_seed_broad_path (F : M.Field I 1)
        {S : Set (Fin n)} (hS : (M.link.induce S).Preconnected)
        {cut : Fin n} (hcut : cut ∈ S) (hmin : ∀ v, cut ≤ v)
        (hJK : J ⊆ K) (hKI : K ⊆ I) {a A j ε : ℝ}
        (hw : ∀ s ∈ K, ∀ t ∈ K, |s-t| ≤ a)
        (c x y : M.Point I root) (Dx : F.BandDescent K x ε) (Dy : F.BandDescent K 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.height ∈ J ∧ (e.column,e.height) ∈ p.trace c.height H ∧
    …

    Mentions: OAI.PlanarL1.ColumnOrder.JumpsAcross

30. theorem OAI.PlanarL1.Columns.Model.Field.restricted_broad_packing line 456
31. def OAI.PlanarL1.Columns.Model.Point.label line 545
32. lemma OAI.PlanarL1.Columns.Model.Point.unlabel_label line 555
33. lemma OAI.PlanarL1.Columns.Model.Point.label_unlabel line 560
34. lemma OAI.PlanarL1.Columns.Model.Point.dist_label line 565
35. def OAI.PlanarL1.Columns.Model.Point.labelEquiv line 569
36. def OAI.PlanarL1.Columns.Model.Field.label line 575
37. lemma OAI.PlanarL1.Columns.Model.Field.eval_label line 580
38. lemma OAI.PlanarL1.Columns.Model.Field.eval_unlabel line 584
39. def OAI.PlanarL1.Columns.Model.Field.BandDescent.label line 588
40. def OAI.PlanarL1.Columns.Model.Field.CircularTipSeparates line 615

    Source documentation

    Strictly opposite sides of an unoriented circular chord.

    def CircularTipSeparates {n : ℕ} (a b x y : Fin n) : Prop :=
    …

41. lemma OAI.PlanarL1.Columns.Model.Field.circularTip_rotate line 618
42. lemma OAI.PlanarL1.Columns.Model.Field.circularTip_iterate line 632
43. lemma OAI.PlanarL1.Columns.Model.Field.circularTip_cycle line 641
44. lemma OAI.PlanarL1.Columns.Model.Point.widen_label line 656
45. lemma OAI.PlanarL1.Columns.Model.Path.support_word_label line 659
46. def OAI.PlanarL1.Columns.Model.Field.NoLowCircular line 671

    Source documentation

    Absence of a low separating tip is intrinsically circular: reversing the listed chord endpoints does not change the exclusion test.

    def NoLowCircular (F : M.Field I 1) (x y : M.Point I root) (J : Set ℝ) (j : ℝ) : Prop :=
    …

47. lemma OAI.PlanarL1.Columns.Model.Field.NoLowCircular.toNoLowTip line 678
48. lemma OAI.PlanarL1.Columns.Model.Field.NoLowCircular.label line 683
49. lemma OAI.PlanarL1.ColumnOrder.preconnected_comap line 706
50. theorem OAI.PlanarL1.Columns.Model.Field.circular_broad_packing line 732

    Source documentation

    Restricted geometric packing with NO privileged linear cut. The proof rotates the actual model, fields, paths and all distance data at a low column. The result measures separation in the BROAD current intrinsic component.

    theorem circular_broad_packing {n : ℕ} {M : Model (n+1)} {I J K : Set ℝ} {root : Fin (n+1)}
        {W : Type*} [Fintype W] (F : M.Field I 1)
        {S : Set (Fin (n+1))} (hS : (M.link.induce S).Preconnected)
        {cut : Fin (n+1)} (hcut : cut ∈ S)
        (hJK : J ⊆ K) (hKI : K ⊆ I) {a A j ε b : ℝ}
        (hw : ∀ s ∈ K, ∀ t ∈ K, |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 K root) (hc : c.height ∈ J) (hcS : c.column ∉ S)
        (seed : W → M.Point K root) (partner : W → M.Point I root)
        (Dx : ∀ w, F.BandDescent K ((seed w).widen hKI) ε)
        (Dy : ∀ w, F.BandDescent K (partner w) ε)
    …

    Mentions: OAI.PlanarL1.Columns.Model

51. theorem OAI.PlanarL1.Columns.Model.Field.radial_surviving_packing line 799

    Source documentation

    The low-set and circular-gap hypotheses of geometric packing are DERIVED from the actual old chart distance and actual witness descents. This is the band-faithful application of pack:bound to surviving seeds.

    theorem radial_surviving_packing {n : ℕ} {M : Model (n+1)} {I J K : Set ℝ}
        {root : Fin (n+1)} {W : Type*} [Fintype W]
        (hI : IsClosed I) (hJK : J ⊆ K) (hKI : K ⊆ I)
        {a A E δ j ε b : ℝ} (hw : ∀ s ∈ K, ∀ t ∈ K, |s-t| ≤ a)
        (hA₀ : 0 ≤ A) (hA : 2*A ≤ 1) (hE : 0 ≤ E)
        (hsmall : (1:ℝ)/50+a+2*A < 1)
        (hlow : 2*A+E+ε+a < (1:ℝ)/100000-δ) (hhigh : 2*A+a < δ)
        (hb : 0 < b) (hpad : j+ε+2*a ≤ b/4) (hvisit : a ≤ j+ε+2*a)
        (o : M.Point I root) (c : M.Point K root) (hc : c.height ∈ J)
        (seed : W → M.Point K root) (partner : W → M.Point I root)
        (hseed : ∀ w, (seed w).height ∈ J)
        (Dx : ∀ w, o.radialField.BandDescent K ((seed w).widen hKI) ε)
    …

    Mentions: OAI.PlanarL1.Columns.Model