orbitLevels_one
plain-language theorem explainer
orbitLevels_one shows the readout after one transition step in the boolean counterexample equals 2. Researchers auditing the T5 to T6 bridge would cite it to verify the explicit finite obstruction. The proof is a one-line simp wrapper that unfolds the definitions of orbitLevels, boolFramework, and baseState.
Claim. In the boolean framework with state space Bool, transition the negation map, and readout sending false to 1 and true to 2, the level after one iteration satisfies $r(T^1(false)) = 2$.
background
The module supplies an explicit finite counterexample demonstrating that ClosedObservableFramework alone cannot force ratio_self_similar or additive_posting on the orbit-defined levels k maps to r(T^[k] baseState). boolFramework is the structure with S equal to Bool, T the negation, and r(b) equal to 2 if b is true else 1. baseState is the constant false. orbitLevels(k) is then the readout of the k-fold iterate of T applied to baseState.
proof idea
The proof is a one-line simp wrapper that applies the definitions of orbitLevels, boolFramework, and baseState to reduce the equality to a direct boolean computation.
why it matters
This result supplies one concrete verification step inside the obstruction module, confirming that ClosedObservableFramework is too weak to derive the hierarchy fields needed for the T5 J-uniqueness to T6 phi fixed-point bridge. It supports the module's claim that any honest derivation of self-similar structure must invoke stronger earlier axioms than the closed-observable framework alone. The theorem does not touch open questions; it simply discharges the k=1 case of the counterexample.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.