IndisputableMonolith.Foundation.NeutralSector
The NeutralSector module defines an observable ratio model on a type α that assigns a positive real ratio to each state and records the associated log-charge. It extends the zero-parameter comparison ledger to isolate the neutral sector within Recognition Science. Researchers deriving unity ratios for parameter-free observables cite this module. The module consists of the core definition together with direct lemmas on free knobs and neutrality.
claimAn observable ratio model on a type $α$ consists of a function $r:α→ℝ_{>0}$ together with its log-charge $log r:α→ℝ$.
background
The module resides in the Foundation domain and imports the Zero-Parameter Local Conserved Comparison Ledger. That ledger packages a countable carrier for discrete states, local binary comparison equipped with a symmetric cost, and a conserved scalar quantity called log-charge. NeutralSector refines this ledger by introducing the ObservableRatioModel to capture ratios that remain neutral when no free parameters are present.
proof idea
This is a definition module, no proofs. It introduces the ObservableRatioModel structure and states supporting lemmas such as sectorLabelIsFreeKnob and parameter_free_observables_are_neutral that follow immediately from the ledger axioms.
why it matters in Recognition Science
The module feeds into higher-level results on neutral ratios and parameter-free observables. It isolates the neutral sector required for the unconditional inevitability theorem and supports the zero-parameter approach of the upstream ledger.
scope and limits
- Does not introduce the J-function or phi-ladder.
- Does not define time evolution or dynamics.
- Does not prove conservation beyond the imported ledger.
- Does not address non-neutral or charged sectors.