failureModeCount
plain-language theorem explainer
The theorem states that the inductive type of structural failure modes has cardinality five. Engineers applying the J-cost model to structural safety certification cite this result to confirm the enumeration of yielding, buckling, fatigue, fracture and creep. The proof is a one-line decision procedure on the Fintype instance derived from the inductive definition.
Claim. The finite type of structural failure modes has cardinality five: $|$yielding, buckling, fatigue, fracture, creep$| = 5$.
background
The module interprets the factor of safety via the J-cost on the working-stress to ultimate-strength ratio, with the RS-optimal value phi. It introduces the inductive type FailureMode whose constructors are yielding, buckling, fatigue, fracture, creep and which derives DecidableEq, Repr, BEq and Fintype. The module doc states that these five modes equal configDim D = 5. Parallel failureModeCount theorems exist in the governance and materials modules, each asserting cardinality five for their own FailureMode types.
proof idea
One-line wrapper that applies the decide tactic to the Fintype.card equality, using the Fintype instance automatically derived from the inductive type and its DecidableEq instance.
why it matters
The result supplies the five_failure_modes field inside structuralSafetyCert. It parallels the identically named theorems in InstitutionalFailureFromJCost and FatigueFractureMechanicsFromJCost, each feeding their respective cert definitions. The pattern confirms configDim D = 5 across domains, consistent with the Recognition Science claim that five modes appear in multiple engineering and governance settings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.