theorem
proved
closedFramework_does_not_force_additive_posting
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 108.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
124end Foundation
125end IndisputableMonolith