compositeFailureModesCert
plain-language theorem explainer
The definition compositeFailureModesCert supplies a concrete witness to the CompositeFailureModesCert structure by setting its five_modes field to the value of the cardinality theorem. Materials modelers working with fiber-reinforced composites would cite it to confirm that the standard damage channels satisfy the configDim requirement of five. It is assembled as a direct record construction that inherits the proof from the decide tactic in the count theorem.
Claim. Let $C$ be the finite type whose elements are the composite failure modes. The structure CompositeFailureModesCert requires that the cardinality of $C$ equals 5. The definition compositeFailureModesCert is the element of this structure obtained by assigning the field five_modes to the theorem establishing $|C| = 5$.
background
In the module on composite failure modes derived from configDim, five canonical modes are identified for fiber-reinforced composites: fiber fracture, matrix cracking, delamination, fiber pull-out, and interfacial debonding. These represent the standard damage channels. The structure CompositeFailureModesCert encodes the requirement that exactly five such modes exist, as captured by the Fintype cardinality being 5. This builds directly on the theorem compositeFailureMode_count, which establishes the cardinality via a decision procedure.
proof idea
The definition is a one-line record construction that directly assigns the five_modes field to the result of the compositeFailureMode_count theorem.
why it matters
This definition completes the certification that composite materials exhibit five failure modes aligned with the configDim parameter set to 5. It supports downstream modeling in the Recognition Science framework by providing a verified count of damage mechanisms. No immediate parent theorems are listed in the used_by relations, but it anchors the materials depth section to the dimensional forcing chain where configDim determines the number of modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.