pith. machine review for the scientific record. sign in
theorem proved term proof

closedFramework_does_not_force_realizedHierarchy_fields

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 121  exact ⟨boolFramework, baseState, orbit_not_ratio_self_similar, orbit_not_additive_posting⟩
 122
 123end HierarchyRealizationObstruction
 124end Foundation
 125end IndisputableMonolith

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.