CompositeFailureModesCert
plain-language theorem explainer
The structure certifies that the enumerated set of composite failure modes has cardinality exactly five. Materials researchers in Recognition Science cite it when fixing configDim to D=5 for fiber-reinforced damage analysis. It is realized as a direct structure definition whose field is discharged by the Fintype instance derived from the five-constructor inductive type.
Claim. Let $M$ be the finite set whose elements are the five modes fiber fracture, matrix cracking, delamination, fiber pull-out, and interfacial debonding. The structure asserts that the cardinality of $M$ equals 5.
background
The module treats composite failure modes as an inductive type whose five constructors are fiberFracture, matrixCracking, delamination, fiberPullout, and interfacialDebonding. This type automatically derives DecidableEq, Repr, BEq, and Fintype, so its cardinality is computable as five. The local setting equates this count with configDim = D = 5 for fiber-reinforced composites, supplying the discrete damage channels used in Recognition Science materials modeling.
proof idea
The structure is introduced with a single field requiring Fintype.card of the inductive type to equal 5. The proof is immediate from the derived Fintype instance on a five-element enumeration; no further lemmas or tactics are required.
why it matters
The definition supplies the type of the certificate constructed in the downstream compositeFailureModesCert, which populates the field via the mode count. It anchors the materials layer by fixing the five-mode enumeration to configDim = 5, consistent with the framework's use of forced discrete dimensions. No open questions remain inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.