boolFramework
plain-language theorem explainer
boolFramework supplies an explicit finite model of ClosedObservableFramework whose state space is the Boolean type, transition is logical negation, and observable ratio alternates between 1 and 2 under iteration. Researchers working on the T5 to T6 bridge cite this construction to exhibit a counterexample showing that the primitive framework axioms alone do not entail self-similar ratio orbits or additive posting. The definition populates the structure fields directly and verifies positivity, nontriviality, countability, and absence of moduli,
Claim. A closed observable framework whose state space is the two-element Boolean set, whose transition map is logical negation, and whose observable ratio function sends true to 2 and false to 1, satisfying positivity of the ratio, existence of distinct ratio values, countability of the state space, and absence of an injective embedding from the reals.
background
ClosedObservableFramework is the structure consisting of a state space S, transition T : S → S, observable r : S → ℝ, together with proofs that r is everywhere positive, that distinct states exist with distinct r-values, that S is countable, and that no continuous modulus exists (i.e., no injective map ℝ → S). The module doc-comment states that this supplies the key honesty check for the T5→T6 bridge: the earlier primitive is too weak to derive ratio_self_similar or additive_posting on the orbit levels k ↦ r(T^[k] base). The upstream no_injective_real_to_bool theorem asserts that any map ℝ → Bool fails to be injective and is used to discharge the no_continuous_moduli field.
proof idea
The definition directly instantiates the ClosedObservableFramework structure by setting S to Bool, T to logical negation, and r to the function returning 2 on true and 1 on false. The field proofs are discharged by case analysis on Bool followed by norm_num for r_pos and nontriviality, by exhibiting an explicit enumeration for S_countable, by direct appeal to the imported no_injective_real_to_bool for no_continuous_moduli, and by reflexivity for charge conservation.
why it matters
This definition populates the existential quantifiers in the downstream obstruction theorems closedFramework_does_not_force_ratio_self_similar, closedFramework_does_not_force_additive_posting, and closedFramework_does_not_force_realizedHierarchy_fields. It thereby shows that any derivation of the self-similar phi-ladder or additive posting must invoke stronger structure than ClosedObservableFramework alone, consistent with the module statement that honest derivations require additional earlier axioms beyond the T5 J-uniqueness layer. The construction touches the open question of the minimal strengthening needed to force the T6 fixed-point hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.