boolFramework
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,
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert that every ClosedObservableFramework satisfies ratio self-similarity.
- Does not derive the phi-ladder mass formula or eight-tick octave.
- Does not claim that the observable map from reals is injective.
- Does not supply a positive existence proof for realized hierarchy fields.
Lean usage
example : ClosedObservableFramework := boolFrameworkformal statement (Lean)
43def boolFramework : ClosedObservableFramework where
44 S := Bool
proof body
Definition body.
45 T := not
46 r := fun b => if b then 2 else 1
47 r_pos := by
48 intro b
49 cases b <;> norm_num
50 nontrivial := by
51 refine ⟨false, true, ?_⟩
52 norm_num
53 S_countable := by
54 refine ⟨fun n => if n % 2 = 0 then false else true, ?_⟩
55 intro b
56 cases b
57 · refine ⟨0, ?_⟩
58 simp
59 · refine ⟨1, ?_⟩
60 simp
61 no_continuous_moduli := no_injective_real_to_bool
62 charge := fun _ => 0
63 charge_conserved := by
64 intro s
65 rfl
66
67/-- The base state used for the obstruction. -/