theorem
proved
orbitLevels_one
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.HierarchyRealizationObstruction on GitHub at line 76.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
73@[simp] theorem orbitLevels_zero : orbitLevels 0 = 1 := by
74 simp [orbitLevels, boolFramework, baseState]
75
76@[simp] theorem orbitLevels_one : orbitLevels 1 = 2 := by
77 simp [orbitLevels, boolFramework, baseState]
78
79@[simp] theorem orbitLevels_two : orbitLevels 2 = 1 := by
80 simp [orbitLevels, boolFramework, baseState]
81
82/-- The counterexample orbit does not satisfy ratio self-similarity. -/
83theorem orbit_not_ratio_self_similar :
84 ¬ (∀ k,
85 orbitLevels (k + 2) / orbitLevels (k + 1) =
86 orbitLevels (k + 1) / orbitLevels k) := by
87 intro h
88 have h0 := h 0
89 simp [orbitLevels, boolFramework, baseState] at h0
90 norm_num at h0
91
92/-- The counterexample orbit does not satisfy additive posting. -/
93theorem orbit_not_additive_posting :
94 ¬ (orbitLevels 2 = orbitLevels 1 + orbitLevels 0) := by
95 simp [orbitLevels, boolFramework, baseState]
96
97/-- Therefore `ClosedObservableFramework` alone cannot force
98`ratio_self_similar`. -/
99theorem closedFramework_does_not_force_ratio_self_similar :
100 ∃ (F : ClosedObservableFramework) (base : F.S),
101 ¬ (∀ k,
102 F.r (F.T^[k + 2] base) / F.r (F.T^[k + 1] base) =
103 F.r (F.T^[k + 1] base) / F.r (F.T^[k] base)) := by
104 exact ⟨boolFramework, baseState, orbit_not_ratio_self_similar⟩
105
106/-- Therefore `ClosedObservableFramework` alone cannot force