parameter_free_ratios_are_unity
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.