neutral_ratio_eq_one
plain-language theorem explainer
If an observable ratio model assigns zero log-charge to a state, then the associated ratio equals one. Researchers establishing neutral-sector forcing for zero-parameter ledgers cite this when showing that parameter-free observables must be unity. The proof rewrites the log-charge hypothesis via the model's defining equality and invokes injectivity of the real logarithm on positive reals.
Claim. Let $M$ be an observable ratio model on a type $α$. For any state $s$ such that the log-charge of $s$ under $M$ equals zero, the ratio of $s$ under $M$ equals 1.
background
The Neutral Sector module shows that observable states of a zero-parameter ledger must lie in the neutral sector where conserved charge equals zero. An ObservableRatioModel on a type $α$ supplies a positive-real ratio function together with a log-charge function obeying log_charge s = Real.log (ratio s) for every s. This structure rests on the log_charge definition from VariationalDynamics, which sums the logarithms of configuration entries and treats the result as a conserved quantity preserved under evolution.
proof idea
The tactic proof first obtains Real.log (model.ratio s) = 0 by rewriting with the log_charge_eq field of the model. It then applies Real.log_injOn_pos to the positive ratio, to the positive number one, and to the rewritten equality together with Real.log_one.
why it matters
This supplies the direct step used by parameter_free_ratios_are_unity, the unconditional statement that parameter-free observable ratios in a zero-parameter ledger equal one. It completes the core of Bridge B4 in the neutral-sector forcing argument: zero log-charge forces unit ratio. Within the Recognition framework the result reinforces that observables must occupy the neutral sector once external parameters are disallowed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.