strain_strict_order_trans
plain-language theorem explainer
Strict transitivity of strain ordering asserts that if x is strictly better than y and y strictly better than z under a strain functional S, then x is strictly better than z. Researchers establishing consistent rankings in RRF order preservation would cite this result. The proof is a one-line wrapper applying the underlying less-than transitivity lemma to the two hypotheses.
Claim. Let $S$ be a strain functional on a state space. For states $x, y, z$, if the strain cost of $x$ is strictly less than that of $y$ and the strain cost of $y$ is strictly less than that of $z$, then the strain cost of $x$ is strictly less than that of $z$.
background
The module RRF.Theorems.OrderPreservation develops results on preservation of ordering by strain. A StrainFunctional is a structure assigning a cost $J : State → ℝ$ to each state, with the property that $J(x) = 0$ precisely when $x$ is at equilibrium. The relation strictlyBetter is defined by $S.J x < S.J y$ for states $x, y$ under $S$ (see upstream snippet for StrainFunctional and strictlyBetter). The local setting emphasizes that RRF tracks ordering of states by strain rather than absolute values, as stated in the module doc-comment.
proof idea
This is a one-line wrapper that applies the lt_trans lemma from ArithmeticFromLogic to the hypotheses hxy and hyz, which are the two strict inequalities on the strain costs.
why it matters
This theorem supplies the transitivity axiom for strict strain ordering inside the RRF order preservation module. It supports the module's key insight that operations preserving strain ordering also preserve meaning. The result aligns with the Recognition framework's focus on ordering rather than metric values and feeds into sibling results such as rank_invariant and strain_order_trans.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.