trivialStrain
plain-language theorem explainer
The trivial strain functional assigns zero J-cost to every element of the single-point state space. Researchers checking internal consistency of the RRF axiom bundle cite it as the minimal base case. The definition is a direct construction of the constant-zero map together with a non-negativity instance obtained by reflexivity.
Claim. Let $S$ be the one-element state space. The trivial strain functional is the map $J:S→ℝ$ defined by $J(s)=0$ for the unique $s∈S$, equipped with the non-negativity witness $0≤0$.
background
The RRF trivial model reduces the state space to a single point via TrivialState, defined as the unit type. StrainFunctional is the structure carrying a J map from states to reals together with a NonNeg instance that enforces non-negative values. The module documentation states that this construction yields a ledger that is trivially closed and thereby proves internal consistency of the core axiom bundle.
proof idea
The definition directly supplies the constant-zero function for J. Non-negativity is witnessed by applying the le_refl lemma to zero, which yields the required 0 ≤ 0 instance.
why it matters
This definition supplies the base strain used by trivial_balanced, trivial_is_minimizer, trivialOctave and trivialStrainLedger. It occupies the minimal consistent model slot in the RRF framework, confirming that the core axioms admit at least one realization without reference to the forcing chain, phi-ladder or eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.