FeedbackControlMode
plain-language theorem explainer
The inductive definition enumerates five canonical feedback control modes that correspond to a configuration dimension of five. Researchers formalizing PID controllers with added feedforward and adaptive channels in the Recognition Science framework would cite this enumeration to anchor discrete mode counts. The definition proceeds by direct listing of the five cases followed by automatic derivation of finite-type and equality instances.
Claim. Let $M$ denote the set of feedback control modes. Then $M$ consists of the five elements proportional, integral, derivative, feedforward, and adaptive, equipped with decidable equality and finite cardinality.
background
The module introduces feedback control modes to realize a configuration dimension of five. Proportional, integral, and derivative form the classical PID axes, while feedforward supplies model-based prediction and adaptive supplies learning-based adjustment. This construction sits inside the cybernetics depth of Recognition Science, where dimensional constraints (configDim = 5) generate discrete control structures without additional axioms.
proof idea
The declaration is an inductive type definition that lists five constructors and invokes the deriving clause to obtain DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
The definition supplies the carrier type for the downstream theorem that proves Fintype.card equals five and for the certificate structure that records the same cardinality. It thereby anchors the cybernetics layer of the Recognition Science framework, extending the spatial dimension D = 3 to a five-mode control alphabet and enabling formal statements about feedback systems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.