FatigueFractureCert
plain-language theorem explainer
The fatigue fracture certificate structure packages a five-mode failure classification together with a canonical J-band damage threshold. Materials researchers in the Recognition Science program cite it when certifying models of cyclic damage accumulation against the J-cost framework. The declaration is a direct structure with two fields that reuses the local five-element inductive type and the six-clause canonical certificate from the J-band module.
Claim. A fatigue-fracture certificate asserts that the failure-mode set has cardinality five and supplies a canonical J-band certificate $C$ satisfying $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(φ)>0$, $0.11<J(φ)<0.13$, and $J(1/φ²)>0$.
background
In the Recognition Science treatment of materials, fatigue arises from cyclic accumulation of recognition cost $J(Δσ/σ_yield)$. When the cumulative cost exceeds the canonical band around $J(φ)$, crack initiation occurs. The module defines five canonical failure modes (ductile fracture, brittle fracture, fatigue, creep, stress corrosion cracking) collected in the inductive type whose cardinality is asserted to be five. The upstream CanonicalCert supplies the six-clause J-band properties used as the damage threshold: matched zero at unity, reciprocity, positivity at φ, the numerical interval (0.11,0.13), and recovery positivity at $1/φ²$. The module doc states that these five modes equal configDim D=5 and predicts the Paris-Erdogan exponent $m≈2/φ≈1.24$.
proof idea
The declaration is the bare structure definition itself. Concrete instances are supplied by the downstream fatigueFractureCert definition, which populates the cardinality field via the failure-mode count lemma and the threshold field via the imported canonical certificate.
why it matters
This structure supplies the certificate type for the B9 Materials section on fatigue and fracture. It feeds the fatigueFractureCert definition that constructs the concrete instance. The five-mode count aligns with the eight-tick octave and D=3 spatial dimensions in the forcing chain, while the CanonicalCert reuses the phi-band from T5 J-uniqueness. It closes the link between J-cost accumulation and empirical failure patterns without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.