`parameter_free_ratios_are_unity`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.NeutralSector
domain: Foundation
line: 67 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.NeutralSector on GitHub at line 67.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  64
  65/-- **Bridge B4 core (unconditional)**: parameter-free observable
  66ratios in a zero-parameter ledger are all equal to 1. -/
  67theorem parameter_free_ratios_are_unity
  68    {α : Type}
  69    (model : ObservableRatioModel α)
  70    (h_no_knob : ∀ Q : ℝ, Q ≠ 0 → ¬ sectorLabelIsFreeKnob model Q)
  71    (s : α) :
  72    model.ratio s = 1 :=
  73  neutral_ratio_eq_one model s (parameter_free_observables_are_neutral model h_no_knob s)
  74
  75end NeutralSector
  76end Foundation
  77end IndisputableMonolith

papers checked against this theorem

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