GridStabilityControlsCert
plain-language theorem explainer
The structure certifies that the inductive type of grid stability controls has cardinality exactly five. Energy systems modelers cite it to fix the control-space dimension at configDim D equals five. It is realized as a one-field structure whose field records the Fintype cardinality equality for the enumerated controls.
Claim. Let $G$ be the inductive type whose five constructors are inertia, primary frequency response, voltage support, demand response and storage dispatch. The structure is the record whose sole field asserts that the cardinality of $G$ equals five.
background
The module establishes the local setting for energy systems depth by equating five canonical grid controls to configDim D equals five. These controls are inertia (rotational buffer), primary frequency response (fast governor response), voltage support (reactive power), demand response (load-side control) and storage dispatch (temporal energy shifting).
proof idea
The declaration is a structure definition with one field. The field directly records the statement that Fintype.card of the grid stability control type equals five. No lemmas or tactics are applied.
why it matters
The structure is instantiated by the downstream definition gridStabilityControlsCert. It supports the framework treatment of energy systems by fixing the control count at five, matching the module statement on the five physical aspects. It aligns with the configDim D equals five landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.