orbitLevels_zero
plain-language theorem explainer
The orbit level function evaluates to 1 at step zero in the boolean counterexample. Researchers auditing the T5 to T6 bridge cite this to confirm the base case of the obstruction showing ClosedObservableFramework is too weak for hierarchy fields. The proof is a one-line simp wrapper that unfolds the definitions of orbitLevels, boolFramework, and baseState.
Claim. In the boolean counterexample, the readout after zero transitions from the base state equals 1: $orbitLevels(0) = 1$.
background
The module exhibits an explicit finite counterexample to demonstrate that ClosedObservableFramework alone cannot derive ratio_self_similar or additive_posting for the orbit-defined levels $k mapsto r(T^[k] baseState)$. boolFramework is the ClosedObservableFramework with state space Bool, transition not, and readout r sending false to 1 and true to 2. baseState is the constant false element. orbitLevels(k) is then the readout after k applications of the transition starting from baseState.
proof idea
The proof is a one-line simp wrapper that unfolds orbitLevels, boolFramework, and baseState to reduce the claim to the definition of r on false.
why it matters
This supplies the base case for the orbit levels in the counterexample used to obstruct hierarchy realization from ClosedObservableFramework. It supports the module's claim that stronger earlier structure is required for the T5 to T6 transition. The result closes the zero case without touching open questions on the full obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.