PhaseDynamics.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SmoothObstruction.PhaseDynamics.iterate_phase line 16
theorem OAI.SmoothObstruction.PhaseDynamics.no_periodic_points line 27
Source documentation
Uniform infinite cyclic factors rule out every periodic point. This uses only the exact phase evolution, not recognition or word frequencies.
```
theorem no_periodic_points (T : X → X) (m : ℕ → ℕ) (a : ∀ i, X → ZMod (m i))
    (ha : ∀ i x, a i (T x) = a i x + 1) (hm : ∀ n, ∃ i, n < m i) :
    ∀ x n, 0 < n → (T^[n]) x ≠ x := by
…
```

theorem OAI.SmoothObstruction.PhaseDynamics.noAtoms_of_phases line 42

Source documentation

The phase extension's nonatomicity: a positive singleton would return by Poincare recurrence, contradicting its arbitrarily large cyclic factors.

theorem noAtoms_of_phases (μ : Measure X) [IsFiniteMeasure μ] (T : X → X)
    (hT : MeasurePreserving T μ μ) (m : ℕ → ℕ) (a : ∀ i, X → ZMod (m i))
    (ha : ∀ i x, a i (T x) = a i x + 1) (hm : ∀ n, ∃ i, n < m i) : NullSingletonClass μ := by
…

abbrev OAI.SmoothObstruction.PhaseDynamics.Space line 56
def OAI.SmoothObstruction.PhaseDynamics.shift line 60
Source documentation
The source map: bilateral symbol shift and addition of one in every phase. Its inverse subtracts one, with no modulo-null restriction.
```
def shift : Space A m ≃ₜ Space A m where
…
```
Mentions: OAI.SmoothObstruction.PhaseDynamics.Space
lemma OAI.SmoothObstruction.PhaseDynamics.shift_symbol line 74
lemma OAI.SmoothObstruction.PhaseDynamics.shift_phase line 75
def OAI.SmoothObstruction.PhaseDynamics.wordAt line 85
Source documentation
Level-i symbols beginning at an integer time.
```
def wordAt (x : Space A m) (i : ℕ) (t : ℤ) : Fin (m i) → A :=
…
```
Mentions: OAI.SmoothObstruction.PhaseDynamics.Space
def OAI.SmoothObstruction.PhaseDynamics.Compatible line 89
Source documentation
Exact compatibility of phases through the canonical cyclic quotient.
```
def Compatible (x : Space A m) (i : ℕ) : Prop :=
…
```
Mentions: OAI.SmoothObstruction.PhaseDynamics.Space
def OAI.SmoothObstruction.PhaseDynamics.Legal line 94
Source documentation
Every level boundary carries a legal word; the sign convention records the index of the origin inside its word, exactly as in source section 6.
```
def Legal (x : Space A m) (i : ℕ) : Prop :=
…
```
Mentions: OAI.SmoothObstruction.PhaseDynamics.Space
def OAI.SmoothObstruction.PhaseDynamics.extension line 97
lemma OAI.SmoothObstruction.PhaseDynamics.continuous_wordAt line 101
lemma OAI.SmoothObstruction.PhaseDynamics.compatible_closed line 105
lemma OAI.SmoothObstruction.PhaseDynamics.legal_closed line 110
lemma OAI.SmoothObstruction.PhaseDynamics.extension_closed line 125
lemma OAI.SmoothObstruction.PhaseDynamics.compatible_shift_iff line 133
lemma OAI.SmoothObstruction.PhaseDynamics.legal_shift_iff line 138
lemma OAI.SmoothObstruction.PhaseDynamics.extension_shift_iff line 163
lemma OAI.SmoothObstruction.PhaseDynamics.extension_shift_symm line 168
def OAI.SmoothObstruction.PhaseDynamics.extensionShift line 174
Source documentation
Restriction to the genuine closed phase extension, in both directions.
```
def extensionShift : extension m hm W ≃ₜ extension m hm W where
…
```
Mentions: OAI.SmoothObstruction.PhaseDynamics.extension
theorem OAI.SmoothObstruction.PhaseDynamics.extension_nonempty line 185
Source documentation
Compactness needs only finite-level admissible configurations. The actual word hierarchy supplies these by periodically repeating a word at the largest requested level; no invariant measure or frequency hypothesis enters.
```
theorem extension_nonempty [CompactSpace A] [∀ i, NeZero (m i)]
    (hfinite : ∀ n, ∃ x : Space A m, ∀ i ≤ n, Compatible m hm x i ∧ Legal m W x i) :
    (extension m hm W).Nonempty := by
…
```
Mentions: OAI.SmoothObstruction.PhaseDynamics.Space, OAI.SmoothObstruction.PhaseDynamics.Compatible, OAI.SmoothObstruction.PhaseDynamics.Legal, OAI.SmoothObstruction.PhaseDynamics.extension
lemma OAI.SmoothObstruction.PhaseDynamics.extension_coordinate_space line 218
theorem OAI.SmoothObstruction.PhaseDynamics.exists_system line 236
Source documentation
A genuine ergodic invertible standard nonatomic finite-KS system from any nonempty finite admissible word hierarchy with unbounded lengths. This is the measure-theoretic construction, not its graph obstruction.
```
theorem exists_system
    (hunbounded : ∀ n, ∃ i, n < m i)
    (hfinite : ∀ n, ∃ x : Space A m, ∀ i ≤ n, Compatible m hm x i ∧ Legal m W x i) :
    ∃ μ : ProbabilityMeasure (extension m hm W),
      StandardNonatomic (μ : Measure (extension m hm W)) ∧
      Ergodic (extensionShift m hm W) (μ : Measure (extension m hm W)) ∧
      FiniteKSEntropy (μ : Measure (extension m hm W)) (extensionShift m hm W) := by
…
```
Mentions: OAI.SmoothObstruction.PhaseDynamics.Space, OAI.SmoothObstruction.PhaseDynamics.Compatible, OAI.SmoothObstruction.PhaseDynamics.Legal, OAI.SmoothObstruction.PhaseDynamics.extension, OAI.SmoothObstruction.StandardNonatomic, OAI.SmoothObstruction.PhaseDynamics.extensionShift, OAI.SmoothObstruction.FiniteKSEntropy