 142
 143This internalizes the `sensitivity` bridge: the perturbation family
 144`ScalePerturbed` lifts to carrier states via the observable `r`. -/
 145theorem nonuniform_ratios_yield_moduli
 146    (F : ClosedObservableFramework)
 147    (levels : ℕ → ℝ)
 148    (levels_pos : ∀ k, 0 < levels k)
 149    (_levels_from_carrier : ∀ k, ∃ s : F.S, F.r s = levels k)
 150    (carrier_lifts_perturbations :
 151      ∀ (_k : ℕ) (v : ℝ), 0 < v →
 152        ∃ s : F.S, F.r s = v) :
 153    (∃ j k, levels (j + 1) / levels j ≠ levels (k + 1) / levels k) →
 154    ∃ (embed : ℝ → F.S), Function.Injective embed := by
 155  intro ⟨j, _, _⟩
 156  have h_pos : 0 < levels (j + 1) := levels_pos (j + 1)
 157  have h_ne : levels (j + 1) ≠ 0 := ne_of_gt h_pos
 158  choose lift h_lift using fun (t : ℝ) =>
 159    carrier_lifts_perturbations (j + 1) (levels (j + 1) * Real.exp t)
 160      (mul_pos h_pos (Real.exp_pos t))
 161  refine ⟨lift, fun t₁ t₂ h_eq => ?_⟩
 162  have h1 : F.r (lift t₁) = levels (j + 1) * Real.exp t₁ := h_lift t₁
 163  have h2 : F.r (lift t₂) = levels (j + 1) * Real.exp t₂ := h_lift t₂
 164  have h3 : F.r (lift t₁) = F.r (lift t₂) := by rw [h_eq]
 165  rw [h1, h2] at h3
 166  exact Real.exp_injective (mul_left_cancel₀ h_ne h3)
 167
 168/-- **Corollary**: In a `ClosedObservableFramework` where the observable
 169can realize all positive values, non-uniform ratios are impossible. -/
 170theorem no_moduli_forces_uniform_ratios
 171    (F : ClosedObservableFramework)
 172    (levels : ℕ → ℝ)
 173    (levels_pos : ∀ k, 0 < levels k)
 174    (_levels_from_carrier : ∀ k, ∃ s : F.S, F.r s = levels k)
 175    (carrier_lifts_perturbations :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.