orbit_not_additive_posting
plain-language theorem explainer
The orbit under the boolean framework fails to satisfy additive posting at the first two steps. Researchers working on the T5 to T6 bridge in Recognition Science would cite this to show that ClosedObservableFramework is insufficient to derive hierarchy fields. The proof is a direct simplification that unfolds the orbit levels and the boolean framework definitions to obtain the concrete values 2, 1 and 1.
Claim. Let $F$ be the closed observable framework with state space Bool, transition $T$ the negation map, and observable $r$ equal to 2 on true and 1 on false. Let $s_0$ be false. Then $r(T^2 s_0) ≠ r(T s_0) + r(s_0)$.
background
ClosedObservableFramework is a structure with state space S, transition T : S → S, and positive real observable r, satisfying non-triviality (distinct r values exist) and closure (no external input). The boolFramework instantiates this with S = Bool, T = not, and r(b) = 2 if b else 1. baseState is the element false, and orbitLevels k is defined as r of the k-fold iterate of T applied to baseState.
proof idea
The proof is a one-line wrapper that applies simplification to unfold the definitions of orbitLevels, boolFramework, and baseState, directly computing the concrete values 2, 1 and 1 to verify the inequality.
why it matters
This theorem supplies the concrete counterexample used by closedFramework_does_not_force_additive_posting to establish that ClosedObservableFramework does not force additive_posting. It forms part of the obstruction showing that stronger structure is needed for the T5 to T6 bridge in the forcing chain. The combined theorem closedFramework_does_not_force_realizedHierarchy_fields uses it to block both ratio_self_similar and additive_posting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.