theorem
proved
hierarchy_forced_gives_phi
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.HierarchyForcing on GitHub at line 141.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
formal source
138 field_simp; linarith }
139
140/-- The forced hierarchy yields σ = φ. -/
141theorem hierarchy_forced_gives_phi
142 (M : NontrivialMultilevelComposition)
143 (no_free_scale : ∀ j k,
144 M.levels (j + 1) / M.levels j = M.levels (k + 1) / M.levels k)
145 (ratio_gt_one : 1 < M.levels 1 / M.levels 0)
146 (additive : M.levels 2 = M.levels 1 + M.levels 0) :
147 (hierarchy_forced M no_free_scale ratio_gt_one).ratio = PhiForcing.φ :=
148 hierarchy_emergence_forces_phi
149 (hierarchy_forced M no_free_scale ratio_gt_one)
150 additive
151
152end HierarchyForcing
153end Foundation
154end IndisputableMonolith