parameter_free_ratios_are_unity
In zero-parameter ledgers every observable ratio equals unity. Researchers formalizing parameter-free models cite this as the unconditional core of Bridge B4. The proof is a one-line term that feeds the neutrality result directly into the zero-log-charge lemma.
claimLet $M$ be an observable ratio model on type $α$. If for every nonzero real $Q$ the value $Q$ is not realized as a log-charge in $M$, then for every state $s$ the ratio assigned by $M$ to $s$ equals 1.
background
The NeutralSector module shows that observable states in a zero-parameter ledger must carry zero conserved charge. An ObservableRatioModel on $α$ supplies a positive-real ratio function together with the identity log_charge(s) = log(ratio(s)). The upstream theorem parameter_free_observables_are_neutral proves that the no-free-knob hypothesis forces log_charge(s) = 0 for every s. The lemma neutral_ratio_eq_one then converts zero log-charge into ratio = 1.
proof idea
Term-mode one-liner: neutral_ratio_eq_one is applied to the model, the state s, and the neutrality fact obtained by instantiating parameter_free_observables_are_neutral on the given no-knob hypothesis.
why it matters in Recognition Science
This theorem supplies the unconditional statement of Bridge B4: parameter-free observable ratios equal 1. It completes the local argument that zero-parameter ledgers admit only neutral-sector observables. The result sits inside the forcing chain that fixes conserved quantities by self-similarity and zero external data.
scope and limits
- Does not apply when nonzero charges are admitted as free parameters.
- Does not constrain ratios outside the observable states of the model.
- Does not prove existence of the model, only the value of its ratios.
- Does not extend to states carrying nonzero conserved charge.
formal statement (Lean)
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 :=
proof body
Term-mode proof.
73 neutral_ratio_eq_one model s (parameter_free_observables_are_neutral model h_no_knob s)
74
75end NeutralSector
76end Foundation
77end IndisputableMonolith