orbit_not_ratio_self_similar
plain-language theorem explainer
The orbit generated by the boolean closed-observable framework with negation transition and readout alternating between 1 and 2 fails ratio self-similarity. Researchers deriving the T5-to-T6 bridge in Recognition Science cite this to demonstrate that ClosedObservableFramework alone cannot enforce the required hierarchy property. The proof specializes the assumed universal quantifier at k=0 and reduces the resulting numerical equality to a contradiction via simplification and normalization.
Claim. Let $F$ be the closed-observable framework with state space Bool, transition $T$ given by negation, and readout $r$ sending false to 1 and true to 2. Let $s$ be the base state false. Then it is not the case that for every natural number $k$, $r(T^{k+2}s)/r(T^{k+1}s) = r(T^{k+1}s)/r(T^ks)$.
background
The module exhibits an explicit finite counterexample showing that ClosedObservableFramework is too weak to derive ratio self-similarity or additive posting for orbit-defined levels. The boolFramework is defined with state space Bool, transition negation, and readout sending false to 1 and true to 2; its orbit alternates between these two observable values. baseState is the initial false element, and orbitLevels(k) is obtained by applying the readout to the k-fold iterate of the transition on baseState.
proof idea
The term proof introduces the assumed universal equality, specializes it at k=0 to obtain a concrete numerical statement, then applies simplification using the definitions of orbitLevels, boolFramework and baseState followed by numerical normalization to reach a contradiction.
why it matters
This theorem supplies the concrete witness for the parent result closedFramework_does_not_force_ratio_self_similar, which states that ClosedObservableFramework admits models where the ratio-self-similar condition fails. It forms part of the honesty check for the T5-to-T6 bridge: the earlier primitive layer must be strengthened before the self-similar fixed point phi can be forced. The combined obstruction theorem then packages this failure together with the additive-posting failure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.