pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.ClosedObservableFramework

show as:
view Lean formalization →

The ClosedObservableFramework module supplies the minimal primitive for Recognition Science: a closed system of positive observables with ratio interface and conserved charge on a countable carrier. CostUniqueness cites it for the T5 J-uniqueness theorem while HierarchyRealization and its obstruction module import it to test hierarchy emergence. The module consists entirely of definitions and interface conditions C1-C3 with no theorems or proofs.

claimA closed observable framework consists of a countable carrier $S$, positive observables $o: S → ℝ^+$, a ratio comparison interface, and a conserved charge $Q$, satisfying non-trivial observability, closure with no external input, and finite description with no continuous moduli.

background

This module builds on the ZeroParameterComparisonLedger from LedgerCanonicality, which packages discrete countable states, local symmetric-cost binary comparisons, and a conserved log-charge scalar. The ClosedObservableFramework refines that ledger into a closed observable system with positive-valued observables and an explicit ratio interface. It enforces the three conditions stated in its doc-comment: non-trivial observability, closure, and countable states without continuous parameters.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the base object that CostUniqueness uses for its main T5 theorem establishing J-cost uniqueness from symmetry, unit normalization, strict convexity, and calibration. HierarchyRealization imports the framework to internalize levels directly onto carrier states and observables, while HierarchyRealizationObstruction demonstrates that the framework alone cannot force ratio self-similarity or additive posting. The structure therefore sits at the T5-to-T6 bridge in the forcing chain.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)