CornerInsertion.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.FKCRT.Inventory.typedStep_suffix line 10
lemma OAI.FKCRT.Inventory.flexibleClosing_suffix line 20
lemma OAI.FKCRT.Inventory.typedRun_suffix line 29
lemma OAI.FKCRT.Inventory.flexibleCount_append line 48
lemma OAI.FKCRT.Inventory.empty_word_context line 62
def OAI.FKCRT.Inventory.cornerInsert line 67
Source documentation
Literal corner insertion, keeping the root skeleton letters in order.
```
def cornerInsert (l : List (TypedLetter×List TypedLetter)) : List TypedLetter :=
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter
theorem OAI.FKCRT.Inventory.cornerInsert_run_count line 73
Source documentation
Successful corner words preserve the current stack and have exactly the same flexible exponent there as from the empty stack. This proves weight multiplicativity, including empty inserts, with no independence hypothesis.
```
theorem cornerInsert_run_count (l : List (TypedLetter×List TypedLetter))
    (hg : ∀ x∈l,stackTypedRun x.2 []=some []) {s t : List Bool}
    (h : stackTypedRun (l.map Prod.fst) s=some t) :
    stackTypedRun (cornerInsert l) s=some t ∧
      flexibleCount (cornerInsert l) s=flexibleCount (l.map Prod.fst) s+
        (l.map (fun x => flexibleCount x.2 [])).sum := by
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.cornerInsert, OAI.FKCRT.Inventory.flexibleCount
def OAI.FKCRT.CornerSplit.split line 110
Source documentation
Split at marked letters, retaining every letter and the possibly empty prefix before the first mark. The marks themselves label the corners.
```
def split (p : α→Bool) : List α→List α × List (α×List α)
  | [] => ([],[])
  | a::w => let r := split p w
…
```
def OAI.FKCRT.CornerSplit.join line 115
lemma OAI.FKCRT.CornerSplit.reassemble line 117
lemma OAI.FKCRT.CornerSplit.skeleton line 124
lemma OAI.FKCRT.CornerSplit.unmarked_prefix line 130
lemma OAI.FKCRT.CornerSplit.marked_corners line 139
lemma OAI.FKCRT.CornerSplit.prefix_nil line 153
lemma OAI.FKCRT.CornerSplit.split_unmarked_append line 156
lemma OAI.FKCRT.CornerSplit.split_join line 167
Source documentation
Exact inverse, including empty corner inserts and the final corner.
```
lemma split_join (p : α→Bool) (l : List (α×List α))
    (h : ∀ x∈l,p x.1=true ∧ ∀ a∈x.2,p a=false) :
    split p (join l)=([],l) := by
…
```
Mentions: OAI.FKCRT.CornerSplit.split, OAI.FKCRT.CornerSplit.join
lemma OAI.FKCRT.CornerSplit.join_injective_on line 180
lemma OAI.FKCRT.CornerSplit.join_first_marked line 187
lemma OAI.FKCRT.CornerSplit.located line 197
Source documentation
Every extracted corner is an actual consecutive interval, bounded on its right by the next marked letter (or the end of the word).
```
lemma located (p : α→Bool) (w : List α) (x : α×List α) (hx : x∈(split p w).2) :
    ∃ u v,w=u++x.1::(x.2++v) ∧
      (v=[] ∨ ∃ b t,v=b::t ∧ p b=true) := by
…
```
Mentions: OAI.FKCRT.CornerSplit.split

theorem OAI.FKCRT.MapCycles.scanArches_corners line 230

Source documentation

Empty corner scans preserve the pre-existing stack while contributing exactly their own pairs. Thus insertion creates no cross-corner matching.

theorem scanArches_corners (f : α→Option Bool) (l : List (α×List α))
    (G : α×List α→List (α×α))
    (hg : ∀ x∈l,∀ S,scanArches f x.2 S=some (S,G x))
    {S T : List α} {E : List (α×α)}
    (h : scanArches f (l.map Prod.fst) S=some (T,E)) :
    ∃ F,scanArches f (CornerSplit.join l) S=some (T,F) ∧
      F.Perm (E++l.flatMap G) := by
…

Mentions: OAI.FKCRT.MapCycles.scanArches, OAI.FKCRT.CornerSplit.join

lemma OAI.FKCRT.MapCycles.scanArches_suffix line 267

Source documentation

A standalone empty scan is unchanged by an arbitrary underlying stack.

lemma scanArches_suffix (f : α→Option Bool) {l S T : List α} {E : List (α×α)}
    (h : scanArches f l S=some (T,E)) (R : List α) :
    scanArches f l (S++R)=some (T++R,E) := by
…

Mentions: OAI.FKCRT.MapCycles.scanArches

theorem OAI.FKCRT.Inventory.ordered_matchings line 305

Source documentation

Matchings on an arbitrary ordered subword. The original positions are retained, so this lemma can be applied inside a larger inventory word.

theorem ordered_matchings (w : α→TypedLetter) (l : List α)
    (hw : stackTypedRun (l.map w) []=some []) :
    ∃ E F : List (α×α),Arches l E ∧ Arches l F ∧
      (endpoints (E++F)).Perm l ∧
      (∀ e∈E,w e.1=.burger true ∧ w e.2=.order true) ∧
      (∀ e∈F,w e.1=.burger false ∧ w e.2=.order false) := by
…

Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.stackTypedRun

theorem OAI.FKCRT.Inventory.empty_typed_scan line 342
Source documentation
An actually empty typed subword has a deterministic one-colour matching which is unchanged by any underlying stack.
```
theorem empty_typed_scan (w : α→TypedLetter) (l : List α) (hn : l.Nodup)
    (hw : stackTypedRun (l.map w) []=some []) (c : Bool) :
    ∃ E, (∀ S,scanArches (fun x => colorInstruction c (w x)) l S=some (S,E)) ∧
      (endpoints E).Perm (l.filter (fun x => (w x).color == c)) := by
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.colorInstruction

lemma OAI.FKCRT.MapCycles.scanArches_interval_subset line 422

Source documentation

Exact locality of the actual stack matching on an empty interval.

lemma scanArches_interval_subset (f : α→Option Bool) (u v z S T : List α)
    {E G : List (α×α)} (h : scanArches f (u++(v++z)) S=some (T,E))
    (hv : scanArches f v []=some ([],G)) : ∀ e∈G,e∈E := by
…

Mentions: OAI.FKCRT.MapCycles.scanArches

theorem OAI.FKCRT.Inventory.empty_interval_matching_closed line 447

Source documentation

Any actual successful consecutive subword is closed under the full word's matching. In particular successful corner inserts do not rematch an old endpoint to a new one.

theorem empty_interval_matching_closed (w : α→TypedLetter) (u v z : List α)
    (hn : (u++(v++z)).Nodup) (E F : List (α×α))
    (hE : Arches (u++(v++z)) E) (hF : Arches (u++(v++z)) F)
    (hcov : (endpoints (E++F)).Perm (u++(v++z)))
    (htE : ∀ e∈E,w e.1=.burger true ∧ w e.2=.order true)
    (htF : ∀ e∈F,w e.1=.burger false ∧ w e.2=.order false)
    (hv : stackTypedRun (v.map w) []=some []) :
    ∀ d∈v,turns (E++F) d∈v := by
…

Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.stackTypedRun

lemma OAI.FKCRT.Chords.gapIndex_strict line 498
def OAI.FKCRT.Chords.rootSplit line 512
lemma OAI.FKCRT.Chords.rootSplit_prefix line 515
lemma OAI.FKCRT.Chords.rootSplit_join line 526
theorem OAI.FKCRT.Chords.rootSplit_closed line 534
Source documentation
The literal interval chunks extracted from a root crossing component are closed under the actual edge pairing. No fresh independent matching is substituted at the corners.
```
theorem rootSplit_closed (a : Perm (Fin N)) (ha : Function.Involutive a)
    (hf : ∀ d,a d≠d) (r : Opener a) (hr : r.val.val=0)
    (x : Fin N×List (Fin N)) (hx : x∈rootSplit a r) :
    ∀ d∈x.2,a d∈x.2 := by
…
```
Mentions: OAI.FKCRT.Chords.Opener, OAI.FKCRT.Chords.rootSplit
lemma OAI.FKCRT.Chords.rootSplit_length_lt line 571
lemma OAI.FKCRT.Inventory.cornerInsert_map line 585

theorem OAI.FKCRT.Inventory.root_component_decomposition line 593

Source documentation

The exact forward rooted-corner decomposition of a genuine matching word, including successful empty corners and multiplicative activity weight.

theorem root_component_decomposition (a : Perm (Fin N)) (ha : Function.Involutive a)
    (hf : ∀ d,a d≠d) (c : Fin N→Bool) (hc : ∀ d,c (a d)=c d)
    (hn : ∀ x y,c x=c y → x<y → y<a x → a x<a y → False)
    (r : Opener a) (hr : r.val.val=0) :
    let l := (rootSplit a r).map (fun x => (pairWord a c x.1,x.2.map (pairWord a c)))
…

Mentions: OAI.FKCRT.Inventory.pairWord

lemma OAI.FKCRT.Chords.chunk_convex line 640

Source documentation

Consecutive chunks are order-convex in the actual dart tour.

lemma chunk_convex (p : Fin N→Bool) (x : Fin N×List (Fin N))
    (hx : x∈(CornerSplit.split p (List.finRange N)).2)
    {i j k : Fin N} (hi : i∈x.2) (hj : j∈x.2) (hik : i≤k) (hkj : k≤j) : k∈x.2 := by
…

Mentions: OAI.FKCRT.CornerSplit.split

lemma OAI.FKCRT.Chords.unmarked_in_chunk line 658

theorem OAI.FKCRT.Chords.no_cross_core_corner line 677

Source documentation

Matching edges in distinct empty corners cannot cross a core edge.

theorem no_cross_core_corner (a : Perm (Fin N)) (p : Fin N→Bool)
    (hcore : ∀ d,p (a d)=p d)
    (hchunks : ∀ x∈(CornerSplit.split p (List.finRange N)).2,∀ d∈x.2,a d∈x.2)
    (hp : ∀ d : Fin N,d.val=0 → p d=true)
    (x y : Opener a) (hx : p x.val=true) (hy : p y.val=false) : ¬Cross a x y := by
…

Mentions: OAI.FKCRT.CornerSplit.split, OAI.FKCRT.Chords.Opener, OAI.FKCRT.Chords.Cross

theorem OAI.FKCRT.Chords.root_component_of_core line 699

Source documentation

Insertion cannot enlarge a connected root core. Reachability here is inside the finite crossing graph, not a probabilistic limiting assertion.

theorem root_component_of_core (a : Perm (Fin N)) (ha : Function.Involutive a)
    (hf : ∀ d,a d≠d) (p : Fin N→Bool) (r : Opener a) (hr : r.val.val=0)
    (hp : p r.val=true) (hcore : ∀ d,p (a d)=p d)
    (hchunks : ∀ x∈(CornerSplit.split p (List.finRange N)).2,∀ d∈x.2,a d∈x.2)
    (hconnected : ∀ x : Opener a,p x.val=true → (graph a).Reachable r x) :
    componentDarts a r=Finset.univ.filter (fun d => p d=true) := by
…

Mentions: OAI.FKCRT.Chords.Opener, OAI.FKCRT.CornerSplit.split, OAI.FKCRT.Chords.graph, OAI.FKCRT.Chords.componentDarts