gridStabilityControlsCert
plain-language theorem explainer
This definition supplies a concrete certificate asserting that the finite type of grid stability controls has cardinality exactly 5. Energy systems modelers working inside Recognition Science would cite it to confirm that configDim D equals the enumerated set of inertia, primary frequency response, voltage support, demand response, and storage dispatch. The construction is a one-line wrapper that assigns the decide-proven cardinality theorem directly to the structure field.
Claim. Let $GridStabilityControlsCert$ be the structure whose sole field requires that the finite cardinality of the type of grid stability controls equals 5. The definition instantiates this structure by setting the field to the theorem establishing that cardinality.
background
The module establishes five canonical electric-grid stability controls corresponding 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). Upstream, Energy is defined as the real numbers. The sibling theorem gridStabilityControl_count proves by decision that the finite type of these controls has cardinality 5, and GridStabilityControlsCert is the structure packaging that cardinality assertion as a certificate.
proof idea
This is a one-line wrapper definition that populates the GridStabilityControlsCert structure by direct assignment of the gridStabilityControl_count theorem to the five_controls field.
why it matters
The definition certifies the count of controls in the energy-systems extension of Recognition Science, aligning the enumerated set with configDim D=5. It has no internal downstream uses. It touches the framework's application of the forcing chain (T0-T8) and RCL to practical domains beyond the core spatial dimension D=3 and phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.