pith. sign in
module module low

IndisputableMonolith.Materials.CompositeFailureModesFromConfigDim

show as:
view Lean formalization →

The module defines CompositeFailureMode and related certificates for composite materials whose failure modes are derived from configuration dimension in the Recognition Science framework. Materials modelers would cite these objects when grounding structural analysis in RS-native units. It imports only the time quantum from Constants and supplies four sibling declarations without proofs.

claimIntroduces CompositeFailureMode as a type of material failure indexed by configuration dimension, together with compositeFailureMode_count, CompositeFailureModesCert as a certification predicate, and compositeFailureModesCert.

background

The module resides in the Materials domain and imports IndisputableMonolith.Constants, whose sole documented content is the fundamental RS time quantum (RS-native) with τ₀ = 1 tick. No J-cost, defectDist, or phi-ladder definitions appear in the supplied imports or siblings. The four sibling declarations supply the core vocabulary for failure-mode classification and counting under dimensional configuration.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the foundational objects for composite failure analysis that would feed parent theorems in the Recognition Science materials section. It anchors material models to the imported time quantum and configuration dimension, supporting the framework's derivation of physics from the single functional equation.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)