OctaveMorphism
plain-language theorem explainer
An OctaveMorphism from octave O1 to O2 is a map on their state spaces that preserves the ordering induced by each strain functional, where one state is weakly better than another precisely when its J-cost is smaller. Researchers modeling scale-invariant patterns across manifestation levels cite this when composing maps or transferring equilibria between octaves. The declaration is a bare structure definition with no proof obligations or computational content.
Claim. Let $O_1$ and $O_2$ be octaves with respective state spaces $S_1$, $S_2$ and strain functionals $J_1$, $J_2$. A morphism $f: O_1 → O_2$ consists of a function $f: S_1 → S_2$ such that $J_1(x) ≤ J_1(y)$ implies $J_2(f(x)) ≤ J_2(f(y))$ for all $x, y ∈ S_1$.
background
In the RRF Core module an octave is an abstract structure consisting of a state space, a strain functional (the J-cost that quantifies deviation from equilibrium), a bundle of display channels, and a non-emptiness witness. The strain functional induces the relation weaklyBetter, defined by $S.J x ≤ S.J y$, which orders states by quality without reference to physical constants. The module treats octaves as scales of manifestation where the same underlying patterns recur, with any φ-scaling introduced only as a later hypothesis.
proof idea
This is a structure definition that directly introduces the two fields map and preserves_order. No lemmas are invoked and no tactics are used; the declaration simply packages the data required for a strain-order-preserving map between octaves.
why it matters
OctaveMorphism supplies the arrows for the category of octaves inside the Recognition framework, enabling the definitions of identity, composition, and OctaveEquiv that appear later in the same module. It is invoked by the theorems channel_quality_transfer, comp_preserves_order, and morphism_preserves_order in OctaveTransfer, which rely on order preservation to move quality statements across scales. The structure therefore supports the claim that patterns at different manifestation levels are related by maps that respect strain, consistent with the self-similar fixed point and the abstract octave construction before concrete constants are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.