channel_quality_transfer
plain-language theorem explainer
The declaration shows that an octave morphism preserving channel state qualities also preserves their ordering. Researchers modeling scale-invariant patterns in Recognition Science cite this when transferring equilibrium orderings between octaves. The proof rewrites both sides of the target inequality via the preservation hypothesis and discharges the result directly.
Claim. Let $O_1$ and $O_2$ be octaves, $i_1$ an index in the channels of $O_1$, and $i_2$ an index in the channels of $O_2$. Let $f$ be a morphism from $O_1$ to $O_2$. Assume that for every state $x$ of $O_1$, the state quality of channel $i_2$ at $f(x)$ equals the state quality of channel $i_1$ at $x$. Then for all states $x,y$ of $O_1$, if the state quality of channel $i_1$ at $x$ is at most that at $y$, the state quality of channel $i_2$ at $f(x)$ is at most that at $f(y)$.
background
The RRF.OctaveTransfer module treats octaves as self-similar structures at successive scales, with morphisms mapping states while preserving strain-related properties. State quality is the ordering measure attached to each channel; the Index type comes from the PeriodicTable structure that enumerates rails and blocks. Upstream definitions include discrete State types from fluid and vorticity models together with Pattern windows from measurement layers, all of which supply the concrete state spaces appearing in the hypotheses.
proof idea
Introduce the states x and y together with the ordering hypothesis. Rewrite the left- and right-hand sides of the target inequality by substituting the given channel-preservation equality at x and at y. The resulting statement is identical to the ordering hypothesis and is discharged immediately.
why it matters
The result supplies the order-transfer step required by the module's main theme that equivalent octaves manifest the same pattern at different scales. It sits inside the Recognition Science octave framework (T7) and supports downstream claims about equilibrium structures being identical under isometric strain maps. No open scaffolding remains; the lemma is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.