orbitLevels
plain-language theorem explainer
orbitLevels defines the sequence of readout values obtained by applying the boolFramework readout r to the k-fold iterate of its transition T starting from baseState. Researchers auditing the T5 to T6 bridge cite it to construct an explicit finite counterexample orbit. The definition is a direct one-line composition of the framework's readout operator with iteration on the initial state.
Claim. Define the orbit levels by $l(k) := r(T^k(s_0))$ for $k : ℕ$, where $s_0$ is the base state, $T$ the transition map, and $r$ the readout function of the boolFramework.
background
The boolFramework is a ClosedObservableFramework instance with state space Bool, transition map not, and readout sending false to 1 and true to 2. baseState is the initial false element. This produces an alternating orbit of readout values 1 and 2 under iteration. The module doc states that ClosedObservableFramework alone is too weak to derive ratio_self_similar or additive_posting for the orbit-defined levels $k ↦ r(T^[k] baseState)$, requiring stronger prior structure for any honest T5 to T6 derivation.
proof idea
Direct definition that composes the readout r of boolFramework with the k-fold iteration of its transition T applied to baseState.
why it matters
This definition supplies the concrete sequence used by the downstream theorems orbitLevels_zero, orbitLevels_one, orbitLevels_two, orbit_not_ratio_self_similar, and orbit_not_additive_posting. Those results exhibit the counterexample showing ClosedObservableFramework cannot force the hierarchy fields needed after T5 J-uniqueness for the T6 phi fixed-point step. It closes the honesty check that any derivation of self-similarity must invoke stronger earlier structure than the current primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.