sectorLabelIsFreeKnob
plain-language theorem explainer
A definition stating that a real number Q is a free sector label for an observable ratio model if some state has log-charge exactly Q. Researchers formalizing zero-parameter ledgers cite this to enforce that observables carry no conserved charge. The definition is a direct existential quantification over states using the model's log-charge function.
Claim. For an observable ratio model $M$ on a type $α$, a real number $Q$ is a free sector label if there exists a state $s ∈ α$ such that the log-charge of $s$ under $M$ equals $Q$.
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 type $α$ consists of a positive real ratio function together with its log-charge, defined pointwise by $log_charge(s) = log(ratio(s))$. This log-charge is the conserved quantity of the ledger, taken from the upstream definition in VariationalDynamics that sums the logarithms of configuration entries and is preserved under evolution.
proof idea
This is a definition, implemented directly as the existential statement that some state $s$ satisfies model.log_charge $s = Q$. It encodes the supplied doc-comment that a sector label is free precisely when it can take any real value, witnessed by an existing state in the model.
why it matters
The definition supplies the key predicate used in the parent theorems parameter_free_observables_are_neutral and parameter_free_ratios_are_unity. It fills the forcing step in the module's argument: if a nonzero log-charge requires a free real knob, then the zero-parameter posture forces every observable log-charge to zero. This anchors the neutral-sector conclusion within the Recognition Science zero-parameter ledger requirement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.