gridStabilityControl_count
plain-language theorem explainer
The theorem asserts that the inductive type of grid stability controls has cardinality exactly five. Energy systems analysts working within Recognition Science would cite the result to fix the control-space dimension at five when modeling grid stability. The proof is a one-line decision procedure that evaluates the derived Fintype instance on the five-constructor inductive type.
Claim. Let $G$ be the inductive type whose constructors are inertia, primary frequency response, voltage support, demand response, and storage dispatch. Then the cardinality of $G$ equals 5.
background
The module states that five canonical electric-grid stability controls correspond to configDim D = 5: inertia (rotational buffer), primary frequency response (fast governor action), voltage support (reactive power), demand response (load-side control), and storage dispatch (temporal energy shifting). The upstream inductive definition GridStabilityControl enumerates precisely these five cases and derives DecidableEq, Repr, BEq, and Fintype instances. This supplies the finite-type structure whose cardinality is asserted by the theorem.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes the cardinality directly from the Fintype instance automatically derived from the inductive definition of GridStabilityControl.
why it matters
The result supplies the value five_controls inside the downstream definition gridStabilityControlsCert, thereby certifying the control dimension. It anchors the energy-systems layer of the Recognition Science framework by fixing configDim D = 5 for the listed controls, consistent with the module's explicit statement that these five span the required stability mechanisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.