FeedbackControlMode
plain-language theorem explainer
The inductive type enumerates the five canonical feedback control modes tied to configDim equal to 5 in the cybernetics layer. Researchers extending Recognition Science to control systems would cite the enumeration when counting modes or building certifications. The definition is introduced directly as an inductive type that derives Fintype for automatic cardinality.
Claim. Let $M$ denote the set of feedback control modes. Then $M$ consists of five elements: proportional, integral, derivative, feedforward, and adaptive, where the first three correspond to the PID axes and the latter two close the model-based and learning channels.
background
The module defines five modes corresponding to configDim D = 5. Proportional, integral, and derivative form the PID axes; feedforward and adaptive close the model-based and learning-control channels. The local setting treats this enumeration as the basis for finite-type operations in the cybernetics depth, with zero axioms or sorrys.
proof idea
Direct inductive definition with five constructors, deriving DecidableEq, Repr, BEq, and Fintype to support downstream cardinality proofs.
why it matters
Supplies the enumeration required by the downstream theorem establishing cardinality exactly 5 and by the certification structure containing that equality. It anchors the cybernetics layer by linking configDim to control modes, consistent with dimensional derivation in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.