feedbackControlModesCert
plain-language theorem explainer
This definition supplies a concrete certificate that exactly five feedback control modes exist in the Recognition Science cybernetics model. Researchers modeling control systems within the framework would cite it to fix the dimensionality of the feedback space at configDim D = 5. The construction is a direct one-line wrapper that populates the structure field with the pre-proven cardinality result.
Claim. Let FeedbackControlModesCert be the structure whose sole field asserts that the finite type of feedback control modes has cardinality 5. The term feedbackControlModesCert is the witness obtained by setting this field to the established count of five modes (proportional, integral, derivative, feedforward, adaptive).
background
The module defines five canonical feedback-control modes for configDim D = 5: proportional, integral, derivative, feedforward, and adaptive. The first three constitute the PID axes; feedforward and adaptive close the model-based and learning-control channels. The upstream theorem feedbackControlMode_count proves by direct decision that the finite type FeedbackControlMode has cardinality exactly 5, and the sibling structure FeedbackControlModesCert packages this cardinality as a field.
proof idea
The definition is a one-line wrapper that constructs the FeedbackControlModesCert structure by assigning the result of the feedbackControlMode_count theorem directly to its five_modes field.
why it matters
This definition completes the cybernetics depth by certifying the count of five modes, anchoring the claim that configDim D equals 5 inside the Recognition Science forcing chain. It supports the T8 step that forces three spatial dimensions and supplies the concrete cardinality needed for downstream control-theoretic arguments. The module reports zero sorry or axiom, so the certificate is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.