strain_order_trans
plain-language theorem explainer
Transitivity of the weaklyBetter relation on states under any StrainFunctional follows from the underlying arithmetic order. Researchers chaining strain comparisons in RRF optimization or ranking arguments cite this result. The proof is a direct one-line application of le_trans to the two hypotheses.
Claim. If a strain functional $S$ on states satisfies $S$ weakly prefers $x$ to $y$ and $y$ to $z$, then $S$ weakly prefers $x$ to $z$.
background
The RRF.Theorems.OrderPreservation module shows that RRF tracks relative ordering of states by strain rather than absolute strain values. A StrainFunctional induces the weaklyBetter relation on the discrete state space. The upstream le_trans theorem supplies transitivity for the underlying LogicNat ordering that weaklyBetter lifts.
proof idea
One-line wrapper that applies the le_trans lemma directly to the hypotheses hxy and hyz.
why it matters
This result supplies the basic composition property for strain orderings that the module uses to build rank_invariant and channel_mono_transfer. It matches the module's stated key insight that only ordering matters for preserving meaning under RRF operations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.