CompositeFailureMode
plain-language theorem explainer
Five canonical damage channels in fiber-reinforced composites are enumerated as an inductive type whose size is fixed by the configuration dimension equaling 5. Materials modelers classifying observed degradation in composites cite this enumeration when mapping experiments to theory. The declaration is a bare inductive definition that automatically derives decidable equality and finite-type structure.
Claim. Let $F$ be the set of composite failure modes. Then $F$ is the inductive type generated by the five constructors fiber fracture, matrix cracking, delamination, fiber pull-out, and interfacial debonding, corresponding to configuration dimension $D=5$.
background
In the Recognition Science framework the configuration dimension configDim fixes the number of canonical failure modes for fiber-reinforced composites at five when $D=5$. The module presents these modes as the exhaustive list of standard damage channels: fiber fracture, matrix cracking, delamination, fiber pull-out, and interfacial debonding. No upstream results are invoked; the declaration stands as a foundational enumeration with zero axioms or sorrys.
proof idea
The declaration is the inductive definition itself, introducing exactly five constructors and deriving the instances DecidableEq, Repr, BEq, and Fintype by the deriving clause with no further proof steps required.
why it matters
This definition supplies the finite set of failure modes certified by the downstream theorem establishing cardinality five and by the structure CompositeFailureModesCert. It occupies the materials-depth slot in the Recognition Science monolith by anchoring configDim $D=5$ to these concrete modes, consistent with the dimensional constraints and eight-tick octave elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.