OAI/Computability/Superstring/Groups.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Superstring.Hierarchical.Threading.SameText line 12

   Source documentation

   Full-text translation equivalence. Finite prefixes alone do not identify groups.

   def SameText (C : Threading V ι) (i j : ι) : Prop :=
   …

   Mentions: OAI.Superstring.Hierarchical.Threading

2. def OAI.Superstring.Hierarchical.Threading.textSetoid line 15
3. def OAI.Superstring.Hierarchical.Threading.Groups line 30
4. instance OAI.Superstring.Hierarchical.Threading.(instance at line 32) line 32
5. instance OAI.Superstring.Hierarchical.Threading.(instance at line 36) line 36
6. def OAI.Superstring.Hierarchical.Threading.group line 38
7. def OAI.Superstring.Hierarchical.Threading.groupText line 40
8. def OAI.Superstring.Hierarchical.Threading.groupPeriod line 43
9. theorem OAI.Superstring.Hierarchical.Threading.primitive_group line 46
10. def OAI.Superstring.Hierarchical.Threading.Compatible line 51

    Source documentation

    Alignment with an arbitrary fixed two-sided primitive text.

    def Compatible (C : Threading V ι) (A : ℤ → α) :=
    …

    Mentions: OAI.Superstring.Hierarchical.Threading

11. instance OAI.Superstring.Hierarchical.Threading.(instance at line 54) line 54
12. def OAI.Superstring.Hierarchical.Threading.phaseMap line 58
13. theorem OAI.Superstring.Hierarchical.Threading.phaseMap_injective line 65
14. theorem OAI.Superstring.Hierarchical.Threading.phaseMap_surjective line 87
15. def OAI.Superstring.Hierarchical.Threading.phaseEquiv line 116

    Source documentation

    Every primitive phase and aligned passage occurs exactly once. This is the finite bookkeeping behind splitting a long turn into primitive layers.

    noncomputable def phaseEquiv (C : Threading V ι) {A : ℤ → α} {p : ℕ}
        (hp : Primitive A p) : (Fin p × C.Aligned A) ≃ C.Compatible A :=
    …

    Mentions: OAI.Superstring.Hierarchical.Threading, OAI.Superstring.Hierarchical.Primitive

16. theorem OAI.Superstring.Hierarchical.Threading.compatible_group line 121
17. def OAI.Superstring.Hierarchical.Threading.groupFiberEquiv line 137
18. theorem OAI.Superstring.Hierarchical.Threading.group_card line 141
19. theorem OAI.Superstring.Hierarchical.Threading.sum_layer_periods line 151

    Source documentation

    The exact second budget: primitive period times the number of layers sums to the original number of down steps, hence to W for the base multiplicities.

    theorem sum_layer_periods (C : Threading V ι) :
        ∑ g : C.Groups, C.groupPeriod g * Fintype.card (C.Aligned (C.groupText g)) =
          Fintype.card ι := by
    …

    Mentions: OAI.Superstring.Hierarchical.Threading

20. abbrev OAI.Superstring.Hierarchical.Threading.Phase line 160

    Source documentation

    Primitive phases with stable layer indices.

    abbrev Phase (C : Threading V ι) :=
    …

    Mentions: OAI.Superstring.Hierarchical.Threading

21. instance OAI.Superstring.Hierarchical.Threading.(instance at line 163) line 163
22. def OAI.Superstring.Hierarchical.Threading.groupPhaseEquiv line 167
23. def OAI.Superstring.Hierarchical.Threading.allPhaseEquiv line 173
24. theorem OAI.Superstring.Hierarchical.Threading.allPhaseEquiv_value line 176
25. def OAI.Superstring.Hierarchical.Threading.phaseWord line 182

    Source documentation

    Exit window of a sorted layer at a specified primitive phase.

    noncomputable def phaseWord (C : Threading V ι) (i : C.Phase) : List α :=
    …

    Mentions: OAI.Superstring.Hierarchical.Threading

26. abbrev OAI.Superstring.Hierarchical.Threading.Recorded line 186
27. instance OAI.Superstring.Hierarchical.Threading.(instance at line 188) line 188
28. theorem OAI.Superstring.Hierarchical.Threading.phase_prefix_count line 193

    Source documentation

    Sorting retains every prefix occurrence histogram, not just total edge cost.

    theorem phase_prefix_count [DecidableEq α] (C : Threading V ι) (g : C.Groups)
        (r : Fin (C.groupPeriod g)) (s : List α) :
        (Finset.univ.filter (fun j => s <+: C.phaseWord ⟨g, r, j⟩)).card =
          (Finset.univ.filter (fun j => s <+: C.word (C.allPhaseEquiv ⟨g, r, j⟩))).card := by
    …

    Mentions: OAI.Superstring.Hierarchical.Threading

29. theorem OAI.Superstring.Hierarchical.Threading.card_recorded line 212

    Source documentation

    The recorded-occurrence identity for any threaded circulation.

    theorem card_recorded [DecidableEq α] (C : Threading V ι) (s : List α) :
        Fintype.card (C.Recorded s) =
          (Finset.univ.filter (fun i => s <+: C.word i)).card := by
    …

    Mentions: OAI.Superstring.Hierarchical.Threading

30. theorem OAI.Superstring.Counts.Data.recorded_count line 232
31. theorem OAI.Superstring.Counts.Data.layer_budget line 237
32. def OAI.Superstring.Hierarchical.TextOccurs line 250

    Source documentation

    An occurrence in a two-sided text, retaining its integer origin.

    def TextOccurs (A : ℤ → α) (s : List α) (x : ℤ) : Prop :=
    …

33. theorem OAI.Superstring.Hierarchical.TextOccurs.word line 257
34. theorem OAI.Superstring.Hierarchical.TextOccurs.eq_word line 262
35. theorem OAI.Superstring.Hierarchical.TextOccurs.get line 270
36. theorem OAI.Superstring.Hierarchical.TextOccurs.unique line 273
37. theorem OAI.Superstring.Hierarchical.TextOccurs.trans line 277
38. theorem OAI.Superstring.Hierarchical.TextOccurs.shift line 285
39. theorem OAI.Superstring.Hierarchical.TextOccurs.prefix_iff line 295
40. def OAI.Superstring.Hierarchical.Layer.Records line 320

    Source documentation

    The entire recording criterion is the exit window at the occurrence start.

    def Records (D : Layer V A p) (s : List α) (x : ℤ) : Prop :=
    …

    Mentions: OAI.Superstring.Hierarchical.Layer

41. theorem OAI.Superstring.Hierarchical.Layer.records_iff_prefix line 323
42. theorem OAI.Superstring.Hierarchical.Layer.records_shift line 329
43. def OAI.Superstring.Hierarchical.Layer.Occurrence line 336
44. instance OAI.Superstring.Hierarchical.Layer.(instance at line 339) line 339
45. def OAI.Superstring.Hierarchical.Layer.normalize line 344

    Source documentation

    Normalize an arbitrary lift of a recorded occurrence to its primitive phase.

    def normalize (D : Layer V A p) (hp : 0 < p) (per : Function.Periodic A (p : ℤ))
        {s : List α} {x : ℤ} (h : D.Records s x) : D.Occurrence s := by
    …

    Mentions: OAI.Superstring.Hierarchical.Layer

46. theorem OAI.Superstring.Hierarchical.Layer.normalize_val line 357
47. theorem OAI.Superstring.Hierarchical.Layer.records_suboccurrence line 365

    Source documentation

    Every nonempty suboccurrence of a recorded interval is again recorded.

    theorem records_suboccurrence (D : Layer V A p) {s r : List α} {x : ℤ} {j : ℕ}
        (hr : D.Records r x) (hs : Counts.Occurs r s j) : D.Records s (x + j) := by
    …

    Mentions: OAI.Superstring.Hierarchical.Layer, OAI.Superstring.Counts.Occurs