HasNeutralStates
plain-language theorem explainer
Zero-parameter comparison ledgers carry a nonempty neutral sector under the HasNeutralStates class. Researchers deriving neutral dynamics or canonicality results in Recognition Science cite this interface to guarantee zero-charge states exist in the generic inhabited case. The declaration is a direct class definition consisting of one field that asserts nonemptiness of the extracted neutral sector.
Claim. A zero-parameter comparison ledger $L$ satisfies the neutral-states property when the set of its zero-charge states is nonempty.
background
The module introduces the ZeroParameterComparisonLedger structure: a countable nonempty carrier equipped with an admissible cost (satisfying the J-cost functional equation), a conserved charge map, the no-free-knobs condition, and cost sufficiency under scaling. The neutral sector is the subset of carrier elements whose conserved charge vanishes. The HasNeutralStates class packages the single requirement that this subset is inhabited for any such ledger.
proof idea
One-line class definition whose sole field is the nonemptiness assertion on the neutral sector of the supplied ledger.
why it matters
The declaration supplies the minimal interface needed for downstream neutral-dynamics theorems inside the unconditional inevitability result. It closes the generic zero-charge case for the zero-parameter ledger that every hierarchy and factorization construction consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.