neutral_ratio_eq_one
A state with zero log-charge in an observable ratio model has ratio exactly one. Workers on zero-parameter ledgers cite this to force neutrality of observables. The proof rewrites the log-charge hypothesis into a logarithm equality and invokes injectivity of the logarithm on the positive reals.
claimLet $M$ be an observable ratio model on a type $α$. For a state $s ∈ α$ satisfying log-charge$(s) = 0$, the ratio of $s$ equals 1.
background
An observable ratio model on a type $α$ assigns to each state a positive real ratio together with its logarithm, called the log-charge. By definition the log-charge of a state equals the natural logarithm of its ratio. The module establishes that in a zero-parameter ledger every observable state must lie in the neutral sector, meaning its conserved charge vanishes.
proof idea
The proof obtains Real.log (model.ratio s) = 0 by rewriting the neutral hypothesis with the equality log_charge s = Real.log (ratio s). It then applies Real.log_injOn_pos on the positive reals, using that the ratio is positive and that log 1 equals zero, to conclude the ratio equals one.
why it matters in Recognition Science
This theorem supplies the core step for parameter_free_ratios_are_unity, which asserts that all parameter-free observable ratios equal one. It fills the neutral-sector forcing step in the zero-parameter ledger argument of the module. In the Recognition framework it supports the claim that observables carry no free parameters and therefore sit at the neutral point.
scope and limits
- Does not establish neutrality for states outside the observable ratio model.
- Does not derive the zero log-charge condition from first principles.
- Does not extend to models with nonzero conserved charges.
formal statement (Lean)
54theorem neutral_ratio_eq_one
55 {α : Type}
56 (model : ObservableRatioModel α)
57 (s : α)
58 (h_neutral : model.log_charge s = 0) :
59 model.ratio s = 1 := by
proof body
Tactic-mode proof.
60 have hlog : Real.log (model.ratio s) = 0 := by
61 rw [← model.log_charge_eq s]; exact h_neutral
62 exact Real.log_injOn_pos (Set.mem_Ioi.mpr (model.ratio_pos s))
63 (Set.mem_Ioi.mpr one_pos) (by rw [hlog, Real.log_one])
64
65/-- **Bridge B4 core (unconditional)**: parameter-free observable
66ratios in a zero-parameter ledger are all equal to 1. -/