preserves_equilibria
plain-language theorem explainer
Octave morphisms map balanced states to balanced states when the target strain functional is non-negative. Researchers modeling RRF transitions between manifestation scales cite this to guarantee equilibrium preservation under morphisms. The term proof unfolds the balance predicate, substitutes the input hypothesis, invokes non-negativity, and closes via linear arithmetic.
Claim. Let $O_1$ and $O_2$ be octaves with the strain functional of $O_2$ non-negative. For a morphism $f$ from $O_1$ to $O_2$, if state $x$ in $O_1$ satisfies zero strain and the strain of $f(x)$ is at most the strain of $x$, then $f(x)$ has zero strain in $O_2$.
background
An octave consists of a state space, a strain functional (J-cost measuring deviation from equilibrium), display channels, and non-emptiness. A morphism is a map preserving the weak ordering induced by strain. The module defines these structures abstractly without physical constants such as phi scaling or the eight-tick period; those enter as separate hypotheses. The isBalanced predicate is the zero-strain condition drawn from the glossary definition.
proof idea
The term proof applies simp to unfold isBalanced, rewrites the input balance hypothesis into the given inequality, invokes the non-negativity instance on the image state, and concludes by linear arithmetic.
why it matters
This theorem supplies one direction of balance preservation needed for octave equivalence. It supports downstream constructions of mutually inverse morphisms that preserve strain exactly. In the Recognition framework it fills the abstract octave layer before phi-ladder or eight-tick hypotheses are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.