feedbackControlMode_count
plain-language theorem explainer
The declaration fixes the number of feedback control modes at five, matching configDim equal to five. Cybernetics researchers cite the count when enumerating the canonical modes in the Recognition Science development. The proof is a one-line decision procedure that exhausts the constructors of the inductive enumeration.
Claim. The finite cardinality of the type whose elements are the five modes proportional, integral, derivative, feedforward, and adaptive equals five: $|M| = 5$ where $M$ is that type.
background
The module states that five canonical feedback-control modes arise when configDim equals five: proportional, integral, derivative, feedforward, and adaptive. The first three are the PID axes; feedforward and adaptive supply the model-based and learning-control channels. FeedbackControlMode is the inductive type with exactly these five constructors, deriving DecidableEq, Repr, BEq, and Fintype instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes the cardinality directly from the Fintype instance generated by the five-constructor inductive definition.
why it matters
The result supplies the mode count to the downstream definition feedbackControlModesCert. It anchors the cybernetics layer to dimension-five configuration, consistent with the framework's derivation of discrete structures. No open questions are indicated in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.