IndisputableMonolith.Cybernetics.FeedbackControlModesFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Feedback Control Modes from configDim — Cybernetics Depth
   6
   7Five canonical feedback-control modes (= configDim D = 5):
   8  proportional, integral, derivative, feedforward, adaptive.
   9
  10The first three are PID axes; feedforward and adaptive close the
  11model-based and learning-control channels.
  12
  13Lean status: 0 sorry, 0 axiom.
  14-/
  15
  16namespace IndisputableMonolith.Cybernetics.FeedbackControlModesFromConfigDim
  17
  18inductive FeedbackControlMode where
  19  | proportional
  20  | integral
  21  | derivative
  22  | feedforward
  23  | adaptive
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem feedbackControlMode_count :
  27    Fintype.card FeedbackControlMode = 5 := by decide
  28
  29structure FeedbackControlModesCert where
  30  five_modes : Fintype.card FeedbackControlMode = 5
  31
  32def feedbackControlModesCert : FeedbackControlModesCert where
  33  five_modes := feedbackControlMode_count
  34
  35end IndisputableMonolith.Cybernetics.FeedbackControlModesFromConfigDim
  36