OAI/Dynamics/SmoothObstruction/Recognition.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothObstruction.WordConcatenation.mismatches line 11
2. lemma OAI.SmoothObstruction.WordConcatenation.mismatches_nonneg line 15
3. lemma OAI.SmoothObstruction.WordConcatenation.mismatches_sum line 18
4. lemma OAI.SmoothObstruction.WordConcatenation.mismatches_comp line 23
5. lemma OAI.SmoothObstruction.WordConcatenation.mismatches_concat line 29
6. lemma OAI.SmoothObstruction.WordConcatenation.concat_distance line 35
7. def OAI.SmoothObstruction.WordConcatenation.joined line 49

   Source documentation

   Arbitrarily addressed letters of a two-word splice. Only addresses less than twice the word length are used by recognition.

   def joined [NeZero m] (u v : Fin m → A) (k : ℕ) : A :=
   …

8. def OAI.SmoothObstruction.WordConcatenation.splice line 53
9. lemma OAI.SmoothObstruction.WordConcatenation.splice_zero line 56
10. lemma OAI.SmoothObstruction.WordConcatenation.joined_low line 60
11. lemma OAI.SmoothObstruction.WordConcatenation.joined_high line 63
12. lemma OAI.SmoothObstruction.WordConcatenation.concat_at line 66
13. lemma OAI.SmoothObstruction.WordConcatenation.joined_concat line 81
14. lemma OAI.SmoothObstruction.WordConcatenation.splice_chunk line 97

    Source documentation

    Every lower-length portion of a shifted concatenation is precisely a splice of two successive lower words. This identity includes the join of the two larger words and repeated constituents.

    lemma splice_chunk [NeZero m] [NeZero N] (u : B → Fin m → A)
        (w v : Fin N → B) (t : Fin (m*N)) (b : Fin N) :
        (fun r => splice (concat u w) (concat u v) t (pack (b,r))) =
          splice (u (joined w v (t.val/m+b.val)))
            (u (joined w v (t.val/m+b.val+1)))
            ⟨t.val%m,Nat.mod_lt _ (NeZero.pos m)⟩ := by
    …

    Mentions: OAI.SmoothObstruction.WordConcatenation.splice, OAI.SmoothObstruction.WordConcatenation.concat, OAI.SmoothObstruction.WordConcatenation.pack, OAI.SmoothObstruction.WordConcatenation.joined

15. lemma OAI.SmoothObstruction.WordConcatenation.mismatches_blocks line 120
16. lemma OAI.SmoothObstruction.WordConcatenation.splice_aligned line 126
17. def OAI.SmoothObstruction.WordConcatenation.Recognizes line 140

    Source documentation

    A single recognition predicate handles both distinct words and every nontrivial splice, so the symbol-scale induction cannot drop an offset.

    def Recognizes [NeZero m] (u : B → Fin m → A) (δ : ℝ) : Prop :=
    …

18. theorem OAI.SmoothObstruction.WordConcatenation.recognition_step line 146
19. lemma OAI.SmoothObstruction.WordHierarchy.splice_first line 194
20. lemma OAI.SmoothObstruction.WordHierarchy.count_complement line 201
21. lemma OAI.SmoothObstruction.WordHierarchy.stage_recognizes line 214
22. lemma OAI.SmoothObstruction.WordHierarchy.recognizes_reindex_length line 232
23. instance OAI.SmoothObstruction.WordHierarchy.recognitionNNeZero line 238
24. lemma OAI.SmoothObstruction.WordHierarchy.children_recognizes line 241
25. def OAI.SmoothObstruction.WordHierarchy.delta line 244
26. lemma OAI.SmoothObstruction.WordHierarchy.delta_zero line 246
27. lemma OAI.SmoothObstruction.WordHierarchy.delta_succ line 247
28. lemma OAI.SmoothObstruction.WordHierarchy.delta_nonneg line 249
29. lemma OAI.SmoothObstruction.WordHierarchy.epsilon_sum line 252
30. lemma OAI.SmoothObstruction.WordHierarchy.delta_lower line 257
31. instance OAI.SmoothObstruction.WordHierarchy.recognitionLengthNeZero line 270
32. theorem OAI.SmoothObstruction.WordHierarchy.word_recognizes line 275

    Source documentation

    Source recognition at every symbol offset for the actual chosen words, not only for the constituent-label lists.

    theorem word_recognizes (i : ℕ) : Recognizes (word i) (delta i) := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.word, OAI.SmoothObstruction.WordHierarchy.delta

33. theorem OAI.SmoothObstruction.WordHierarchy.uniform_recognition line 303

    Source documentation

    The uniform fixed-alphabet constant is at least 3/4, hence strictly positive independently of the level and the three source labels.

    theorem uniform_recognition (i : ℕ) : Recognizes (word i) (3/4) := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.word

34. def OAI.SmoothObstruction.RecognitionWindow.LegalAt line 316

    Source documentation

    A legal phase-marked bilateral sequence, with no restriction at window endpoints; adjacent words are allowed to be identical.

    def LegalAt (w : B → Fin m → A) (u : ℤ → A) (p : ZMod m) : Prop :=
    …

35. theorem OAI.SmoothObstruction.RecognitionWindow.window_splice line 322

    Source documentation

    Every arbitrary length-m window is a splice of the two actual adjacent legal words. This includes negative starts and windows beyond the observed half-name.

    theorem window_splice (w : B → Fin m → A) (u : ℤ → A)
        (p : ZMod m) (hu : LegalAt w u p) (t : ℤ) :
        ∃ a b, ∃ o : Fin m, (o.val : ZMod m)=p+(t : ZMod m) ∧
          (fun r : Fin m => u (t+r.val))=splice (w a) (w b) o := by
    …

    Mentions: OAI.SmoothObstruction.RecognitionWindow.LegalAt

36. lemma OAI.SmoothObstruction.RecognitionWindow.mismatches_symm line 361
37. lemma OAI.SmoothObstruction.RecognitionWindow.phase_block_cost line 368

    Source documentation

    Recognition forces a fixed cost on every aligned block whenever the other sequence has a different phase.

    lemma phase_block_cost (w : B → Fin m → A) {δ : ℝ} (hw : Recognizes w δ)
        (u v : ℤ → A) (p q : ZMod m) (hu : LegalAt w u p) (hv : LegalAt w v q)
        (hpq : p≠q) (t : ℤ) (ht : (t : ZMod m)=-p) :
        δ*m≤(mismatches (fun r : Fin m => u (t+r.val))
          (fun r : Fin m => v (t+r.val)) : ℝ) := by
    …

    Mentions: OAI.SmoothObstruction.RecognitionWindow.LegalAt

38. lemma OAI.SmoothObstruction.RecognitionWindow.mismatches_injection line 384
39. def OAI.SmoothObstruction.RecognitionWindow.blocksEmbedding line 395

    Source documentation

    The D-1 full blocks after first alignment are disjoint and remain in [0,D*m), including the case of a nonzero advance.

    def blocksEmbedding (D a : ℕ) (ha : a < m) : Fin (D-1) × Fin m ↪ Fin (D*m) where
    …

40. lemma OAI.SmoothObstruction.RecognitionWindow.complete_blocks_le line 422

    Source documentation

    The whole-window mismatch count dominates the sum of all complete aligned block counts. No stochastic independence is involved.

    lemma complete_blocks_le (D a : ℕ) (ha : a < m) (u v : ℤ → A) (t : ℤ) :
        (∑ j : Fin (D-1),mismatches
          (fun r : Fin m => u (t+(a+j.val*m+r.val : ℕ)))
          (fun r : Fin m => v (t+(a+j.val*m+r.val : ℕ))))≤
        mismatches (fun r : Fin (D*m) => u (t+r.val)) (fun r : Fin (D*m) => v (t+r.val)) := by
    …

41. theorem OAI.SmoothObstruction.RecognitionWindow.phase_recovery line 438

    Source documentation

    Small mismatch on one half-name recovers the ORIGINAL phase. It does not choose or shift entry indices after the geometric switch.

    theorem phase_recovery (w : B → Fin m → A) {δ : ℝ} (_hδ : 0<δ)
        (hw : Recognizes w δ) (u v : ℤ → A) (p q : ZMod m)
        (hu : LegalAt w u p) (hv : LegalAt w v q)
        (D : ℕ) (hD : 2≤D) (a : ℕ) (ha : a < m) (haP : (a : ZMod m)=-p)
        (hclose : (mismatches (fun r : Fin (D*m) => u r.val)
          (fun r : Fin (D*m) => v r.val) : ℝ)<δ*(D*m)/100) : p=q := by
    …

    Mentions: OAI.SmoothObstruction.RecognitionWindow.LegalAt

42. lemma OAI.SmoothObstruction.RecognitionWindow.distinct_word_cost line 472
43. theorem OAI.SmoothObstruction.RecognitionWindow.entry_recovery line 480

    Source documentation

    Once the original phases have been recovered, the original entry labels cannot disagree with the switched labels at many positions. No new alignment or reindexing of entries is permitted.

    theorem entry_recovery (w : B → Fin m → A) {δ : ℝ} (hδ : 0<δ)
        (hw : Recognizes w δ) (u v : ℤ → A) (D a : ℕ) (ha : a < m) (t : ℤ)
        (U V : Fin (D-1) → B)
        (hU : ∀ j r,u (t+(a+j.val*m+r.val:ℕ))=w (U j) r)
        (hV : ∀ j r,v (t+(a+j.val*m+r.val:ℕ))=w (V j) r)
        (hclose : (mismatches (fun r : Fin (D*m) => u (t+r.val))
          (fun r : Fin (D*m) => v (t+r.val)):ℝ)<δ*(D*m)/100) :
        (mismatches U V:ℝ)<D/100 := by
    …

44. theorem OAI.SmoothObstruction.RecognitionWindow.paired_graph_bound line 521

    Source documentation

    Pure entry pairing: two small label-error sets remove at most their sum from a graph window. In particular the source constants give the literal .96 passing bound in the unchanged index order.

    theorem paired_graph_bound {D : ℕ} (hD : 2≤D) (R : B → B → Prop)
        [DecidableRel R] (U V Z W : Fin (D-1) → B)
        (hgraph : ∀ j,R (Z j) (W j))
        (hU : (mismatches U Z:ℝ)<D/100) (hV : (mismatches V W:ℝ)<D/100) :
        (24/25:ℝ)≤(∑ j,if R (U j) (V j) then (1:ℝ) else 0)/(D-1) := by
    …

45. lemma OAI.SmoothObstruction.WordHierarchy.actual_legal line 550
46. lemma OAI.SmoothObstruction.WordHierarchy.actual_iterate_symbol line 556
47. lemma OAI.SmoothObstruction.WordHierarchy.advance_phase line 560
48. lemma OAI.SmoothObstruction.WordHierarchy.measurable_advance line 563
49. def OAI.SmoothObstruction.WordHierarchy.firstList line 568

    Source documentation

    Original ordered labels after the first true boundary, without changing its phase or introducing a new pairing.

    noncomputable def firstList (i D : ℕ) (x : Extension) : Fin (D-1) → A i :=
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.A

50. lemma OAI.SmoothObstruction.WordHierarchy.measurable_firstList line 571
51. lemma OAI.SmoothObstruction.WordHierarchy.firstList_word line 574
52. theorem OAI.SmoothObstruction.WordHierarchy.actual_recovery line 593

    Source documentation

    On the actual extension, source symbol agreement recovers both the true phase and all but D/100 of the original ordered labels.

    theorem actual_recovery (i D : ℕ) (hD : 2≤D) (x z : Extension)
        (hclose : (mismatches (fun r : Fin (D*length 40000 i) => x.val.1 r.val)
          (fun r : Fin (D*length 40000 i) => z.val.1 r.val):ℝ)<
            (3/4:ℝ)*(D*length 40000 i)/100) :
        phase i x=phase i z ∧ (mismatches (firstList i D x) (firstList i D z):ℝ)<D/100 := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.phase, OAI.SmoothObstruction.WordHierarchy.firstList

53. lemma OAI.SmoothObstruction.WordHierarchy.measurable_form_pair line 612
54. lemma OAI.SmoothObstruction.WordHierarchy.measurable_graphWindows_at line 616
55. lemma OAI.SmoothObstruction.WordHierarchy.measurable_graphWindows line 626
56. theorem OAI.SmoothObstruction.WordHierarchy.stationary_graph_probability line 635

    Source documentation

    Actual graph-event probability under the stationary law, obtained by pushing its first-boundary advance, never by assuming uniform parents.

    theorem stationary_graph_probability (μ : Measure Extension) [IsProbabilityMeasure μ]
        (hT : MeasurePreserving T μ μ) (i k : ℕ) (hk : k≤K (S i)/8) :
        1-((2*2^k-2:ℕ):ℝ)/H (S i)≤
          μ.real {x | graphWindows i k (advance i x)} := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.graphWindows, OAI.SmoothObstruction.WordHierarchy.advance