OAI/Computability/Superstring/Counting.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Superstring.Hierarchical.TextOccurs.occurs_word line 11
2. theorem OAI.Superstring.Hierarchical.TextOccurs.agrees_template line 23
3. theorem OAI.Superstring.Counts.Block.text_left line 42
4. theorem OAI.Superstring.Counts.Block.text_right line 48
5. theorem OAI.Superstring.Counts.Block.text_inside line 58
6. theorem OAI.Superstring.Counts.Block.text_boundaries_unique line 70

   Source documentation

   Nearest-mismatch uniqueness on a bi-infinite lift; endpoints may be negative.

   theorem text_boundaries_unique (h : Block A s r j) (h' : Block A s r' j')
       (hr : TextOccurs B r x) (hr' : TextOccurs B r' x') (he : x + j = x' + j') :
       x = x' ∧ r.length = r'.length := by
   …

   Mentions: OAI.Superstring.Counts.Block

7. theorem OAI.Superstring.Counts.Block.of_bounds line 102
8. theorem OAI.Superstring.Hierarchical.Layer.first_containing line 140

   Source documentation

   The first up crossing of an occurrence end is an actual containing window.

   theorem first_containing (D : Layer V B p) (hp : 0 < p) {s : List α} {t : ℤ}
       (hr : D.Records s t) : ∃ a : ℤ,
         a ≤ t ∧ D.first a ≤ t + s.length ∧ t + s.length ≤ D.last a := by
   …

   Mentions: OAI.Superstring.Hierarchical.Layer

9. theorem OAI.Superstring.Hierarchical.Layer.matching_or_block line 160
10. abbrev OAI.Superstring.Hierarchical.Layer.BlockWitness line 231

    Source documentation

    A recorded complete bracketing word and one of its eligible inner placements.

    abbrev BlockWitness (D : Layer V B p) (F : Finset (List α)) (A : ℤ → α) (s : List α) :=
    …

    Mentions: OAI.Superstring.Hierarchical.Layer

11. def OAI.Superstring.Hierarchical.Layer.blockedOccurrence line 234
12. theorem OAI.Superstring.Hierarchical.Layer.blockedOccurrence_injective line 240

    Source documentation

    Injectivity holds modulo one primitive turn, even when a block spans many turns.

    theorem blockedOccurrence_injective (D : Layer V B p) (hp : 0 < p)
        (per : Function.Periodic B (p : ℤ)) (F : Finset (List α)) (A : ℤ → α) (s : List α) :
        Function.Injective (D.blockedOccurrence hp per F A s) := by
    …

    Mentions: OAI.Superstring.Hierarchical.Layer

13. theorem OAI.Superstring.Hierarchical.Layer.card_blockWitness line 291

    Source documentation

    The exact block count for one periodic layer.

    theorem card_blockWitness [DecidableEq α] (D : Layer V B p) (F : Finset (List α))
        (A : ℤ → α) (s : List α) :
        Fintype.card (D.BlockWitness F A s) =
          Counts.blocking F A s (fun r => Fintype.card (D.Occurrence r)) := by
    …

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

14. theorem OAI.Superstring.Hierarchical.Layer.normalize_add line 302

    Source documentation

    Normalization is compatible with moving to an inner occurrence.

    theorem normalize_add (D : Layer V B p) (hp : 0 < p) (per : Function.Periodic B (p : ℤ))
        {r s : List α} {y : ℤ} (hy : D.Records r y) {j : ℕ} (hj : Counts.Occurs r s j) :
        D.normalize hp per (D.records_suboccurrence (D.normalize hp per hy).property hj) =
          D.normalize hp per (D.records_suboccurrence hy hj) := by
    …

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

15. theorem OAI.Superstring.Hierarchical.Layer.matching_of_not_blocked line 319

    Source documentation

    Unblocked occurrences have actual matching windows; no matching-window certificate is assumed in selecting an occurrence later in the algorithm.

    theorem matching_of_not_blocked (D : Layer V B p) (F : Finset (List α))
        (hV : V = (F : Set (List α))) (closed : SubstringClosed V) (hp : 0 < p)
        (per : Function.Periodic B (p : ℤ)) {A : ℤ → α} {s : List α}
        (hA : Counts.Matches A s) (o : D.Occurrence s)
        (ho : ¬ ∃ w : D.BlockWitness F A s, D.blockedOccurrence hp per F A s w = o) :
        ∃ a b : ℤ, a ≤ o.val.val ∧ (o.val.val : ℤ) + s.length ≤ b ∧
          D.first a ≤ b ∧ b ≤ D.last a ∧ AgreeOn B (fun x => A (x - o.val.val)) a b := by
    …

    Mentions: OAI.Superstring.Hierarchical.Layer, OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Counts.Matches, OAI.Superstring.Hierarchical.AgreeOn

16. theorem OAI.Superstring.Hierarchical.Layer.aligned_not_blocked line 344

    Source documentation

    An occurrence whose full-text alignment equals the template is never blocked.

    theorem aligned_not_blocked (D : Layer V B p) (hp : 0 < p)
        (per : Function.Periodic B (p : ℤ)) (F : Finset (List α)) {A : ℤ → α} {s : List α}
        (o : D.Occurrence s) (halign : ∀ x : ℤ, B (x + o.val.val) = A x) :
        ¬ ∃ w : D.BlockWitness F A s, D.blockedOccurrence hp per F A s w = o := by
    …

    Mentions: OAI.Superstring.Hierarchical.Layer

17. abbrev OAI.Superstring.Hierarchical.Family.Occurrence line 370

    Source documentation

    All recorded occurrences, retaining the actual original layer as their owner.

    abbrev Occurrence (s : List α) := Σ i, (D i).Occurrence s

18. abbrev OAI.Superstring.Hierarchical.Family.BlockWitness line 373

    Source documentation

    Bracketing witnesses over the whole fixed family of layers.

    abbrev BlockWitness (F : Finset (List α)) (B : ℤ → α) (s : List α) :=
    …

19. def OAI.Superstring.Hierarchical.Family.blockedOccurrence line 376
20. theorem OAI.Superstring.Hierarchical.Family.blockedOccurrence_injective line 383
21. theorem OAI.Superstring.Hierarchical.Family.card_blockWitness line 391
22. theorem OAI.Superstring.Hierarchical.Family.outside_image_and_pred line 403

    Source documentation

    An actual finite pigeonhole argument used by the period-rule forcing step.

    theorem outside_image_and_pred {X Y : Type} [Fintype X] [Fintype Y]
        (f : X → Y) (P : Y → Prop) [Fintype {y // P y}] (k : ℕ)
        (hX : Fintype.card X + k < Fintype.card Y)
        (hP : Fintype.card {y // P y} ≤ k) :
        ∃ y, (¬ ∃ x, f x = y) ∧ ¬ P y := by
    …

23. theorem OAI.Superstring.Hierarchical.Family.aligned_not_blocked line 427

    Source documentation

    An aligned recorded occurrence is outside the global blocking image.

    theorem aligned_not_blocked (hp : ∀ i, 0 < p i)
        (per : ∀ i, Function.Periodic (A i) (p i : ℤ))
        (F : Finset (List α)) {B : ℤ → α} {s : List α} (o : Occurrence D s)
        (halign : ∀ x : ℤ, A o.1 (x + o.2.val.val) = B x) :
        ¬ ∃ w : BlockWitness D F B s, blockedOccurrence D hp per F B s w = o := by
    …

    Mentions: OAI.Superstring.Hierarchical.Family.Occurrence, OAI.Superstring.Hierarchical.Family.BlockWitness, OAI.Superstring.Hierarchical.Family.blockedOccurrence

24. theorem OAI.Superstring.Hierarchical.Family.blocking_lt_of_aligned line 441
25. theorem OAI.Superstring.Hierarchical.Family.matching_different line 456

    Source documentation

    The excess forced by a period rule produces a matching actual window on a DIFFERENT aligned text. The exceptional set must have the proved size bound k.

    theorem matching_different [DecidableEq α] (hp : ∀ i, 0 < p i)
        (per : ∀ i, Function.Periodic (A i) (p i : ℤ))
        (F : Finset (List α)) (hV : V = (F : Set (List α)))
        (closed : SubstringClosed V) {B : ℤ → α} {s : List α}
        (hB : Counts.Matches B s) (k : ℕ)
        (hexcess : Counts.blocking F B s (fun r => Fintype.card (Occurrence D r)) + k <
          Fintype.card (Occurrence D s))
        (hfew : Nat.card {o : Occurrence D s //
          ∀ x : ℤ, A o.1 (x + o.2.val.val) = B x} ≤ k) :
        ∃ o : Occurrence D s, (¬ ∀ x : ℤ, A o.1 (x + o.2.val.val) = B x) ∧
          ∃ a b : ℤ, a ≤ o.2.val.val ∧ (o.2.val.val : ℤ) + s.length ≤ b ∧
            (D o.1).first a ≤ b ∧ b ≤ (D o.1).last a ∧
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Counts.Matches, OAI.Superstring.Counts.blocking, OAI.Superstring.Hierarchical.Family.Occurrence