neutralSector
plain-language theorem explainer
neutralSector extracts the zero-charge subset of states from any ZeroParameterComparisonLedger. Researchers on neutral dynamics or hierarchy emergence cite this set when establishing nonempty neutral sectors. The definition is a direct set comprehension on the conserved charge component of the ledger structure.
Claim. Let $L$ be a zero-parameter comparison ledger with carrier set and conserved charge map. The neutral sector is the set $S = { s ∈ Carrier(L) | charge_L(s) = 0 }$.
background
A ZeroParameterComparisonLedger packages a countable nonempty carrier, an admissible cost satisfying the recognition composition law, and a conserved charge map on the carrier. The module presents this structure as the single primitive interface for unconditional emergence theorems, with no external parameters. The charge field is the conserved scalar (log-charge) required for the ledger to support neutral dynamics.
proof idea
The definition is a direct set comprehension that selects states where the charge field of the ledger evaluates to zero.
why it matters
This definition supplies the neutral sector consumed by HasNeutralStates to assert nonemptiness for generic inhabited ledgers. It forms part of the zero-parameter ledger interface that feeds hierarchy and factorization results downstream from the unconditional theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.