compositeFailureMode_count
plain-language theorem explainer
The theorem asserts that the inductive enumeration of composite failure modes has cardinality five. Materials researchers applying the Recognition Science configDim model to fiber-reinforced composites would cite this result to confirm the completeness of standard damage-channel lists. The proof is a one-line decision procedure that exhausts the finite type.
Claim. The set of composite failure modes has cardinality five: $|S| = 5$, where $S$ consists of fiber fracture, matrix cracking, delamination, fiber pull-out, and interfacial debonding.
background
The module treats composite failure modes as fixed by configDim equal to five, listing the five canonical damage channels observed in fiber-reinforced composites. The upstream inductive definition enumerates these modes explicitly and derives Fintype, DecidableEq, and related instances. This supplies the finite set whose cardinality the theorem evaluates.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype.card expression for the inductive type, which succeeds by exhaustive enumeration of its five constructors.
why it matters
The result supplies the five_modes field inside the compositeFailureModesCert definition. It realizes the five-mode count stated in the module documentation for the materials domain. In the broader framework this provides a concrete cardinality instance tied to configDim, parallel to the dimension and octave counts derived from the forcing chain, though the enumeration itself remains an explicit inductive definition rather than a consequence of the J-cost equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.