OAI/Dynamics/SmoothObstruction/WordHierarchy.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SmoothObstruction.WordHierarchy.S line 12
2. abbrev OAI.SmoothObstruction.WordHierarchy.A line 13
3. abbrev OAI.SmoothObstruction.WordHierarchy.size line 14
4. abbrev OAI.SmoothObstruction.WordHierarchy.groupLength line 15
5. abbrev OAI.SmoothObstruction.WordHierarchy.Config line 16
6. abbrev OAI.SmoothObstruction.WordHierarchy.Labels line 17
7. abbrev OAI.SmoothObstruction.WordHierarchy.goodDim line 18
8. abbrev OAI.SmoothObstruction.WordHierarchy.raw line 21
9. structure OAI.SmoothObstruction.WordHierarchy.Family line 25

   Source documentation

   The chosen family stores the actual conditioning event and its mass, not merely the existence of enough labels.

   structure Family (i : ℕ) where
   …

10. def OAI.SmoothObstruction.WordHierarchy.chooseFamily line 40
11. def OAI.SmoothObstruction.WordHierarchy.Family.word line 49
12. lemma OAI.SmoothObstruction.WordHierarchy.Family.word_injective line 52
13. def OAI.SmoothObstruction.WordHierarchy.stage line 55
14. lemma OAI.SmoothObstruction.WordHierarchy.stage_approximates line 68

    Source documentation

    Every stored successor word actually obeys the W4 event for every nonwrapping lower-window offset.

    lemma stage_approximates (i : ℕ) (a : A (i+2)) (t : Offsets (S i)) :
        tvFromUniformObservable (fun b => window (S i) t ((stage i).word b))
          (WordFlatten.flattenEquiv.symm ((stage (i+1)).word a)) ≤ 1/10000 := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.A, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.stage, OAI.SmoothObstruction.WordHierarchy.word

15. def OAI.SmoothObstruction.WordConcatenation.pack line 81
16. lemma OAI.SmoothObstruction.WordConcatenation.pack_val line 84
17. def OAI.SmoothObstruction.WordConcatenation.concat line 88
18. lemma OAI.SmoothObstruction.WordConcatenation.concat_pack line 91
19. lemma OAI.SmoothObstruction.WordConcatenation.concat_injective line 94
20. lemma OAI.SmoothObstruction.WordConcatenation.slice_is_constituent line 105

    Source documentation

    Every aligned lower word in a concatenation is an actual constituent, including near the last endpoint.

    lemma slice_is_constituent (hm : 0 < m) (u : B → Fin m → A) (w : Fin N → B)
        (a : ℕ) (ha : m ∣ a) (hlen : a+m ≤ m*N) :
        ∃ b : Fin N, (fun r : Fin m => concat u w
          ⟨a+r.val,lt_of_lt_of_le (Nat.add_lt_add_left r.isLt a) hlen⟩) = u (w b) := by
    …

    Mentions: OAI.SmoothObstruction.WordConcatenation.concat

21. def OAI.SmoothObstruction.WordHierarchy.children line 127
22. lemma OAI.SmoothObstruction.WordHierarchy.children_injective line 130
23. def OAI.SmoothObstruction.WordHierarchy.word line 140

    Source documentation

    Source words have exactly the recursively prescribed lengths, over the fixed initial alphabet. Reindexing is the fixed arbitrary labeling allowed by the manuscript, not a new conditioning at any level.

    noncomputable def word : (i : ℕ) → A i → Fin (length 40000 i) → A 0
      | 0,a,_ => a
      | i+1,a,j => concat (word i) (children i a) j

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

24. lemma OAI.SmoothObstruction.WordHierarchy.word_injective line 144
25. def OAI.SmoothObstruction.WordHierarchy.words line 152
26. lemma OAI.SmoothObstruction.WordHierarchy.alphabet_nonempty line 154
27. lemma OAI.SmoothObstruction.WordHierarchy.words_nonempty line 164
28. lemma OAI.SmoothObstruction.WordHierarchy.words_card line 168
29. def OAI.SmoothObstruction.PhaseDynamics.SubwordClosed line 180

    Source documentation

    The exact concatenation property of legal source words, expressed at all aligned lower-word positions.

    def SubwordClosed : Prop :=
    …

30. lemma OAI.SmoothObstruction.PhaseDynamics.legal_of_succ line 187
31. def OAI.SmoothObstruction.PhaseDynamics.repeatWord line 216

    Source documentation

    Periodic repetition is used solely as a finite-admissibility witness; it is not the ergodic measure ultimately selected.

    def repeatWord (n : ℕ) (w : Fin (m n) → A) : Space A m :=
    …

    Mentions: OAI.SmoothObstruction.PhaseDynamics.Space

32. lemma OAI.SmoothObstruction.PhaseDynamics.repeatWord_legal line 220
33. theorem OAI.SmoothObstruction.PhaseDynamics.finite_configs line 235

    Source documentation

    Every nonempty concatenated word hierarchy has all the finite-level configurations required by the compact phase construction.

    theorem finite_configs (hW : SubwordClosed m W) (hne : ∀ i, (W i).Nonempty) :
        ∀ n, ∃ x : Space A m, ∀ i ≤ n, Compatible m hm x i ∧ Legal m W x i := by
    …

    Mentions: OAI.SmoothObstruction.PhaseDynamics.SubwordClosed, OAI.SmoothObstruction.PhaseDynamics.Space, OAI.SmoothObstruction.PhaseDynamics.Compatible, OAI.SmoothObstruction.PhaseDynamics.Legal

34. instance OAI.SmoothObstruction.WordHierarchy.lengthNeZero line 250
35. lemma OAI.SmoothObstruction.WordHierarchy.words_subwordClosed line 253
36. abbrev OAI.SmoothObstruction.WordHierarchy.Extension line 262

    Source documentation

    The compact source extension is nonvacuous for the actual balanced, shift-separated, symplectically constrained recursively selected hierarchy.

    noncomputable abbrev Extension := PhaseDynamics.extension (length 40000) (length_dvd 40000) words

    Mentions: OAI.SmoothObstruction.PhaseDynamics.extension, OAI.SmoothObstruction.WordHierarchy.words

37. instance OAI.SmoothObstruction.WordHierarchy.initialNonempty line 264
38. theorem OAI.SmoothObstruction.WordHierarchy.actual_system line 268

    Source documentation

    Here the finite-admissibility producers are discharged by the actual words. The remaining main obstruction is not part of this theorem.

    theorem actual_system : ∃ μ : ProbabilityMeasure Extension,
        StandardNonatomic (μ : Measure Extension) ∧
        Ergodic (PhaseDynamics.extensionShift (length 40000) (length_dvd 40000) words)
          (μ : Measure Extension) ∧
        FiniteKSEntropy (μ : Measure Extension)
          (PhaseDynamics.extensionShift (length 40000) (length_dvd 40000) words) := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.StandardNonatomic, OAI.SmoothObstruction.PhaseDynamics.extensionShift, OAI.SmoothObstruction.WordHierarchy.words, OAI.SmoothObstruction.FiniteKSEntropy

39. def OAI.SmoothObstruction.PhaseDynamics.containingWord line 290

    Source documentation

    The actual symbol word containing the origin, not an independently assigned label. Its starting time is minus the finite phase representative.

    def containingWord (x : Space A m) (i : ℕ) : Fin (m i) → A :=
    …

    Mentions: OAI.SmoothObstruction.PhaseDynamics.Space

40. lemma OAI.SmoothObstruction.PhaseDynamics.measurable_containingWord line 294
41. lemma OAI.SmoothObstruction.PhaseDynamics.iterate_symbol line 305
42. lemma OAI.SmoothObstruction.PhaseDynamics.shift_iterate_phase line 317
43. lemma OAI.SmoothObstruction.PhaseDynamics.containingWord_tower line 323
44. theorem OAI.SmoothObstruction.PhaseDynamics.parent_phase_mass line 336

    Source documentation

    Every parent-word event has exactly the same unnormalized mass at each phase. This is the invariance argument in source (parent-slot-law), before normalizing either restriction. No uniform-parent assumption occurs.

    theorem parent_phase_mass (μ : Measure (Space A m))
        (hT : MeasurePreserving (shift A m) μ μ) (i : ℕ) (v : Fin (m i) → A)
        (j : ℕ) (hj : j < m i) :
        μ {x | x.2 i=(j : ZMod (m i)) ∧ containingWord m x i=v} =
          μ {x | x.2 i=0 ∧ containingWord m x i=v} := by
    …

    Mentions: OAI.SmoothObstruction.PhaseDynamics.Space, OAI.SmoothObstruction.PhaseDynamics.shift, OAI.SmoothObstruction.PhaseDynamics.containingWord

45. lemma OAI.SmoothObstruction.PhaseDynamics.parent_phase_mass_zmod line 359
46. lemma OAI.SmoothObstruction.PhaseDynamics.sum_phase_parent line 367
47. theorem OAI.SmoothObstruction.PhaseDynamics.parent_slot_independent line 387

    Source documentation

    Parent and containing slot are independent under the full stationary law, although the parent distribution can be wholly nonuniform.

    theorem parent_slot_independent (μ : Measure (Space A m)) [IsFiniteMeasure μ]
        (hT : MeasurePreserving (shift A m) μ μ) (i : ℕ) (v : Fin (m i) → A)
        (j : ZMod (m i)) :
        (m i : ℝ)*μ.real {x | x.2 i=j ∧ containingWord m x i=v} =
          μ.real {x | containingWord m x i=v} := by
    …

    Mentions: OAI.SmoothObstruction.PhaseDynamics.Space, OAI.SmoothObstruction.PhaseDynamics.shift, OAI.SmoothObstruction.PhaseDynamics.containingWord

48. abbrev OAI.SmoothObstruction.WordHierarchy.T line 404
49. lemma OAI.SmoothObstruction.WordHierarchy.containingWord_legal line 407
50. def OAI.SmoothObstruction.WordHierarchy.label line 414

    Source documentation

    The actual legal word containing the origin, read as its unique selected level label. This is a function of the symbolic configuration, not added data.

    noncomputable def label (i : ℕ) (x : Extension) : A i :=
    …

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

51. lemma OAI.SmoothObstruction.WordHierarchy.word_label line 417
52. lemma OAI.SmoothObstruction.WordHierarchy.label_eq_iff line 421
53. lemma OAI.SmoothObstruction.WordHierarchy.measurable_label line 425
54. lemma OAI.SmoothObstruction.WordHierarchy.stationary_ambient line 436
55. theorem OAI.SmoothObstruction.WordHierarchy.label_phase_independent line 452

    Source documentation

    Actual selected parent labels are independent of the fine phase under EVERY invariant finite measure on the extension. The parent law is arbitrary.

    theorem label_phase_independent (μ : Measure Extension) [IsFiniteMeasure μ]
        (hT : MeasurePreserving T μ μ) (i : ℕ) (a : A i) (j : ZMod (length 40000 i)) :
        (length 40000 i : ℝ)*μ.real {x | x.val.2 i=j ∧ label i x=a} =
          μ.real {x | label i x=a} := by
    …

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

56. lemma OAI.SmoothObstruction.WordHierarchy.phase_mod line 473

    Source documentation

    Compatibility determines the child offset by the parent residue.

    lemma phase_mod (i : ℕ) (x : Extension) :
        (x.val.2 (i+1)).val % length 40000 i=(x.val.2 i).val := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension

57. def OAI.SmoothObstruction.WordHierarchy.slot line 483

    Source documentation

    The slot of the containing selected child inside the containing parent.

    noncomputable def slot (i : ℕ) (x : Extension) : Fin (N (S i)) :=
    …

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

58. lemma OAI.SmoothObstruction.WordHierarchy.phase_decompose line 488
59. theorem OAI.SmoothObstruction.WordHierarchy.label_child line 495

    Source documentation

    The observed child label is exactly the selected concatenation entry indexed by the actual parent phase, with no exceptional configurations.

    theorem label_child (i : ℕ) (x : Extension) :
        label i x=children i (label (i+1) x) (slot i x) := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.label, OAI.SmoothObstruction.WordHierarchy.children, OAI.SmoothObstruction.WordHierarchy.slot

60. lemma OAI.SmoothObstruction.Alignment.sum_fibers line 522

    Source documentation

    Partition an arbitrary event by a finite measurable observation.

    lemma sum_fibers (μ : Measure X) [IsFiniteMeasure μ] (E : Set X)
        {f : X → Y} (hf : Measurable f) :
        (∑ a : Y,μ.real {x | x∈E ∧ f x=a})=μ.real E := by
    …

61. def OAI.SmoothObstruction.Alignment.align line 539
62. lemma OAI.SmoothObstruction.Alignment.iterate_phase line 542
63. lemma OAI.SmoothObstruction.Alignment.measurable_align line 548
64. lemma OAI.SmoothObstruction.Alignment.align_phase line 554
65. lemma OAI.SmoothObstruction.Alignment.phase_piece line 559

    Source documentation

    Each fixed phase piece maps to exactly the same boundary event; this is an unnormalized identity using invariance, not a uniform-word assumption.

    lemma phase_piece (μ : Measure X) (hT : MeasurePreserving T μ μ)
        (ha : Measurable a) (hevolve : ∀ x,a (T x)=a x+1)
        (E : Set X) (hE : MeasurableSet E) (j : ZMod m) :
        μ {x | x∈(align T a) ⁻¹' E ∧ a x=j}=μ (E∩{x | a x=0}) := by
    …

    Mentions: OAI.SmoothObstruction.Alignment.align

66. theorem OAI.SmoothObstruction.Alignment.align_real line 578

    Source documentation

    Exact forward-alignment law for every measurable event.

    theorem align_real (μ : Measure X) [IsFiniteMeasure μ]
        (hT : MeasurePreserving T μ μ) (ha : Measurable a)
        (hevolve : ∀ x,a (T x)=a x+1) (E : Set X) (hE : MeasurableSet E) :
        μ.real ((align T a) ⁻¹' E) = (m:ℝ)*μ.real (E∩{x | a x=0}) := by
    …

    Mentions: OAI.SmoothObstruction.Alignment.align

67. def OAI.SmoothObstruction.Alignment.boundaryMeasure line 586
68. lemma OAI.SmoothObstruction.Alignment.boundary_real line 590
69. theorem OAI.SmoothObstruction.Alignment.align_map line 598

    Source documentation

    The image of the original stationary law under first-boundary advance is the normalized boundary restriction itself.

    theorem align_map (μ : Measure X) [IsFiniteMeasure μ]
        (hT : MeasurePreserving T μ μ) (ha : Measurable a)
        (hevolve : ∀ x,a (T x)=a x+1) :
        μ.map (align T a)=boundaryMeasure a μ := by
    …

    Mentions: OAI.SmoothObstruction.Alignment.align, OAI.SmoothObstruction.Alignment.boundaryMeasure

70. theorem OAI.SmoothObstruction.Alignment.boundary_probability line 613

    Source documentation

    Its normalization is proved, including the literal source factor m.

    theorem boundary_probability (μ : Measure X) [IsProbabilityMeasure μ]
        (hT : MeasurePreserving T μ μ) (ha : Measurable a)
        (hevolve : ∀ x,a (T x)=a x+1) : IsProbabilityMeasure (boundaryMeasure a μ) := by
    …

    Mentions: OAI.SmoothObstruction.Alignment.boundaryMeasure

71. abbrev OAI.SmoothObstruction.WordHierarchy.phase line 626
72. lemma OAI.SmoothObstruction.WordHierarchy.measurable_phase line 627
73. lemma OAI.SmoothObstruction.WordHierarchy.iterate_coe line 630
74. lemma OAI.SmoothObstruction.WordHierarchy.phase_iterate line 639
75. def OAI.SmoothObstruction.WordHierarchy.boundary line 643
76. lemma OAI.SmoothObstruction.WordHierarchy.boundary_isProbability line 646
77. def OAI.SmoothObstruction.WordHierarchy.advance line 650
78. theorem OAI.SmoothObstruction.WordHierarchy.advance_map line 654

    Source documentation

    Literal forward-to-first-boundary law; µ_i is the source's factor-m_i normalized restriction, not a newly chosen distribution.

    theorem advance_map (μ : Measure Extension) [IsFiniteMeasure μ]
        (hT : MeasurePreserving T μ μ) (i : ℕ) : μ.map (advance i)=boundary μ i :=
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.advance, OAI.SmoothObstruction.WordHierarchy.boundary

79. lemma OAI.SmoothObstruction.WordHierarchy.phase_mod_two line 658
80. lemma OAI.SmoothObstruction.WordHierarchy.length_two line 662
81. def OAI.SmoothObstruction.WordHierarchy.parentSlot line 667
82. lemma OAI.SmoothObstruction.WordHierarchy.measurable_parentSlot line 672
83. lemma OAI.SmoothObstruction.WordHierarchy.parentSlot_decompose line 680
84. lemma OAI.SmoothObstruction.WordHierarchy.parentSlot_site_lt line 685
85. lemma OAI.SmoothObstruction.WordHierarchy.parentSlot_site line 690
86. theorem OAI.SmoothObstruction.WordHierarchy.boundary_parentSlot_mass line 710

    Source documentation

    Every genuine parent slot has the same mass with a fixed parent label. The right-hand side is the arbitrary stationary parent law, not uniform.

    theorem boundary_parentSlot_mass (μ : Measure Extension) [IsFiniteMeasure μ]
        (hT : MeasurePreserving T μ μ) (i : ℕ) (v : A (i+2))
        (j : Fin (N (S i)*N (S (i+1)))) :
        (N (S i)*N (S (i+1)) : ℕ)*(boundary μ i).real {x | parentSlot i x=j ∧ label (i+2) x=v} =
          μ.real {x | label (i+2) x=v} := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.A, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.boundary, OAI.SmoothObstruction.WordHierarchy.parentSlot, OAI.SmoothObstruction.WordHierarchy.label

87. lemma OAI.SmoothObstruction.WordHierarchy.phase_val_nonwrap line 737
88. lemma OAI.SmoothObstruction.WordHierarchy.label_nonwrap line 743
89. lemma OAI.SmoothObstruction.WordHierarchy.length_step line 756
90. lemma OAI.SmoothObstruction.WordHierarchy.slot_pair line 758
91. lemma OAI.SmoothObstruction.WordHierarchy.label_advance_child line 769

    Source documentation

    Inside a parent, advancement by a child-word length advances its actual slot by one. Alignment is the genuine phase-zero event.

    lemma label_advance_child (i r : ℕ) (x : Extension) (hx : phase i x=0)
        (hr : (slot i x).val+r < N (S i)) :
        label i ((T^[r*length 40000 i]) x) =
          children i (label (i+1) x) ⟨(slot i x).val+r,hr⟩ := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.phase, OAI.SmoothObstruction.WordHierarchy.slot, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.label, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.children

92. def OAI.SmoothObstruction.WordHierarchy.labelList line 787

    Source documentation

    The exact observed finite word-label list on the normalized boundary.

    noncomputable def labelList (i r : ℕ) (x : Extension) : Fin r → A i :=
    …

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

93. lemma OAI.SmoothObstruction.WordHierarchy.measurable_T line 790
94. lemma OAI.SmoothObstruction.WordHierarchy.measurable_labelList line 798
95. theorem OAI.SmoothObstruction.WordHierarchy.labelList_inside line 804

    Source documentation

    Uniform finite-window sampling is an exact identification of the actual symbolic orbit, not a replacement process. No wrap occurs at admissible slots.

    theorem labelList_inside (i r : ℕ) (x : Extension) (hx : phase i x=0)
        (hr : (slot i x).val+r ≤ N (S i)) :
        labelList i r x = fun j : Fin r =>
          children i (children (i+1) (label (i+2) x) (slot (i+1) x))
            ⟨(slot i x).val+j.val,by have := j.isLt; omega⟩ := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.phase, OAI.SmoothObstruction.WordHierarchy.slot, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.labelList, OAI.SmoothObstruction.WordHierarchy.children, OAI.SmoothObstruction.WordHierarchy.label