trivial_is_minimizer
plain-language theorem explainer
In the trivial RRF model the unique state minimizes strain. Consistency checks of the core axiom bundle cite this result. The proof is a direct one-line application of the general fact that balanced states minimize non-negative strain.
Claim. Let $S$ be the trivial strain functional on the unit type. The unique state satisfies the minimizer predicate: for every state $y$, the strain cost of the unique state is at most the cost of $y$.
background
A strain functional assigns a non-negative real-valued cost $J$ to each state, with $J(x)=0$ precisely when the state is balanced. The minimizer predicate holds when no other state has strictly lower cost. The trivial model sets the state space to the unit type with $J$ identically zero, so the single state is balanced by reflexivity. The upstream theorem equilibria_are_minimizers states that any balanced state of a non-negative strain functional is a minimizer.
proof idea
One-line wrapper that applies equilibria_are_minimizers to the trivial strain functional at the unit state, supplying the trivial_balanced fact as the balance hypothesis.
why it matters
The result verifies that the simplest model satisfies the minimizer property demanded by the RRF axiom bundle, confirming internal consistency as stated in the module documentation. It rests on equilibria_are_minimizers together with the trivial balanced state. No downstream uses are recorded, so the declaration serves as a base case before non-trivial models are constructed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.