uniform_scaling_forced

formal source

  86which derives uniform ratios from the `RealizedHierarchy.ratio_self_similar`
  87field, with `no_continuous_moduli` as backup
  88(`HierarchyRealization.no_moduli_forces_uniform_ratios`). -/
  89theorem uniform_scaling_forced
  90    (M : NontrivialMultilevelComposition)
  91    (no_free_scale : ∀ j k,
  92      M.levels (j + 1) / M.levels j = M.levels (k + 1) / M.levels k)
  93    (ratio_gt_one : 1 < M.levels 1 / M.levels 0) :
  94    ∃ σ : ℝ, 1 < σ ∧ ∀ k, M.levels (k + 1) = σ * M.levels k := by
  95  use M.levels 1 / M.levels 0
  96  refine ⟨ratio_gt_one, fun k => ?_⟩
  97  have hk := M.levels_pos k
  98  have h0 := M.levels_pos 0
  99  have hratio := no_free_scale k 0
 100  rw [div_eq_div_iff (ne_of_gt hk) (ne_of_gt h0)] at hratio
 101  have : M.levels (k + 1) = M.levels 1 / M.levels 0 * M.levels k := by
 102    field_simp; linarith
 103  exact this
 104
 105/-- **Theorem (Phase 3)**: Among recurrence coefficients (a, b) with
 106a ≥ 1 and b ≥ 1, the pair (1, 1) uniquely minimizes max(a, b).
 107No axiom needed — this is pure arithmetic. -/
 108theorem additive_composition_is_minimal (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b) :
 109    max a b = 1 → a = 1 ∧ b = 1 := by
 110  intro h
 111  constructor
 112  · exact Nat.le_antisymm (by omega) ha
 113  · exact Nat.le_antisymm (by omega) hb
 114
 115/-- The pair (1,1) achieves max = 1. -/
 116theorem min_max_achieved : max 1 1 = 1 := by simp
 117
 118/-- Any other pair has max ≥ 2. -/
 119theorem other_pairs_larger (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b)