pith. sign in
module module high

IndisputableMonolith.Foundation.ClosedObservableFramework

show as:
view Lean formalization →

ClosedObservableFramework defines the structure for closed systems with positive observables, ratio interfaces, and conserved charges under non-trivial observability, closure, and finite countable description. It is cited by CostUniqueness for the T5 J-uniqueness result and by hierarchy modules. This is a definition module that packages the ZeroParameterComparisonLedger with added closure axioms.

claimA closed observable framework consists of a countable carrier $S$, positive observables $o: S → ℝ_{>0}$, a ratio interface, and conserved charge, satisfying (C1) non-trivial observability, (C2) closure with no external input, and (C3) finite description with no continuous moduli.

background

The module extends the ZeroParameterComparisonLedger from LedgerCanonicality, which packages discrete state generation on a countable carrier, local binary comparison with symmetric cost, and a conserved scalar quantity (log-charge). It adds the three conditions C1-C3 to enforce a closed system. The local theoretical setting is the Recognition Science primitive for unconditional inevitability theorems, where structures derive from comparison ledgers without free parameters.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the base structure for the T5 uniqueness theorem in CostUniqueness, where any cost functional meeting symmetry, normalization, convexity, and calibration equals J-cost. It is internalized in HierarchyRealization to connect carrier states to level observables, while HierarchyRealizationObstruction records that it remains too weak to derive ratio_self_similar or additive_posting, serving as the honesty check on the T5 to T6 bridge.

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)