NontrivialMultilevelComposition

formal source

  75/-! ## Uniform Scaling Forced -/
  76
  77/-- Multilevel composition with at least three levels. -/
  78structure NontrivialMultilevelComposition where
  79  levels : ℕ → ℝ
  80  levels_pos : ∀ k, 0 < levels k
  81  at_least_three : 0 < levels 0 ∧ 0 < levels 1 ∧ 0 < levels 2
  82
  83/-- **Theorem**: No free scale parameters forces uniform adjacent ratios.
  84
  85The canonical derivation now uses `HierarchyRealization.realized_uniform_ratios`
  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) :