strictlyBetter
plain-language theorem explainer
strictlyBetter defines when one state has strictly lower strain cost than another under a given strain functional. Researchers establishing order preservation for strain minimization cite this when proving transitivity of improvements. The definition reduces directly to a comparison of the real-valued J costs.
Claim. Let $S$ be a strain functional on a state space. State $x$ is strictly better than state $y$ when the strain cost satisfies $J(x) < J(y)$.
background
The RRF Core Strain module treats strain as the measure of deviation from equilibrium, with the governing law that strain tends to zero. A strain functional assigns a real cost $J$ to each state such that $J(x) = 0$ precisely when the state is balanced, and non-negativity is imposed separately as a class constraint.
proof idea
The declaration is a definition that unfolds directly to the inequality on the strain values. It supplies the base proposition for one-line applications of transitivity in order-preservation results.
why it matters
This definition is invoked by the strain_strict_order_trans theorem, which proves transitivity of strict improvements via lt_trans. It supports the RRF treatment of strain as the indicator of consistency, aligning with the framework principle that lower strain corresponds to greater reality and enabling comparisons in equilibrium and minimization arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.