maintenanceStrategy_count
plain-language theorem explainer
The theorem asserts that the inductive type of maintenance strategies has finite cardinality exactly five. Operations researchers modeling configuration dimension D=5 cite this count when certifying protocol sets. The proof is a one-line decide tactic that exhausts the five constructors.
Claim. The finite set of canonical maintenance strategies has cardinality five: $|$reactive, preventive, predictive, condition-based, reliability-centered$| = 5$.
background
The module formalizes maintenance strategies as an inductive type with exactly five constructors that correspond to configDim D = 5. These cover run-to-failure, schedule-based, model-based, sensor-based, and system-criticality-based approaches. The local setting is the operations depth of Recognition Science, where discrete configuration dimensions receive explicit finite-type encodings.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card on the inductive type whose constructors are the five listed strategies.
why it matters
This cardinality supplies the five_strategies field inside the downstream maintenanceStrategiesCert definition. It anchors the operations layer to the module's configDim = 5 convention and extends the framework's discrete counting practice beyond the core T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.