FailureMode
The inductive definition enumerates the five canonical structural failure modes for civil engineering safety analysis under the J-cost framework. Engineers and certification protocols cite it when confirming that a structure accounts for all standard failure paths in the factor-of-safety calculation. The definition is a direct inductive enumeration that derives Fintype and equality instances to support immediate cardinality verification.
claimThe inductive type of structural failure modes consists of the five constructors yielding, buckling, fatigue, fracture, and creep.
background
In the Recognition Science treatment of structural engineering the factor of safety is the reciprocal of the working-stress to ultimate-strength ratio r, with the J-cost J(r) measuring the recognition deficit for any given margin. The module sets the RS-optimal safety factor at phi and identifies five canonical failure modes that realize configuration dimension D = 5. These modes are yielding under static overload, buckling under compression, fatigue under cyclic loading, fracture from crack growth, and creep under sustained stress.
proof idea
The declaration is a direct inductive type definition listing the five constructors, followed by automatic derivation of DecidableEq, Repr, BEq, and Fintype instances.
why it matters in Recognition Science
The definition supplies the five_failure_modes field required by StructuralSafetyCert and the exact cardinality asserted by failureModeCount. It instantiates configDim D = 5 for the engineering domain, consistent with the five-tick structure inside the eight-tick octave and the Recognition Composition Law. It also supplies the failure mode component for ProtocolFalsifiable and ProtocolSpec records in the Option A empirical protocol.
scope and limits
- Does not assign probabilities or rates to the modes.
- Does not model interactions among simultaneous modes.
- Does not incorporate material-specific parameters or environmental variables.
- Does not treat time-dependent evolution of any mode.
Lean usage
theorem failureModeCount : Fintype.card FailureMode = 5 := by decideformal statement (Lean)
28inductive FailureMode where
29 | yielding | buckling | fatigue | fracture | creep
30 deriving DecidableEq, Repr, BEq, Fintype
31