closedFramework_does_not_force_realizedHierarchy_fields
plain-language theorem explainer
Researchers bridging T5 uniqueness to the phi fixed point cite this result to show that ClosedObservableFramework alone permits orbits lacking both ratio self-similarity and additive posting. The explicit counterexample is the two-state boolFramework whose r values alternate between 1 and 2 under negation. The proof is a one-line term that packages the framework, base state, and the two negation lemmas.
Claim. There exists a closed observable framework $F$ and base state $s$ in $F.S$ such that the orbit sequence $a_k = r(T^k s)$ satisfies neither $a_{k+2}/a_{k+1} = a_{k+1}/a_k$ for all $k$ nor $a_2 = a_1 + a_0$.
background
ClosedObservableFramework is a structure with state space $S$, transition $T: S → S$, positive observable $r: S → ℝ$, and nontriviality. The boolFramework realizes it via $S = $ Bool, $T =$ negation, and $r$ sending false to 1 and true to 2. Orbit levels are the sequence obtained by iterating $T$ from baseState (false) and applying $r$, producing the alternating values 1, 2, 1, 2, …. The module documentation states that this setup tests whether the T5 to T6 bridge can be derived from the closed framework alone.
proof idea
The proof is a one-line term that supplies boolFramework as the framework, baseState as the base, and the two theorems orbit_not_ratio_self_similar and orbit_not_additive_posting as witnesses for the negations.
why it matters
This combined obstruction shows that ClosedObservableFramework is too weak to force the hierarchy fields used by the internal bridge. It feeds directly into closedFramework_alone_insufficient_for_bridge in HierarchyDynamics and fills the honesty check for the T5 to T6 step in the forcing chain. The result underscores the need for additional structure beyond the current primitive layer to reach the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.