Pith. sign in
module module moderate

IndisputableMonolith.Materials.RS_Matl_Module_001

show as:
view Lean formalization →

Materials module 001 packages an RS domain cost for materials, its nonnegativity, a positive canonical threshold, and an inhabited certificate type. Materials-side RS claims cite the cost lemmas and the certificate bundle. Structure is mostly definitions plus short positivity and equality facts drawn from the Cost and Constants layers.

claimModule objects: a materials domain cost $C_{\mathrm{matl}}$ (from the RS cost $J$), equality and nonnegativity facts for $C_{\mathrm{matl}}$, a canonical threshold $\theta>0$, and an inhabited certificate asserting those cost and threshold properties.

background

Recognition Science measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and obeying the Recognition Composition Law. The Cost import supplies that cost layer; Constants supplies RS-native units, including the time quantum $\tau_0=1$ tick.

This materials module sits in the Materials domain of the monolith. It specializes the global cost to a domain cost $C_{\mathrm{matl}}$ and fixes a canonical threshold used as a materials decision or stability cut. Sibling names indicate equality-at-a-point, nonnegativity of the domain cost, positivity of the threshold, and a certificate record bundling those facts for later checks.

proof idea

Definition-heavy module, not a single deep theorem. Domain cost is introduced as a thin specialization of the imported Cost API; equality and nonnegativity are short transfers of Cost lemmas. Canonical threshold is a positive constant (positivity proved directly or from Constants). The certificate type packages those propositions; inhabitation is a constructor application assembling the proved facts.

why it matters in Recognition Science

Gives the Materials domain a named cost, threshold, and certificate so later materials claims can cite one bundle instead of re-deriving nonnegativity and positivity. No downstream edges are recorded yet; the natural parents are future materials theorems that need $C_{\mathrm{matl}}\ge 0$, $\theta>0$, or an RSMatl001-style cert. Ties to the framework via J-cost (T5) and RS-native constants rather than via T6–T8 geometry. Closes local scaffolding for module 001 certification only.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)