pith. sign in
module module high

IndisputableMonolith.Materials.FatigueFractureMechanicsFromJCost

show as:
view Lean formalization →

The module certifies fatigue and fracture mechanics as consequences of the J-cost functional equation in materials. Researchers deriving failure criteria from Recognition Science would cite it for the materials domain slot. It applies the reusable six-clause J-cost-on-ratio template imported from CanonicalJBand to establish matched-zero and nonnegativity.

claimFailureMode enumerates material failure types; FatigueFractureCert asserts $J(1)=0$ and $J(x)≥0$ for $x>0$, where $J(x)=(x+x^{-1})/2-1$, via the six-clause template.

background

The module sits inside the master cert chain for B-tier domain openings under Plan v7. It imports the CanonicalJBand template, whose doc states: 'The six-clause J-cost-on-ratio template is used across the master cert chain... Each domain cert proves: 1. matched-zero: J(1)=0 2. nonneg: J(x)≥0 for x>0'. Sibling declarations introduce FailureMode as the classification of failure types and fatigueFractureCert as the domain-specific instance of the template.

proof idea

This is a definition module, no proofs. It declares the FailureMode type and failureModeCount, then instantiates the imported CanonicalJBand template to produce FatigueFractureCert.

why it matters in Recognition Science

The module supplies the materials entry in the Plan v7 domain certs and feeds the master cert chain. It extends the CanonicalJBand template to fatigue and fracture, ensuring the J-cost band (matched-zero and nonnegativity) holds for defectDist in this domain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)