Periods.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.Superstring.Hierarchical.Primitive line 12
Source documentation
The least positive period is explicit, as required for primitive groups.
```
structure Primitive (A : ℤ → α) (p : ℕ) : Prop where
…
```
theorem OAI.Superstring.Hierarchical.exists_primitive line 18
Source documentation
Existence from any positive turn length.
```
theorem exists_primitive {A : ℤ → α} {P : ℕ} (hP : 0 < P)
    (hper : Function.Periodic A (P : ℤ)) : ∃ p, Primitive A p := by
…
```
Mentions: OAI.Superstring.Hierarchical.Primitive
theorem OAI.Superstring.Hierarchical.Primitive.period_iff_dvd line 28
Source documentation
All translational symmetries, including negative ones, are precisely the multiples of the primitive period.
```
theorem Primitive.period_iff_dvd {A : ℤ → α} {p : ℕ} (h : Primitive A p) (d : ℤ) :
    Function.Periodic A d ↔ (p : ℤ) ∣ d := by
…
```
Mentions: OAI.Superstring.Hierarchical.Primitive

theorem OAI.Superstring.Hierarchical.Primitive.alignment_unique line 52

Source documentation

There is exactly one identical full-text alignment in a primitive turn.

theorem Primitive.alignment_unique {A : ℤ → α} {p : ℕ} (h : Primitive A p)
    {i j : ℤ} (hi : 0 ≤ i) (hip : i < p) (hj : 0 ≤ j) (hjp : j < p)
    (heq : ∀ x, A (x + i) = A (x + j)) : i = j := by
…

Mentions: OAI.Superstring.Hierarchical.Primitive

def OAI.Superstring.OrderStats.sortedList line 77
theorem OAI.Superstring.OrderStats.sortedList_length line 80
def OAI.Superstring.OrderStats.order line 83
theorem OAI.Superstring.OrderStats.monotone_order line 86
theorem OAI.Superstring.OrderStats.ofFn_order line 92
theorem OAI.Superstring.OrderStats.order_mem line 97

theorem OAI.Superstring.OrderStats.countP_ofFn line 103

Source documentation

Counting a finite function's values is the same on its explicit list.

theorem countP_ofFn {γ : Type} (P : γ → Bool) (f : Fin n → γ) :
    (List.ofFn f).countP P = ∑ i : Fin n, if P (f i) then 1 else 0 := by
…

theorem OAI.Superstring.OrderStats.card_filter_order line 113

Source documentation

Sorting preserves all value multiplicities, including repetitions.

theorem card_filter_order (f : Fin n → β) (P : β → Prop) [DecidablePred P] :
    (Finset.univ.filter (fun i => P (order f i))).card =
      (Finset.univ.filter (fun i => P (f i))).card := by
…

Mentions: OAI.Superstring.OrderStats.order

theorem OAI.Superstring.OrderStats.monotone_count_iff line 123

Source documentation

Order statistics characterized by cumulative counts.

theorem monotone_count_iff {f : Fin n → β} (hm : Monotone f) (i : Fin n) (t : β) :
    f i ≤ t ↔ i.val < (Finset.univ.filter (fun j => f j ≤ t)).card := by
…

theorem OAI.Superstring.OrderStats.order_le_iff line 145
theorem OAI.Superstring.OrderStats.order_le_order line 150
Source documentation
A coordinatewise increasing matching remains increasing after sorting.
```
theorem order_le_order {f g : Fin n → β} (h : ∀ i, f i ≤ g i) (i : Fin n) :
    order f i ≤ order g i := by
…
```
Mentions: OAI.Superstring.OrderStats.order
theorem OAI.Superstring.OrderStats.order_eq_of_counts line 158
theorem OAI.Superstring.OrderStats.order_add line 166

theorem OAI.Superstring.OrderStats.sorted_window line 180

Source documentation

No artificial window is introduced by sorting matched passages.

theorem sorted_window {entry exit : Fin n → β} (i : Fin n) {e : β}
    (hentry : order entry i ≤ e) (hexit : e ≤ order exit i) :
    ∃ j, entry j ≤ e ∧ e ≤ exit j := by
…

Mentions: OAI.Superstring.OrderStats.order

theorem OAI.Superstring.OrderStats.sorted_edge_count line 203
Source documentation
Exact upward-unit-edge conservation. For each height, sorting preserves the number of vertical intervals traversing it, not just the set of vertices.
```
theorem sorted_edge_count {entry exit : Fin n → ℤ} (h : ∀ j, entry j ≤ exit j) (e : ℤ) :
    (Finset.univ.filter (fun j => order entry j ≤ e ∧ e < order exit j)).card =
      (Finset.univ.filter (fun j => entry j ≤ e ∧ e < exit j)).card := by
…
```
Mentions: OAI.Superstring.OrderStats.order

theorem OAI.Superstring.PrefixMatching.hall line 243

Source documentation

A direct laminar Hall argument. Prefix requests can be assigned distinct extensions precisely when every prefix subtree has enough capacity.

theorem hall (request : ι → List α) (supply : κ → List α)
    (hcapacity : ∀ w, (Finset.univ.filter (fun i => w <+: request i)).card ≤
      (Finset.univ.filter (fun j => w <+: supply j)).card) :
    ∃ f : ι → κ, Function.Injective f ∧ ∀ i, request i <+: supply (f i) := by
…

theorem OAI.Superstring.PrefixMatching.permutation line 302

Source documentation

On equal finite token sets the matching is a permutation.

theorem permutation (request supply : ι → List α)
    (hcapacity : ∀ w, (Finset.univ.filter (fun i => w <+: request i)).card ≤
      (Finset.univ.filter (fun j => w <+: supply j)).card) :
    ∃ f : Equiv.Perm ι, ∀ i, request i <+: supply (f i) := by
…