pith. sign in
module module high

IndisputableMonolith.Materials.FractureMechanicsFromJCost

show as:
view Lean formalization →

The module defines fracture mechanics quantities from J-cost applied to the strain-to-surface energy ratio. Materials researchers using Recognition Science would cite these for deriving Paris-law exponents and fracture certification. It supplies fractureCost, surfaceEnergyFactor, parisLawExponent, and the FractureCert structure. The module is definitional, establishing non-negativity, positivity, and basic equalities with no complex proofs.

claimfractureCost is defined as $J(E_s / E_f)$ where $E_s$ is strain energy and $E_f$ surface energy; surfaceEnergyFactor equals $J_{ph}$; parisLawExponent is fixed at 4; FractureCert is the structure certifying fracture properties under these quantities.

background

The module imports Constants (with RS time quantum τ₀ = 1 tick) and Cost (source of J-cost). J-cost is the Recognition Science functional J(x) = (x + x^{-1})/2 - 1 that encodes the strain energy to surface energy ratio. It introduces fractureCost as the direct application of J to that ratio, surfaceEnergyFactor as the associated energy scaling, parisLawExponent as the derived power-law index, and FractureCert as the certification record. The local setting is Recognition Science applied to materials failure, extending the J-uniqueness and phi-ladder from the core framework.

proof idea

This is a definition module, no proofs. Sibling declarations establish fractureCost, surfaceEnergyFactor_eq_Jph, parisLawExponent_eq, and the inhabited FractureCert structure by direct construction and elementary positivity checks.

why it matters in Recognition Science

The module supplies the J-cost foundation for fracture mechanics inside Recognition Science, enabling FractureCert and related certification results. It fills the materials-domain step that connects the core J-uniqueness (T5) and RCL to observable crack-growth laws such as Paris' relation. No downstream uses are recorded yet, so the module remains an entry point for further material-property derivations.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)