neutralSector
plain-language theorem explainer
The neutral sector isolates the zero-charge states inside any zero-parameter comparison ledger. Researchers deriving neutral dynamics or hierarchy emergence from the unconditional theorem would reference this set when proving non-emptiness or stability. It is introduced by direct set comprehension on the ledger's conserved charge component.
Claim. Let $L$ be a zero-parameter local conserved comparison ledger with carrier $C$ and conserved charge $q$. The neutral sector is the subset $N = { s ∈ C | q(s) = 0 }$.
background
The module defines the ZeroParameterComparisonLedger as the single primitive interface for unconditional emergence theorems. It packages a countable nonempty carrier, an admissible cost obeying the Recognition Composition Law, a conserved scalar charge, and closure under composition with no external parameters. The neutral sector is the subset of carrier elements whose charge vanishes. This construction sits inside the broader ledger interface that every downstream hierarchy or factorization result consumes.
proof idea
Direct set comprehension over the charge field of the supplied ledger structure.
why it matters
The definition supplies the object consumed by the HasNeutralStates class, which asserts non-emptiness for any inhabited zero-parameter ledger. It therefore participates in the chain that extracts neutral dynamics from the conserved-charge component of the ledger, a prerequisite for later composition and hierarchy results in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.