failureModeCount
Exactly five canonical structural failure modes are enumerated for structural safety analysis under the J-cost framework. Certification procedures in engineering would cite this cardinality to fix the dimension of the failure space at five. The proof reduces to a single decide tactic that enumerates the constructors of the FailureMode inductive type.
claimThe set of structural failure modes has exactly five elements: yielding, buckling, fatigue, fracture, and creep, so that its cardinality satisfies $|FailureMode| = 5$.
background
The Structural Safety from J-Cost module expresses the factor of safety as FoS = 1/r, where r is the ratio of working stress to ultimate strength. Recognition Science identifies the optimum at FoS = phi, which minimizes the associated J-cost. The module enumerates five canonical failure modes—yielding, buckling, fatigue, fracture, and creep—corresponding to the configuration dimension D = 5 in the forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card for the inductive FailureMode type, whose five constructors yield a decidable cardinality of five.
why it matters in Recognition Science
This result populates the five_failure_modes field of the structuralSafetyCert definition. It realizes the pattern that each Recognition Science domain admits exactly five failure modes, aligning with configDim D = 5 from the T8 step of the unified forcing chain. The theorem supplies the enumeration required by downstream certification constructions in engineering and related fields.
scope and limits
- Does not derive the five modes from the J-cost equation.
- Does not prove completeness of the mode list for all possible structures.
- Does not assign J-cost values to individual modes.
- Does not model interactions or sequences of failure modes.
Lean usage
have h : Fintype.card FailureMode = 5 := failureModeCountformal statement (Lean)
32theorem failureModeCount : Fintype.card FailureMode = 5 := by decide
proof body
33