feedbackControlMode_count
plain-language theorem explainer
The theorem establishes that the inductive type of feedback control modes has cardinality exactly five. Cybernetics researchers cite the count when fixing the number of canonical modes to configDim D equals five. The proof is a one-line decision procedure that enumerates the five constructors of the inductive type.
Claim. The finite type of feedback control modes has cardinality five: $ |FeedbackControlMode| = 5 $.
background
The module defines five canonical feedback-control modes tied to configDim D = 5: proportional, integral, derivative, feedforward, and adaptive. The first three form the PID axes; feedforward and adaptive close the model-based and learning-control channels. The inductive type FeedbackControlMode enumerates these five cases and derives Fintype, DecidableEq, Repr, and BEq.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality Fintype.card FeedbackControlMode = 5. The tactic succeeds because the inductive definition supplies exactly five constructors and the derived Fintype instance computes the cardinality directly.
why it matters
This supplies the five_modes field inside feedbackControlModesCert. It instantiates the framework claim that configDim D = 5 fixes the number of feedback channels in the cybernetics layer. The module states Lean status is zero sorry and zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.