Pith. sign in
module module high

IndisputableMonolith.Foundation.NeutralSector

show as:
view Lean formalization →

The NeutralSector module introduces observable ratio models that assign positive real ratios to states on a type alpha while recording the associated log-charge. It extends the ZeroParameterComparisonLedger from the imported LedgerCanonicality module to handle neutral sectors. Foundation researchers cite it when establishing that parameter-free observables are neutral and that free ratios equal unity. The module consists entirely of definitions and supporting lemmas with no complex proofs.

claimAn observable ratio model on a type $\alpha$ is a structure assigning to each state a positive real ratio $r(s)>0$ together with its log-charge $\log r(s)$.

background

This module resides in the Foundation domain and imports LedgerCanonicality, whose doc-comment states: "A ZeroParameterComparisonLedger packages: 1. discrete state generation (countable carrier), 2. local binary comparison with a symmetric cost, 3. a conserved scalar quantity (log-charge)." The supplied DOC_COMMENT defines the central object: "An observable ratio model on a type α assigns a positive real ratio to each state and records the log-charge of that ratio." Sibling declarations such as ObservableRatioModel, sectorLabelIsFreeKnob, parameter_free_observables_are_neutral and neutral_ratio_eq_one indicate the module develops the neutral sector where ratios act as free knobs or collapse to unity.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the core objects for the neutral sector that feed sibling results such as parameter_free_observables_are_neutral and neutral_ratio_eq_one. These in turn support the Recognition Science forcing chain (T0-T8) by isolating the neutral case before J-uniqueness and the phi fixed point are imposed. It closes the gap between the conserved log-charge ledger and the claim that parameter-free ratios equal one.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)