HasNeutralStates
plain-language theorem explainer
Any zero-parameter comparison ledger possesses at least one neutral state. Researchers proving the unconditional inevitability theorem invoke this interface to cover the generic zero-charge case. The declaration is a class with a single field that directly requires the neutral sector to be nonempty.
Claim. Let $L$ be a zero-parameter comparison ledger. Then the neutral sector of $L$ is nonempty.
background
The module defines the ZeroParameterComparisonLedger as the refined primitive object for the unconditional inevitability theorem. It packages a countable carrier with nonempty and surjective enumeration, an admissible cost function satisfying the Recognition Composition Law, a conserved charge, the prohibition on free real embeddings, and cost sufficiency under scaling. Every downstream emergence theorem for hierarchy, factorization, and neutral dynamics consumes this single interface. The neutral sector is the subset of states with zero conserved charge.
proof idea
The declaration is a class definition whose sole field is the nonemptiness assertion on the neutral sector. No lemmas are applied and no tactics are used.
why it matters
This interface supplies the generic zero-charge assumption required by the unconditional inevitability theorem in the Foundation module. It closes the case for inhabited ledgers without external parameters and feeds the neutral dynamics results that follow from the ledger interface. The construction aligns with the zero-parameter ledger that eliminates all free knobs before deriving T5 J-uniqueness and subsequent chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.