Counts.lean`

81 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Superstring.Counts.Occurs line 13
Source documentation
A substring occurrence retains its starting position, so overlapping occurrences are counted separately.
```
def Occurs (T s : List α) (x : ℕ) : Prop :=
…
```
instance OAI.Superstring.Counts.(instance at line 16) line 16
abbrev OAI.Superstring.Counts.Occurrence line 19
def OAI.Superstring.Counts.number line 21
theorem OAI.Superstring.Counts.Occurs.at line 23
theorem OAI.Superstring.Counts.Occurs.refl line 26
theorem OAI.Superstring.Counts.Occurs.trans line 29
theorem OAI.Superstring.Counts.Occurs.infix line 37
theorem OAI.Superstring.Counts.Occurs.unique line 48
def OAI.Superstring.Counts.Block line 58
Source documentation
The inner occurrence is strictly inside the two single-letter mismatches.
```
def Block (A : ℤ → α) (s r : List α) (j : ℕ) : Prop :=
…
```
instance OAI.Superstring.Counts.(instance at line 65) line 65
abbrev OAI.Superstring.Counts.BlockPosition line 68
def OAI.Superstring.Counts.coefficient line 71
def OAI.Superstring.Counts.blocking line 74
theorem OAI.Superstring.Counts.Block.length_pos line 81
theorem OAI.Superstring.Counts.Block.left line 83
theorem OAI.Superstring.Counts.Block.right line 92
theorem OAI.Superstring.Counts.Block.inside line 104
theorem OAI.Superstring.Counts.Block.boundaries_unique line 119
abbrev OAI.Superstring.Counts.BlockWitness line 150
Source documentation
A recorded bracketing word occurrence, and a counted placement inside it.
```
abbrev BlockWitness (V : Finset (List α)) (T : List α) (A : ℤ → α) (s : List α) :=
…
```
def OAI.Superstring.Counts.blockedOccurrence line 154
Source documentation
The blocked-occurrence map.
```
def blockedOccurrence (V : Finset (List α)) (T : List α) (A : ℤ → α) (s : List α)
    (w : BlockWitness V T A s) : Occurrence T s :=
…
```
Mentions: OAI.Superstring.Counts.BlockWitness, OAI.Superstring.Counts.Occurrence
theorem OAI.Superstring.Counts.blockedOccurrence_injective line 159
theorem OAI.Superstring.Counts.card_blockWitness line 176
theorem OAI.Superstring.Counts.blocking_le_number line 186
theorem OAI.Superstring.Counts.coefficient_pos_length line 193
Source documentation
Positivity of a coefficient forces the strict length dependency used in both the descending recursion and its occurrence-bound induction.
```
theorem coefficient_pos_length [DecidableEq α] {A : ℤ → α} {s r : List α}
    (h : 0 < coefficient A s r) : s.length + 2 ≤ r.length := by
…
```
Mentions: OAI.Superstring.Counts.coefficient
def OAI.Superstring.Counts.Matches line 201
Source documentation
Agreement with a template at origin zero, as in every count rule.
```
def Matches (A : ℤ → α) (s : List α) : Prop :=
…
```
theorem OAI.Superstring.Counts.periodic_nat_add line 204
theorem OAI.Superstring.Counts.periodic_nat_sub line 208

theorem OAI.Superstring.Counts.period_prefix line 213

Source documentation

All period-spaced prefixes of a rule's longer word are genuine occurrences.

theorem period_prefix {A : ℤ → α} {p t : ℕ} {v w : List α}
    (per : Function.Periodic A (p : ℤ)) (hv : Matches A v) (hw : Matches A w)
    (hlen : t * p + w.length ≤ v.length) : Occurs v w (t * p) := by
…

Mentions: OAI.Superstring.Counts.Matches, OAI.Superstring.Counts.Occurs

theorem OAI.Superstring.Counts.Block.shift line 226
Source documentation
A bracketing placement of the long word generates every period-spaced placement of its short prefix in the SAME bracketing word.
```
theorem Block.shift {A : ℤ → α} {p t j : ℕ} {v w r : List α}
    (h : Block A v r j) (per : Function.Periodic A (p : ℤ))
    (hv : Matches A v) (hw : Matches A w) (hlen : t * p + w.length ≤ v.length) :
    Block A w r (j + t * p) := by
…
```
Mentions: OAI.Superstring.Counts.Block, OAI.Superstring.Counts.Matches

theorem OAI.Superstring.Counts.coefficient_amplification line 246

Source documentation

Coefficient amplification for occurrence counts.

theorem coefficient_amplification [DecidableEq α] {A : ℤ → α} {p k : ℕ}
    {v w r : List α} (hp : 0 < p) (per : Function.Periodic A (p : ℤ))
    (hv : Matches A v) (hw : Matches A w) (hlen : w.length + k * p = v.length)
    (hb : 0 < coefficient A v r) : k + 1 ≤ coefficient A w r := by
…

Mentions: OAI.Superstring.Counts.Matches, OAI.Superstring.Counts.coefficient

theorem OAI.Superstring.Counts.Occurs.factor line 266

Source documentation

Restrict an occurrence through another containing occurrence.

theorem Occurs.factor {T r v : List α} {x y : ℕ}
    (hr : Occurs T r y) (hv : Occurs T v x) (hyx : y ≤ x)
    (hend : x + v.length ≤ y + r.length) : Occurs r v (x - y) := by
…

Mentions: OAI.Superstring.Counts.Occurs

theorem OAI.Superstring.Counts.Block.expand line 280
Source documentation
Retarget a block by a whole number of template periods, when the enlarged inner occurrence still lies strictly between the same mismatch letters.
```
theorem Block.expand {A : ℤ → α} {p t j j' : ℕ} {v w r : List α}
    (h : Block A w r j) (per : Function.Periodic A (p : ℤ)) (hj : j = j' + t * p)
    (hj' : 1 ≤ j') (hlen : j' + v.length < r.length) (hr : Occurs r v j') :
    Block A v r j' := by
…
```
Mentions: OAI.Superstring.Counts.Block, OAI.Superstring.Counts.Occurs

theorem OAI.Superstring.Counts.Block.encloses_matching line 299

Source documentation

A blocking pair around a period-spaced short occurrence inside a matching long word must lie outside that entire long occurrence, and blocks it too.

theorem Block.encloses_matching {A : ℤ → α} {T v w r : List α} {p t x y j : ℕ}
    (h : Block A w r j) (hr : Occurs T r y) (hv : Occurs T v x)
    (hmatch : Matches A v) (per : Function.Periodic A (p : ℤ))
    (hlen : t * p + w.length ≤ v.length) (hpos : y + j = x + t * p) :
    ∃ j', Block A v r j' ∧ y + j' = x := by
…

Mentions: OAI.Superstring.Counts.Block, OAI.Superstring.Counts.Occurs, OAI.Superstring.Counts.Matches

def OAI.Superstring.Counts.periodOccurrence line 336

Source documentation

A period-spaced suboccurrence of a fixed long occurrence.

def periodOccurrence {A : ℤ → α} {T v w : List α} {p k : ℕ}
    (per : Function.Periodic A (p : ℤ)) (hv : Matches A v) (hw : Matches A w)
    (hlen : w.length + k * p = v.length) (o : Occurrence T v) (t : Fin (k + 1)) :
    Occurrence T w :=
…

Mentions: OAI.Superstring.Counts.Matches, OAI.Superstring.Counts.Occurrence

theorem OAI.Superstring.Counts.periodOccurrence_injective line 346
def OAI.Superstring.Counts.Unblocked line 358
theorem OAI.Superstring.Counts.Unblocked.period_prefix line 361
theorem OAI.Superstring.Counts.unblocked_count_growth line 382
theorem OAI.Superstring.Counts.blocking_mono line 405
Source documentation
The functional depends monotonically only on words STRICTLY longer than its inner word, although the triggered count operator itself need not be monotone.
```
theorem blocking_mono [DecidableEq α] {V : Finset (List α)} {A : ℤ → α}
    {s : List α} {m n : List α → ℕ}
    (hmn : ∀ r ∈ V, s.length < r.length → m r ≤ n r) :
    blocking V A s m ≤ blocking V A s n := by
…
```
Mentions: OAI.Superstring.Counts.blocking

theorem OAI.Superstring.Counts.sum_increase line 417

Source documentation

Retaining the increase at one summand while all other summands increase.

theorem sum_increase {ι : Type} [DecidableEq ι] (I : Finset ι) (a b : ι → ℕ)
    (h : ∀ i ∈ I, a i ≤ b i) {r : ι} (hr : r ∈ I) :
    (∑ i ∈ I, a i) + (b r - a r) ≤ ∑ i ∈ I, b i := by
…

theorem OAI.Superstring.Counts.period_rule_lower_bound line 428
theorem OAI.Superstring.Counts.exists_occurs_of_infix line 478
theorem OAI.Superstring.Counts.number_pos_of_infix line 486
theorem OAI.Superstring.Counts.Occurs.cons_tail line 492
theorem OAI.Superstring.Counts.Occurs.append_init line 499
theorem OAI.Superstring.Counts.left_extension_number line 508
Source documentation
Disjointness of preceding-letter occurrence classes gives the first extension lower bound in the count recursion.
```
theorem left_extension_number [DecidableEq α] (alphabet : Finset α) (T w : List α) :
    (∑ c ∈ alphabet, number T (c :: w)) ≤ number T w := by
…
```
Mentions: OAI.Superstring.Counts.number
theorem OAI.Superstring.Counts.right_extension_number line 531
Source documentation
The analogous following-letter occurrence classes are disjoint too.
```
theorem right_extension_number [DecidableEq α] (alphabet : Finset α) (T w : List α) :
    (∑ c ∈ alphabet, number T (w ++ [c])) ≤ number T w := by
…
```
Mentions: OAI.Superstring.Counts.number
structure OAI.Superstring.Counts.Data line 555
Source documentation
Finite data of the preprocessed instance; geometric hypotheses are proved for the actual input construction below, not hidden in this record.
```
structure Data (α : Type) where
…
```
def OAI.Superstring.Counts.finiteText line 562
Source documentation
The unique period-p text determined by the first p letters of v. Fallback values are never used in a valid rule, since there 0 < p < length v.
```
def finiteText [Inhabited α] (v : List α) (p : ℕ) (x : ℤ) : α :=
…
```
theorem OAI.Superstring.Counts.finiteText_periodic line 565
instance OAI.Superstring.Counts.(instance at line 570) line 570

theorem OAI.Superstring.Counts.blocking_congr line 574

Source documentation

Equality of the longer counts preserves a blocking functional.

theorem blocking_congr [DecidableEq α] {V : Finset (List α)} {A : ℤ → α}
    {s : List α} {m n : List α → ℕ}
    (hmn : ∀ r ∈ V, s.length < r.length → m r = n r) :
    blocking V A s m = blocking V A s n := by
…

Mentions: OAI.Superstring.Counts.blocking

def OAI.Superstring.Counts.Data.rule line 590
def OAI.Superstring.Counts.Data.rules line 598
Source documentation
Finite enumeration of ALL rules; no least-period restriction is imposed.
```
def rules (D : Data α) (m : List α → ℕ) (w : List α) : ℕ :=
…
```
Mentions: OAI.Superstring.Counts.Data
def OAI.Superstring.Counts.Data.left line 602
def OAI.Superstring.Counts.Data.right line 605
def OAI.Superstring.Counts.Data.step line 609
def OAI.Superstring.Counts.Data.stage line 616
Source documentation
Parallel triangular evaluation; the stabilization proof below shows that this computes the exact descending recursion, rather than a different fixed point.
```
def stage (D : Data α) : ℕ → List α → ℕ
  | 0 => fun _ => 0
  | n + 1 => D.step (D.stage n)
```
Mentions: OAI.Superstring.Counts.Data
def OAI.Superstring.Counts.Data.depth line 620
def OAI.Superstring.Counts.Data.count line 622
theorem OAI.Superstring.Counts.Data.step_le_number line 624
theorem OAI.Superstring.Counts.Data.stage_le_number line 668
Source documentation
Every intermediate computational stage, not only the final counts, is bounded by the occurrence counts of EVERY common superstring.
```
theorem stage_le_number (D : Data α) (T : List α)
    (hinput : ∀ w ∈ D.required, w <:+: T) (n : ℕ) (w : List α) :
    D.stage n w ≤ number T w := by
…
```
Mentions: OAI.Superstring.Counts.Data, OAI.Superstring.Counts.number

theorem OAI.Superstring.Counts.Data.rule_congr line 676

Source documentation

A rule value depends only on strictly longer words.

theorem rule_congr (D : Data α) {m n : List α → ℕ} {w v : List α} (p k : ℕ)
    (hvV : v ∈ D.vertices)
    (hmn : ∀ r ∈ D.vertices, w.length < r.length → m r = n r) :
    D.rule m w v p k = D.rule n w v p k := by
…

Mentions: OAI.Superstring.Counts.Data

theorem OAI.Superstring.Counts.Data.step_congr line 696

Source documentation

Triangularity of the complete finite operator.

theorem step_congr (D : Data α) {m n : List α → ℕ} {w : List α}
    (hmn : ∀ r ∈ D.vertices, w.length < r.length → m r = n r) :
    D.step m w = D.step n w := by
…

Mentions: OAI.Superstring.Counts.Data

theorem OAI.Superstring.Counts.Data.stage_stable line 722
Source documentation
After n stages every word less than n levels from the top has stabilized.
```
theorem stage_stable (D : Data α) (n : ℕ) (w : List α)
    (hdepth : D.depth < w.length + n) : D.stage (n + 1) w = D.stage n w := by
…
```
Mentions: OAI.Superstring.Counts.Data
theorem OAI.Superstring.Counts.Data.count_fixed line 738
Source documentation
The actual counts satisfy exactly the minimal-bound recursion.
```
theorem count_fixed (D : Data α) (w : List α) : D.step D.count w = D.count w := by
…
```
Mentions: OAI.Superstring.Counts.Data
theorem OAI.Superstring.Counts.Data.count_le_number line 742
theorem OAI.Superstring.Counts.Data.count_zero line 746
theorem OAI.Superstring.Counts.Data.required_le_count line 757
theorem OAI.Superstring.Counts.Data.left_le_count line 764
theorem OAI.Superstring.Counts.Data.right_le_count line 770
theorem OAI.Superstring.Counts.Data.left_count line 776
theorem OAI.Superstring.Counts.Data.right_count line 784
theorem OAI.Superstring.Counts.Data.rule_le_count line 792
theorem OAI.Superstring.Counts.finiteText_eq line 813
Source documentation
The finite rule representative is the original two-sided text, not merely its forward restriction.
```
theorem finiteText_eq [Inhabited α] {A : ℤ → α} {v : List α} {p : ℕ}
    (hp : 0 < p) (hper : Function.Periodic A (p : ℤ))
    (hm : Matches A v) (hlen : p ≤ v.length) : finiteText v p = A := by
…
```
Mentions: OAI.Superstring.Counts.Matches, OAI.Superstring.Counts.finiteText

theorem OAI.Superstring.Counts.Data.period_rule line 832

Source documentation

Every period rule holds for the computed counts.

theorem period_rule (D : Data α) {A : ℤ → α} {w v : List α} {p k : ℕ}
    (hp : 0 < p) (hk : 0 < k) (hper : Function.Periodic A (p : ℤ))
    (hw : w ∈ D.vertices) (hne : w ≠ []) (hv : v ∈ D.vertices)
    (hmv : Matches A v) (hmw : Matches A w)
    (hlen : w.length + k * p = v.length)
    (htrigger : blocking D.vertices A v D.count < D.count v) :
    blocking D.vertices A w D.count + k + 1 ≤ D.count w := by
…

Mentions: OAI.Superstring.Counts.Data, OAI.Superstring.Counts.Matches, OAI.Superstring.Counts.blocking

theorem OAI.Superstring.Counts.number_le_length line 851
Source documentation
Nonempty occurrences inject into the positions of the ambient word.
```
theorem number_le_length [DecidableEq α] {T s : List α} (hs : s ≠ []) : number T s ≤ T.length := by
…
```
Mentions: OAI.Superstring.Counts.number
theorem OAI.Superstring.Counts.singleton_number_sum line 864
Source documentation
Counts of one-letter occurrences, independently of how large the alphabet of labels is, sum to at most the symbol length of the ambient word.
```
theorem singleton_number_sum [DecidableEq α] (C : Finset α) (T : List α) :
    (∑ c ∈ C, number T [c]) ≤ T.length := by
…
```
Mentions: OAI.Superstring.Counts.number
def OAI.Superstring.Counts.Data.weight line 887
theorem OAI.Superstring.Counts.Data.weight_le_length line 889