feedbackControlMode_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the modes from the forcing chain T0-T8.
- Does not invoke the Recognition Composition Law.
- Does not compute stability margins or gain values.
- Does not address physical implementation or discretization.
Lean usage
def feedbackControlModesCert : FeedbackControlModesCert where five_modes := feedbackControlMode_countformal statement (Lean)
26theorem feedbackControlMode_count :
27 Fintype.card FeedbackControlMode = 5 := by decide
proof body
28