scale_perturbed_low

formal source

  54  · exact mul_pos (h_pos k) (Real.exp_pos t)
  55
  56/-- The perturbation fixes all levels at or below position `j`. -/
  57theorem scale_perturbed_low (levels : ℕ → ℝ) (j : ℕ) (t : ℝ)
  58    (k : ℕ) (hk : k ≤ j) :
  59    ScalePerturbed levels j t k = levels k := by
  60  unfold ScalePerturbed; rw [if_pos hk]
  61
  62/-- Different perturbation parameters give different level sequences.
  63The key step: at position `j + 1` the values are `levels(j+1) · exp(t)`,
  64and `exp` is injective. -/
  65theorem scale_perturbed_family_injective (levels : ℕ → ℝ) (j : ℕ)
  66    (h_pos : 0 < levels (j + 1)) :
  67    Function.Injective (ScalePerturbed levels j) := by
  68  intro t₁ t₂ h
  69  have h_eval := congr_fun h (j + 1)
  70  unfold ScalePerturbed at h_eval
  71  rw [if_neg (by omega : ¬(j + 1 ≤ j)), if_neg (by omega : ¬(j + 1 ≤ j))] at h_eval
  72  have h_ne : levels (j + 1) ≠ 0 := ne_of_gt h_pos
  73  exact Real.exp_injective (mul_left_cancel₀ h_ne h_eval)
  74
  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