ClosedObservableFramework
plain-language theorem explainer
ClosedObservableFramework supplies the base structure for closed observable systems in Recognition Science, with positive ratio observable r, dynamics T preserving charge, countable states, and no continuous moduli. It is cited by ledger reconstruction and the T5-T6 forcing bridges in HierarchyDynamics. The declaration is a structure definition that directly bundles conditions C1-C3 as fields rather than separate axioms.
Claim. A structure consisting of a type $S$ of states, a map $T:S→S$, a positive observable $r:S→ℝ$ satisfying $r(s)>0$ for all $s$, distinct values of $r$, a surjective enumeration $ℕ→S$, no injective embedding $ℝ→S$, and a charge map conserved under $T$.
background
The module treats Gap 1 of the axiom-closure plan (phases 1, 2, 6). ClosedObservableFramework absorbs R1, R2, R5, R6 as structure fields, leaving only the Regularity Axiom to encode the finite-description content of C3. The local setting is a closed system with no external input and finite description via countability plus absence of continuous moduli.
proof idea
This declaration is a structure definition with no proof body; it assembles the fields for positive observables, ratio interface, conserved charge, and the three conditions C1-C3 into a single type.
why it matters
It is the parent for ledger_reconstruction (which proves R1-R6 with three explicit finite-description obligations) and for the bridge_T5_T6 theorems that force the scale ratio to phi. The structure realizes the closed observable setting required for J-uniqueness (T5) and the self-similar fixed point (T6) in the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.