weaklyBetter
plain-language theorem explainer
weaklyBetter declares that state x has strain cost no higher than state y under a given strain functional. Researchers building order-preserving maps between octaves or characterizing minimizers cite this relation when working in the RRF core. The definition is a direct one-line comparison of the two J values.
Claim. For a strain functional $S$ on states, $x$ is weakly better than $y$ when $J(x) ≤ J(y)$.
background
StrainFunctional is a structure assigning a real-valued strain cost $J$ to each state, with non-negativity imposed separately and $J(x)=0$ exactly at equilibrium. The RRF.Core.Strain module treats strain as the fundamental deviation from balance, where $J→0$ encodes the law of increasing consistency. The State type is the discrete 2D Galerkin state from the CPM2D bridge; upstream constants such as active edge count $A$ enter related balance identities.
proof idea
One-line definition that sets weaklyBetter S x y to the inequality S.J x ≤ S.J y.
why it matters
This supplies the ordering used by OctaveMorphism to preserve strain order across octaves and by equilibria_are_minimizers to prove balanced states are minimizers. It anchors the basic comparison in the strain-ordering theorems of the RRF core, supporting the strain-to-zero law and the eight-tick octave structure via morphisms that respect phi-ladder ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.