boolFramework
plain-language theorem explainer
The definition constructs a finite ClosedObservableFramework on Boolean states with negation as transition map and observable values 1 and 2. Researchers auditing the T5 to T6 bridge cite it as the explicit counter-model showing that the ClosedObservableFramework axioms alone do not force ratio_self_similar or additive_posting on orbit levels. Construction proceeds by direct field assignment with case analysis and norm_num for positivity and nontriviality, plus the upstream non-injectivity theorem for the moduli condition.
Claim. Let $F$ be the closed observable framework with state space $S = B = $ {false, true}, transition $T(s) = $ negation of $s$, observable $r($false$) = 1$ and $r($true$) = 2$, charge function identically zero, and no continuous moduli (via non-injectivity of any map from reals to $B$). Then $F$ satisfies positivity of $r$, existence of distinct observable values, countability of $S$, and charge conservation.
background
ClosedObservableFramework is the structure consisting of a state type $S$, transition $T : S → S$, observable $r : S → ℝ$ obeying positivity and nontriviality, plus countability of $S$ and absence of continuous moduli. The module HierarchyRealizationObstruction uses this structure to test whether its axioms suffice for the hierarchy fields ratio_self_similar and additive_posting on the sequence $k ↦ r(T^{[k]} base)$. Upstream, the structure definition appears in ClosedObservableFramework; the non-injectivity result no_injective_real_to_bool supplies the no_continuous_moduli witness.
proof idea
The definition directly populates every field of the ClosedObservableFramework structure. Positivity of $r$ and nontriviality are discharged by cases on Bool with norm_num. Countability is witnessed by the parity map from naturals. The no_continuous_moduli field is supplied by the upstream theorem no_injective_real_to_bool. Charge conservation holds by reflexivity.
why it matters
This definition supplies the concrete model for the obstruction theorems closedFramework_does_not_force_ratio_self_similar, closedFramework_does_not_force_additive_posting, and the combined closedFramework_does_not_force_realizedHierarchy_fields. It thereby shows that any derivation of realized hierarchy fields after the T5 J-uniqueness step must invoke structure stronger than ClosedObservableFramework alone, closing the honesty check stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.