Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.lqr

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/lqr.clj1 definitions, 2 theorems

LQR linear feedback control (Kochenderfer Decision Making D7.11), one of the signed-subtraction cluster deferred in August until the signed layer landed. The control law is the linear feedback u = -K x: negate the gain-scaled state. `control/lqr-action gain state = signed/negate (signed/scale gain state)`, a higher-order composition of the two signed primitives, and the worked theorem proves the concrete action for gain 2, state 3 is equivalent to -6 by signed cross-product reflexivity -- the standard worked-instance idiom of the 222 catalog. Native and axiom-free on D63; a proved native module at module level, not a formally credited ledger row (that pipeline is a separate follow-up per the catalog workflow).

Depends onalgorithms.proofs.counterfactual-objective-lawsmath.rational.signed.deviation-rows

control/lqr-action :
  (x₁ : ℚ≥0) (x₂ : ℚ)
  → ℚ

control/lqr-action-worked :
  → control/lqr-action 2 (signed/from-nnrat 3) = signed/negate (signed/from-nnrat 6)

control/lqr-action-sign-reversing :
  (gain : ℚ≥0) (state : ℚ) (state-nonnegative : signed/nonnegative state)
  → control/lqr-action gain state ≤ 0