sectorLabelIsFreeKnob

formal source

  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
  60  have hlog : Real.log (model.ratio s) = 0 := by
  61    rw [← model.log_charge_eq s]; exact h_neutral
  62  exact Real.log_injOn_pos (Set.mem_Ioi.mpr (model.ratio_pos s))
  63    (Set.mem_Ioi.mpr one_pos) (by rw [hlog, Real.log_one])
  64
  65/-- **Bridge B4 core (unconditional)**: parameter-free observable
  66ratios in a zero-parameter ledger are all equal to 1. -/