comp_preserves_order
plain-language theorem explainer
Composition of octave morphisms preserves the weaklyBetter ordering on states induced by strain. Researchers modeling scale transfer in Recognition Science cite this when chaining morphisms across octaves. The proof is a one-line wrapper that extracts the preserves_order field already constructed in the definition of morphism composition.
Claim. Let $O_1, O_2, O_3$ be octaves. For morphisms $f: O_1 → O_2$ and $g: O_2 → O_3$, and states $x, y$ in the state space of $O_1$ such that $x$ is weakly better than $y$ under the strain ordering of $O_1$, the images of $x$ and $y$ under the composed map satisfy the weakly better relation under the strain ordering of $O_3$.
background
Octaves model self-similar patterns at successive scales and carry a strain function that induces a weaklyBetter partial order on their states. An OctaveMorphism is a map between octaves that preserves this ordering. The upstream definition of composition in RRF.Core.Octave sets the map to the ordinary function composition and defines the preserves_order field by chaining: g.preserves_order applied after f.preserves_order on the given pair and hypothesis.
proof idea
The proof is a one-line wrapper that applies the preserves_order field of the composed morphism (OctaveMorphism.comp g f). That field was already assembled in the upstream comp declaration by nesting the two individual preservation steps, so the theorem simply projects the required instance for the supplied x, y, and hxy.
why it matters
The result completes the ordering-transfer half of the OctaveTransfer module, whose documentation highlights that equivalent octaves share equilibrium structures and that morphisms allow patterns to transfer across scales. It sits alongside the sibling morphism_preserves_order and supports the eight-tick octave structure by ensuring order relations survive composition. No downstream uses are recorded, so its integration into full equivalence theorems remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.