CoreWords.lean`

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.FKCRT.PermutationWedge.perm_preserves_range line 12
lemma OAI.FKCRT.PermutationWedge.pow_intertwine line 23
lemma OAI.FKCRT.PermutationWedge.sameCycle_embedding line 29
def OAI.FKCRT.PermutationWedge.vertexEmbeddingEquiv line 40
lemma OAI.FKCRT.PermutationWedge.vertexEmbeddingEquiv_vertex line 45
def OAI.FKCRT.PermutationWedge.dartGraphEmbeddingIso line 51
Source documentation
Relabelling literal darts, without adding edges or collapsing nonzero original distances.
```
def dartGraphEmbeddingIso (f : α → β) (hf : Function.Injective f)
    {p e : Perm α} {q a : Perm β}
    (hp : ∀ x,q (f x)=f (p x)) (he : ∀ x,a (f x)=f (e x)) :
    dartGraph e p ≃g sideGraph a q (Set.range f) (perm_preserves_range f he) where
…
```
Mentions: OAI.FKCRT.PermutationWedge.dartGraph, OAI.FKCRT.PermutationWedge.sideGraph, OAI.FKCRT.PermutationWedge.perm_preserves_range
theorem OAI.FKCRT.PermutationWedge.dartGraph_embedding_edist line 87
lemma OAI.FKCRT.Inventory.formPerm_map_on line 104
lemma OAI.FKCRT.Inventory.StackMatching.unique_first line 111
lemma OAI.FKCRT.Inventory.StackMatching.unique_distance line 119
lemma OAI.FKCRT.Inventory.turns_map_total line 125
lemma OAI.FKCRT.Inventory.StackMatching.map_first line 137
lemma OAI.FKCRT.Inventory.StackMatching.map_distance_of_full line 145
theorem OAI.FKCRT.Inventory.StackMatching.normalized_distance line 161
Source documentation
Compressing an actual isolated core/subtree to its ordered dart positions preserves exact all-edge distances, not only its crossing graph.
```
theorem StackMatching.normalized_distance [Fintype α]
    {w : α → TypedLetter} {l : List α} (M : StackMatching w l) (hn : l.Nodup) :
    ∃ D : StackMatching (w ∘ l.get) (List.finRange l.length),
      ∀ i j,M.distance (l.get i) (l.get j)=D.distance i j := by
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.D
def OAI.FKCRT.Inventory.CoreWord line 191
Source documentation
A connected nonempty typed core, expressed without an arbitrary pairing choice: any matching certificate is the unique literal stack matching.
```
def CoreWord (w : List TypedLetter) : Prop :=
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter
lemma OAI.FKCRT.Inventory.coreWord_empty line 196
lemma OAI.FKCRT.Inventory.coreWord_pos line 200
lemma OAI.FKCRT.Inventory.filter_finRange_eq line 204
lemma OAI.FKCRT.Inventory.StackMatching.closed_subword line 210
theorem OAI.FKCRT.Inventory.normalized_root_core line 228
Source documentation
The actual root component becomes a connected finite core after order compression. No independence law or substituted matching is used.
```
theorem normalized_root_core (w : Fin N→TypedLetter)
    (M : StackMatching w (List.finRange N)) (r : Opener M.mate) (hr : r.val.val=0) :
    CoreWord (((List.finRange N).filter (fun d => decide (d∈componentDarts M.mate r))).map w) := by
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Inventory.CoreWord
theorem OAI.FKCRT.Inventory.successful_core_decomposition line 271
Source documentation
Canonical decomposition of every genuine nonempty successful word into its root connected core and its literal successful corner words.
```
theorem successful_core_decomposition (w : Fin N→TypedLetter)
    (M : StackMatching w (List.finRange N)) (r : Opener M.mate) (hr : r.val.val=0) :
    let l := (rootSplit M.mate r).map (fun x => (w x.1,x.2.map w))
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.StackMatching
lemma OAI.FKCRT.CornerSplit.lift_join line 314
lemma OAI.FKCRT.CornerSplit.join_first_zero line 335
theorem OAI.FKCRT.Inventory.core_matching_at_positions line 358
Source documentation
A genuinely connected typed core remains connected when its positions are stretched by the actual corner inserts, including empty inserts.
```
theorem core_matching_at_positions (w : Fin N→TypedLetter)
    (l : List (Fin N×List (Fin N))) (hjoin : CornerSplit.join l=List.finRange N)
    (hcore : CoreWord ((l.map Prod.fst).map w)) :
    ∃ C : StackMatching w (l.map Prod.fst),∃ r : Opener C.mate,
      r.val.val=0 ∧ ∀ x : Opener C.mate,(Chords.graph C.mate).Reachable r x := by
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.CornerSplit.join, OAI.FKCRT.Inventory.CoreWord, OAI.FKCRT.Inventory.StackMatching, OAI.FKCRT.Chords.graph
theorem OAI.FKCRT.Inventory.core_word_insertion_inverse line 404
Source documentation
Literal inverse with normalized connected words as cores. The graph connectivity and the full matching are constructed from the words.
```
theorem core_word_insertion_inverse (w : Fin N→TypedLetter)
    (l : List (Fin N×List (Fin N))) (hjoin : CornerSplit.join l=List.finRange N)
    (hcore : CoreWord ((l.map Prod.fst).map w))
    (hw : ∀ x∈l,stackTypedRun (x.2.map w) []=some [])
    (M : StackMatching w (List.finRange N)) :
    ∃ r : Opener M.mate,r.val.val=0 ∧ rootSplit M.mate r=l := by
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.CornerSplit.join, OAI.FKCRT.Inventory.CoreWord, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.StackMatching
abbrev OAI.FKCRT.Inventory.EmptyTypedWord line 426
abbrev OAI.FKCRT.Inventory.NonemptyTypedWord line 427
def OAI.FKCRT.Inventory.ValidCorners line 429
lemma OAI.FKCRT.Inventory.ValidCorners.empty line 432
lemma OAI.FKCRT.Inventory.ValidCorners.nonempty line 436
lemma OAI.FKCRT.Inventory.core_lift_valid line 443
theorem OAI.FKCRT.Inventory.valid_corner_injective line 456
Source documentation
Rooted corner substitution is injective for the actual typed-word inventory model, with every corner individually identified.
```
theorem valid_corner_injective {l r : List (TypedLetter×List TypedLetter)}
    (hl : ValidCorners l) (hr : ValidCorners r) (he : cornerInsert l=cornerInsert r) : l=r := by
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.ValidCorners, OAI.FKCRT.Inventory.cornerInsert
theorem OAI.FKCRT.Inventory.exists_valid_corners line 476
Source documentation
Every nonempty successful typed word has its actual unique connected core decomposition; children are strictly shorter, enabling recursion.
```
theorem exists_valid_corners (w : List TypedLetter) (hw : stackTypedRun w []=some [])
    (hne : w≠[]) :
    ∃ l : List (TypedLetter×List TypedLetter),ValidCorners l ∧ cornerInsert l=w ∧
      ∀ x∈l,x.2.length<w.length := by
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.ValidCorners, OAI.FKCRT.Inventory.cornerInsert
abbrev OAI.FKCRT.Inventory.CornerWords line 497
def OAI.FKCRT.Inventory.insertCornerWords line 499
lemma OAI.FKCRT.Inventory.insertCornerWords_bijective line 502
def OAI.FKCRT.Inventory.wordCornerEquiv line 513
Source documentation
Exact finite rooted corner-substitution bijection. This is not an assumed block law, and it preserves all zero-size corner inserts.
```
def wordCornerEquiv : CornerWords ≃ NonemptyTypedWord :=
…
```
Mentions: OAI.FKCRT.Inventory.CornerWords, OAI.FKCRT.Inventory.NonemptyTypedWord
abbrev OAI.FKCRT.Inventory.Core line 524
abbrev OAI.FKCRT.Inventory.CornerData line 525
def OAI.FKCRT.Inventory.cornerList line 527
lemma OAI.FKCRT.Inventory.cornerList_fst line 530
lemma OAI.FKCRT.Inventory.cornerList_valid line 535
def OAI.FKCRT.Inventory.cornersOfData line 543
def OAI.FKCRT.Inventory.dataOfCorners line 546
lemma OAI.FKCRT.Inventory.cornersOfData_dataOfCorners line 550
lemma OAI.FKCRT.Inventory.cornerList_congr_core line 558
lemma OAI.FKCRT.Inventory.cornerList_injective line 564
lemma OAI.FKCRT.Inventory.cornersOfData_injective line 570
lemma OAI.FKCRT.Inventory.dataOfCorners_cornersOfData line 582
def OAI.FKCRT.Inventory.cornerDataEquiv line 585
def OAI.FKCRT.Inventory.coreChildrenEquiv line 592
Source documentation
An exact product description of all nonempty genuine words.
```
def coreChildrenEquiv : CornerData ≃ NonemptyTypedWord := cornerDataEquiv.trans wordCornerEquiv
…
```
Mentions: OAI.FKCRT.Inventory.CornerData, OAI.FKCRT.Inventory.NonemptyTypedWord, OAI.FKCRT.Inventory.wordCornerEquiv