closedFramework_does_not_force_ratio_self_similar
plain-language theorem explainer
ClosedObservableFramework admits an explicit finite counterexample whose orbit ratios fail to be constant. Researchers deriving the T5 to T6 bridge in Recognition Science cite this result to establish that the basic closed-framework axioms are insufficient to force ratio self-similarity on orbit levels. The proof is a one-line term that directly packages the boolFramework counterexample with the already-proved non-self-similarity of its orbit.
Claim. There exists a closed observable framework $F$ (with state space $S$, transition $T:S→S$, and positive observable $r:S→ℝ^+$ satisfying nontriviality) together with a base state $s_0∈S$ such that the successive ratios $r(T^{k+2}s_0)/r(T^{k+1}s_0)$ are not independent of $k$.
background
ClosedObservableFramework is the structure consisting of a countable state space $S$, a transition map $T$, a positive real-valued observable $r$, and the axioms of nontrivial observability and closure. The module exhibits a concrete instance called boolFramework whose states are Bool, whose transition is negation, and whose observable alternates between the values 1 and 2. The base state is taken to be false, so the orbit is the periodic sequence 1,2,1,2,… . The upstream lemma orbit_not_ratio_self_similar records that this particular orbit violates the constant-ratio condition.
proof idea
The proof is a one-line term that supplies the triple (boolFramework, baseState, orbit_not_ratio_self_similar) as a witness. No further tactics or reductions are required once the counterexample and its non-self-similarity theorem are in hand.
why it matters
The declaration supplies the honesty check required by the module doc-comment: ClosedObservableFramework alone cannot derive ratio_self_similar for the orbit-defined levels. It therefore forces any derivation of the T5→T6 bridge (J-uniqueness to the self-similar fixed point phi) to import stronger structure than the basic closed axioms. The result sits immediately upstream of any attempt to realize the phi-ladder or the eight-tick octave inside a closed framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.