shifted_equilibrium
plain-language theorem explainer
The shifted quadratic strain functional on the reals vanishes at the shift parameter a. Model builders in the RRF framework cite this to confirm that the quadratic cost admits an equilibrium state at the prescribed location. The proof reduces immediately to the definitions via simplification.
Claim. Let $J_a : ℝ → ℝ$ be given by $J_a(x) = (x - a)^2$. Then $J_a(a) = 0$.
background
In the quadratic RRF model, states are real numbers and the strain functional assigns squared distance from a reference point as cost. The isBalanced predicate holds exactly when this cost is zero, marking equilibrium. The module presents this construction as a continuous optimization example inside the Recognition framework.
proof idea
The proof is a one-line wrapper that applies simplification to the definitions of isBalanced for StrainFunctional and the explicit form of the shifted quadratic strain.
why it matters
This result verifies the equilibrium property inside the quadratic RRF model and supports the claim that such functionals possess minimizers. It aligns with the Recognition Science focus on zero-strain balance conditions. No downstream theorems are recorded, yet the lemma anchors model-specific ledger checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.