IndisputableMonolith.Materials.Plasticity5
Materials module defining a non-negative domain cost, a positive canonical yield threshold, and an inhabited Plasticity5 certificate bundling those facts. Materials theorists in the RS stack cite it when they need a cost-gated plasticity predicate rather than a continuum yield surface. The file is mostly definitions plus short positivity and equality lemmas; no deep forcing argument lives here.
claimThe module introduces a domain cost $C$ (built from the RS $J$-cost), proves $C \ge 0$ and an evaluation identity, fixes a canonical threshold $\theta > 0$, and packages these into an inhabited Plasticity5 certificate asserting the cost-threshold pair is well-formed for materials plasticity.
background
Recognition Science measures mismatch with the unique cost $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced at T5 of the unified chain and obeying the Recognition Composition Law. The Cost import supplies that $J$; Constants supplies the RS-native tick $\tau_0 = 1$ and the golden ratio $\varphi$ used elsewhere on the mass ladder.
In the materials layer, plastic onset is not postulated as a continuum yield surface. It is gated by a domain cost derived from $J$, compared against a canonical positive threshold. The module sits in that cost-threshold setting: define the cost on domains, record non-negativity and pointwise evaluation, fix the threshold, then wrap the pair as a certificate object for downstream materials arguments.
proof idea
Definition-heavy module, not a single theorem. Domain cost is introduced as a def from the imported $J$-cost; a one-line evaluation lemma records how it specializes at equality of arguments; non-negativity follows from the corresponding property of $J$. The canonical threshold is a positive constant (positivity is a short lemma). Plasticity5Cert is a structure bundling cost and threshold data; cert builds an instance and cert_inhabited shows the type is inhabited. No multi-step tactic proof or forcing reduction appears.
why it matters in Recognition Science
Gives the Materials domain a concrete, certificate-shaped plasticity interface tied to the RS cost rather than an external phenomenological yield criterion. Downstream used-by edges are empty in the current graph, so the module is a leaf provider: later plasticity, dislocation, or yield lemmas are expected to consume Plasticity5Cert and the non-negativity/threshold facts. It does not itself close a T0–T8 forcing step; it applies the already-forced $J$ (T5) and $\varphi$-native constants inside a materials model. Open scaffolding elsewhere in Materials can discharge against this inhabited certificate once those consumers land.
scope and limits
- Does not derive continuum elastoplasticity or dislocation dynamics.
- Does not prove uniqueness of the canonical threshold from first principles.
- Does not connect plasticity onset to the eight-tick octave or $D=3$.
- Does not compute numerical yield stresses or material-specific constants.
- Does not feed any recorded downstream theorem in the current graph.