theorem
proved
closedFramework_does_not_force_realizedHierarchy_fields
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 115.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
T -
ClosedObservableFramework -
baseState -
boolFramework -
orbit_not_additive_posting -
orbit_not_ratio_self_similar -
T -
F -
F -
F -
S
used by
formal source
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