failureModeCount
plain-language theorem explainer
Recognition Science counts exactly five canonical failure modes for materials under cyclic loading, matching the configuration dimension D = 5 in the J-cost model. Materials researchers certifying fatigue life or crack initiation thresholds would cite this cardinality when building damage accumulation arguments. The proof reduces to a single decide tactic on the Fintype instance derived from the five enumerated constructors.
Claim. The set of canonical material failure modes has cardinality five: $ |M| = 5 $, where $M$ enumerates ductile fracture, brittle fracture, fatigue, creep, and stress corrosion cracking.
background
The module models fatigue as cyclic deposition of recognition cost J(Δσ/σ_yield), with crack initiation once the cumulative cost exceeds the canonical band J(φ). The inductive type enumerates the five modes and derives DecidableEq, Repr, BEq, and Fintype. This count is presented as the materials instance of configDim D = 5. Upstream cardinality theorems in StructuralSafetyFromJCost and InstitutionalFailureFromJCost establish the same pattern for their domains, each asserting exactly five modes.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card equality on the inductive type whose five constructors supply the Fintype instance.
why it matters
The result populates the five_modes field of fatigueFractureCert, which certifies damage thresholds under J-cost accumulation and feeds structural safety and governance certificates in sibling modules. It reinforces the framework pattern that each domain carries five failure modes tied to configuration dimension, consistent with the module's link to the Paris-Erdogan exponent m ≈ 2/φ and the broader forcing chain. The parallel theorems in engineering and governance modules close the same counting step for their respective certs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.