Records.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Superstring.Hierarchical.Threading.LayerId line 12
Source documentation
Stable IDs for every sorted primitive layer of the exact base threading.
```
abbrev LayerId (C : Threading V ι) :=
…
```
Mentions: OAI.Superstring.Hierarchical.Threading
def OAI.Superstring.Hierarchical.Threading.layerAt line 15
def OAI.Superstring.Hierarchical.Threading.occurrenceEquiv line 20
Source documentation
Reordering a phase and a stable layer ID does not alter the recorded words.
```
noncomputable def occurrenceEquiv (C : Threading V ι) (closed : SubstringClosed V)
    (s : List α) : Family.Occurrence (C.layerAt closed) s ≃ C.Recorded s where
…
```
Mentions: OAI.Superstring.Hierarchical.Threading, OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Family.Occurrence
theorem OAI.Superstring.Hierarchical.Layer.records_at_alignment line 38
Source documentation
Moving a recorded occurrence to any identical full-text alignment preserves its exact exit-end test. Primitivity, not just periodicity, is essential here.
```
theorem records_at_alignment (D : Layer V A p) (hp : Primitive A p)
    {s : List α} {r t : ℤ} (hr : D.Records s r)
    (halign : ∀ x, A (x + r) = A (x + t)) : D.Records s t := by
…
```
Mentions: OAI.Superstring.Hierarchical.Layer, OAI.Superstring.Hierarchical.Primitive
theorem OAI.Superstring.Hierarchical.Threading.group_eq_of_alignment line 58
Source documentation
Identical aligned infinite texts necessarily belong to the same primitive text group; no finite-word coincidence is substituted for this condition.
```
theorem group_eq_of_alignment (C : Threading V ι) (g h : C.Groups) (r t : ℤ)
    (halign : ∀ x, C.groupText h (x + r) = C.groupText g (x + t)) : h = g := by
…
```
Mentions: OAI.Superstring.Hierarchical.Threading
abbrev OAI.Superstring.Hierarchical.Threading.AlignedOccurrence line 68
instance OAI.Superstring.Hierarchical.Threading.(instance at line 73) line 73

def OAI.Superstring.Hierarchical.Threading.qualifyingLayer line 80

Source documentation

Forgetting the unique aligned residue retains a qualifying sorted layer.

noncomputable def qualifyingLayer (C : Threading V ι) (closed : SubstringClosed V)
    (g : C.Groups) (t : ℤ) (s : List α) (o : C.AlignedOccurrence closed g t s) :
    {j : Fin (Fintype.card (C.Aligned (C.groupText g))) //
      t + s.length ≤ C.sortedExit (C.groupText g) j t} := by
…

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

theorem OAI.Superstring.Hierarchical.Threading.qualifyingLayer_injective line 90
theorem OAI.Superstring.Hierarchical.Threading.aligned_card_le_qualifying line 112
def OAI.Superstring.Hierarchical.Processing.qualifying line 127
Source documentation
The occurrence count tested when choosing a layer.
```
def qualifying {m : ℕ} (z : Fin m → ℤ) (H : ℤ) (p k : ℕ) : Finset (Fin m) :=
…
```
theorem OAI.Superstring.Hierarchical.Processing.qualifying_bound line 130

theorem OAI.Superstring.Hierarchical.Processing.choose_k line 144

Source documentation

The first failed test exists by the number of still available upper layers; the sharp-band bound comes from the previous, successful, integer test.

theorem choose_k {m n : ℕ} (hn : 0 < n) (hnm : n ≤ m)
    (z : Fin m → ℤ) (hz : Monotone z) (H : ℤ) (p : ℕ)
    (hH : H ≤ z ⟨m - 1, by omega⟩)
    (hstop : (qualifying z H p n).card ≤ n) :
    ∃ (k : ℕ) (hk : 0 < k) (hkn : k ≤ n),
      (qualifying z H p k).card ≤ k ∧
      H - ((k - 1) * p : ℕ) ≤ z ⟨m - k, by omega⟩ := by
…

Mentions: OAI.Superstring.Hierarchical.Processing.qualifying

theorem OAI.Superstring.Hierarchical.Processing.wide_band line 171
theorem OAI.Superstring.Hierarchical.Layer.normalize_alignment line 209
theorem OAI.Superstring.Counts.Data.family_occurrence_count line 229
theorem OAI.Superstring.Counts.Data.blocking_layer_count line 238
Source documentation
Empty recorded words do not disturb this identity: every positive blocking coefficient has a strictly longer, hence nonempty, bracketing word.
```
theorem blocking_layer_count (D : Data α) (hD : D.WellFormed)
    (A : ℤ → α) (s : List α) :
    blocking D.vertices A s
      (fun r => Fintype.card (Family.Occurrence ((D.threading hD).layerAt hD.closed) r)) =
      blocking D.vertices A s D.count := by
…
```
Mentions: OAI.Superstring.Counts.Data, OAI.Superstring.Counts.blocking

theorem OAI.Superstring.Counts.Data.period_forces_matching line 252

Source documentation

The exact period rule plus the exact base-layer histogram forces a genuine matching record with a different aligned bi-infinite text.

theorem period_forces_matching (D : Data α) (hD : D.WellFormed)
    {A : ℤ → α} {w v : List α} {p k : ℕ}
    (hp : 0 < p) (hk : 0 < k) (hper : Function.Periodic A (p : ℤ))
    (hw : w ∈ D.vertices) (hwne : w ≠ []) (hv : v ∈ D.vertices)
    (hmv : Matches A v) (hmw : Matches A w)
    (hlen : w.length + k * p = v.length)
    (ov : Family.Occurrence ((D.threading hD).layerAt hD.closed) v)
    (halign : ∀ x : ℤ, (D.threading hD).groupText ov.1.1 (x + ov.2.val.val) = A x)
    (hfew : Nat.card {o : Family.Occurrence ((D.threading hD).layerAt hD.closed) w //
      ∀ x : ℤ, (D.threading hD).groupText o.1.1 (x + o.2.val.val) = A x} ≤ k) :
    ∃ o : Family.Occurrence ((D.threading hD).layerAt hD.closed) w,
      (¬ ∀ x : ℤ, (D.threading hD).groupText o.1.1 (x + o.2.val.val) = A x) ∧
…

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

theorem OAI.Superstring.Hierarchical.textWord_reindex line 293
Source documentation
Reindexing a text changes coordinates, never the represented graph word.
```
theorem textWord_reindex (A : ℤ → α) (c a b : ℤ) :
    textWord (fun x => A (x + c)) a b = textWord A (a + c) (b + c) := by
…
```
Mentions: OAI.Superstring.Hierarchical.textWord
structure OAI.Superstring.Hierarchical.Layer.Record line 309
theorem OAI.Superstring.Hierarchical.Layer.Record.start_le_stop line 321
theorem OAI.Superstring.Hierarchical.Layer.Record.word_eq line 326
theorem OAI.Superstring.Hierarchical.Layer.Record.word_mem line 330
theorem OAI.Superstring.Hierarchical.Layer.Record.touched line 333
theorem OAI.Superstring.Hierarchical.Layer.Record.length_lt line 338
theorem OAI.Superstring.Hierarchical.Layer.Record.same_period_length_lt line 346
theorem OAI.Superstring.Counts.Data.hard_case_record line 364