parameter_free_observables_are_neutral
plain-language theorem explainer
Zero-parameter observable ratio models force every state to have zero log-charge, since any nonzero value would require a free real parameter to specify. Researchers establishing neutrality in Recognition Science ledgers cite this to enforce the zero-parameter posture. The proof proceeds by contradiction, applying the no-knob hypothesis directly to the assumed nonzero charge via a witness state.
Claim. Let $M$ be an observable ratio model on type $α$, with positive ratio function and log-charge satisfying log-charge$(s) = $log(ratio$(s))$. If for every nonzero real $Q$ there is no state $s$ with log-charge$(s) = Q$, then for every state $s$ the log-charge of $s$ equals zero.
background
The Neutral Sector module shows that observable states in a zero-parameter ledger must lie in the neutral sector with conserved charge zero. An ObservableRatioModel on $α$ consists of a ratio : $α → ℝ_{>0}$ and log_charge : $α → ℝ$ obeying log_charge $s =$ Real.log(ratio $s$) for each $s$. The predicate sectorLabelIsFreeKnob model $Q$ holds precisely when some state realizes log-charge equal to $Q$ (from the sibling definition in the same module).
proof idea
The proof is by contradiction. Assume model.log_charge $s ≠ 0$. The hypothesis h_no_knob applied to this value together with the witness pair ⟨$s$, rfl⟩ yields an immediate contradiction. This is a one-line tactic wrapper using by_contra followed by exact.
why it matters
This theorem supplies the neutrality step that the downstream result parameter_free_ratios_are_unity relies upon to conclude that parameter-free ratios equal 1. It completes the Neutral Sector Forcing argument in the foundation module, enforcing that zero-parameter ledgers admit only the additive identity for sector labels. In the Recognition framework this aligns with the requirement that observable states be internally generated without external parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.