channel_mono_transfer
plain-language theorem explainer
If two display channels share the same observation map and their quality functions differ by a monotone g, then the ordering of states by stateQuality transfers exactly from the first channel to the second. Researchers on RRF order preservation and strain-based ranking would cite this to justify that monotone reparameterizations leave comparative state orderings invariant. The proof is a short term-mode reduction that simplifies the composed stateQuality definitions, rewrites via the shared observe map and quality relation, and applies the Mond
Claim. Let $C_1$ and $C_2$ be display channels. Let $g : {R} {R}$ be monotone. If $C_2.quality(o) = g(C_1.quality(o))$ for all observations $o$ and $C_1.observe = C_2.observe$, then for all states $x,y$, $C_1.stateQuality(x) {C_1.stateQuality(y)$ implies $C_2.stateQuality(x) {C_2.stateQuality(y)$.
background
In the RRF framework a DisplayChannel pairs a quality map from observations to reals with an observe map from states to observations. stateQuality is defined as the composition quality ∘ observe, so states are ranked by the quality of the features they produce. The module states that RRF prioritizes ordering by strain over absolute values; any operation preserving this ordering preserves meaning.
proof idea
The term proof introduces x and y together with the assumed inequality on C1. It simplifies stateQuality using the composition definition and the rule comp_apply. It rewrites the inequality by substituting the shared observe map and the quality relation twice, reducing the claim to monotonicity of g applied directly to the original inequality.
why it matters
This is a basic order-preservation lemma inside the RRF order theorems module. It supports rank_invariant and channel_transfer results by showing monotone quality reparameterizations leave comparative rankings unchanged. In the Recognition framework it aligns with the emphasis on ordering rather than absolute measures, consistent with the strain-ordering focus in RRF core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.