hierarchy_forced

formal source

 120    (h : ¬(a = 1 ∧ b = 1)) : 2 ≤ max a b := by omega
 121
 122/-- Construct the uniform scale ladder from forced data. -/
 123noncomputable def hierarchy_forced
 124    (M : NontrivialMultilevelComposition)
 125    (no_free_scale : ∀ j k,
 126      M.levels (j + 1) / M.levels j = M.levels (k + 1) / M.levels k)
 127    (ratio_gt_one : 1 < M.levels 1 / M.levels 0) :
 128    UniformScaleLadder :=
 129  { levels := M.levels
 130    levels_pos := M.levels_pos
 131    ratio := M.levels 1 / M.levels 0
 132    ratio_gt_one := ratio_gt_one
 133    uniform_scaling := fun k => by
 134      have hk := M.levels_pos k
 135      have h0 := M.levels_pos 0
 136      have hratio := no_free_scale k 0
 137      rw [div_eq_div_iff (ne_of_gt hk) (ne_of_gt h0)] at hratio
 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