gridStabilityControl_count
plain-language theorem explainer
The result states that the enumerated set of grid stability controls has exactly five members, matching the configuration dimension for energy systems. Grid modelers and stability analysts would cite the count when confirming that the listed mechanisms exhaust the required controls. The proof is a direct decision on the Fintype instance automatically derived from the five-constructor inductive type.
Claim. The finite set consisting of inertia, primary frequency response, voltage support, demand response, and storage dispatch has cardinality five: $|S| = 5$.
background
The module treats grid stability controls as the five mechanisms required when the configuration dimension equals five. These comprise rotational inertia for buffering, primary frequency response for governor action, voltage support for reactive power, demand response for load adjustment, and storage dispatch for time-shifting of energy. The local setting is the direct extraction of these controls from the energy-domain configuration dimension in the Recognition Science framework.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic evaluates the cardinality by enumerating the five constructors of the inductive type and using the derived Fintype instance.
why it matters
This count populates the gridStabilityControlsCert definition that certifies the five controls. It supplies the concrete cardinality for the energy-system case of configuration dimension five, aligning with the Recognition Science derivation of D = 5 from the forcing chain. The result closes the enumeration step that feeds downstream certification of grid stability mechanisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.