ObservableRatioModel

formal source

  26
  27/-- An observable ratio model on a type `α` assigns a positive real
  28ratio to each state and records the log-charge of that ratio. -/
  29structure ObservableRatioModel (α : Type) where
  30  ratio : α → ℝ
  31  ratio_pos : ∀ s, 0 < ratio s
  32  log_charge : α → ℝ
  33  log_charge_eq : ∀ s, log_charge s = Real.log (ratio s)
  34
  35/-- A sector label is a free parameter if it can take any real value. -/
  36def sectorLabelIsFreeKnob {α : Type} (model : ObservableRatioModel α)
  37    (Q : ℝ) : Prop :=
  38  ∃ s : α, model.log_charge s = Q
  39
  40/-- **Theorem (Parameter-free observables are neutral)**:
  41If every observable state must be specifiable without free parameters,
  42and specifying a nonzero log-charge requires a free real knob, then
  43all observable states have zero log-charge. -/
  44theorem parameter_free_observables_are_neutral
  45    {α : Type}
  46    (model : ObservableRatioModel α)
  47    (h_no_knob : ∀ Q : ℝ, Q ≠ 0 → ¬ sectorLabelIsFreeKnob model Q)
  48    (s : α) :
  49    model.log_charge s = 0 := by
  50  by_contra h
  51  exact h_no_knob (model.log_charge s) h ⟨s, rfl⟩
  52
  53/-- Neutral log-charge forces the ratio to equal 1. -/
  54theorem neutral_ratio_eq_one
  55    {α : Type}
  56    (model : ObservableRatioModel α)
  57    (s : α)
  58    (h_neutral : model.log_charge s = 0) :
  59    model.ratio s = 1 := by