theorem
proved
orbit_not_additive_posting
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.HierarchyRealizationObstruction on GitHub at line 93.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
107`additive_posting`. -/
108theorem closedFramework_does_not_force_additive_posting :
109 ∃ (F : ClosedObservableFramework) (base : F.S),
110 ¬ (F.r (F.T^[2] base) = F.r (F.T^[1] base) + F.r base) := by
111 exact ⟨boolFramework, baseState, orbit_not_additive_posting⟩
112
113/-- Combined obstruction theorem: the earlier primitive layer admits
114models where both target fields fail. -/
115theorem closedFramework_does_not_force_realizedHierarchy_fields :
116 ∃ (F : ClosedObservableFramework) (base : F.S),
117 (¬ (∀ k,
118 F.r (F.T^[k + 2] base) / F.r (F.T^[k + 1] base) =
119 F.r (F.T^[k + 1] base) / F.r (F.T^[k] base))) ∧
120 (¬ (F.r (F.T^[2] base) = F.r (F.T^[1] base) + F.r base)) := by
121 exact ⟨boolFramework, baseState, orbit_not_ratio_self_similar, orbit_not_additive_posting⟩
122
123end HierarchyRealizationObstruction