closedFramework_does_not_force_additive_posting
plain-language theorem explainer
The theorem establishes that a closed observable framework with positive ratio function need not satisfy additive posting on its orbit levels. Researchers deriving the T5 to T6 bridge in Recognition Science cite it to show why the primitive layer must be strengthened. The proof is a one-line wrapper that supplies the boolFramework counterexample together with its base state and the negation lemma for additive posting.
Claim. There exists a closed observable framework $F$ with state space $S$, transition map $T$, and positive ratio function $r:S→ℝ$, together with a base state $base∈S$, such that $r(T^2(base))≠r(T(base))+r(base)$.
background
ClosedObservableFramework is a structure consisting of a type $S$, a transition $T:S→S$, a ratio $r:S→ℝ$ that is everywhere positive, and a nontriviality condition guaranteeing at least two distinct ratio values. The module exhibits an explicit finite model called boolFramework whose states are Bool, whose transition is negation, and whose ratio alternates between 1 and 2. baseState is the false element of this model, and orbitLevels extracts the sequence of ratios along its orbit. The local setting is the honesty check for the T5→T6 bridge: ClosedObservableFramework alone is too weak to force either ratio_self_similar or additive_posting on the orbit-defined levels.
proof idea
The proof is a one-line wrapper that applies the exact tactic to the triple consisting of boolFramework, baseState, and the theorem orbit_not_additive_posting. That upstream lemma already shows by direct simplification that the second orbit level fails to equal the sum of the first and zeroth levels in the boolFramework model.
why it matters
This result demonstrates that the earlier primitive layer admits models where additive posting fails, thereby justifying the need for stronger structure before the self-similar fixed point phi can be forced. It supplies one half of the combined obstruction theorem stated immediately after in the same module. In the Recognition Science forcing chain it closes the honesty check that ClosedObservableFramework alone cannot derive the hierarchy fields required for T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.