IndisputableMonolith.Materials.YieldStrengthFromPhiLadder
Materials module that packages yield strength as a phi-ladder threshold on a non-negative domain cost. It defines the equilibrium cost, a positive canonical threshold, and an inhabited YieldStrengthCert record. Materials theorists in RS cite it when converting ladder rungs into macroscopic failure stresses. The argument is definitional plus elementary positivity and equilibrium lemmas, not a deep existence proof.
claimOn the Recognition $\varphi$-ladder, a domain cost $C$ is non-negative, vanishes at equilibrium, and yield strength is certified by a positive canonical threshold $T_*>0$ packaged in a $YieldStrengthCert$ record (with an inhabited witness).
background
Recognition Science places macroscopic material scales on the same $\varphi$-ladder used for particle masses: energies and stresses are yardstick times $\varphi$ to a rung offset. The Cost import supplies the J-cost infrastructure ($J(x)=(x+x^{-1})/2-1$), while Constants fixes the RS tick $\tau_0$.
This module specializes that cost language to material domains. Sibling definitions introduce a domain cost, prove it is non-negative and zero at equilibrium, and fix a positive canonical threshold. The YieldStrengthCert record bundles those facts into a single certificate that downstream materials claims can inhabit.
The local setting is therefore not continuum plasticity; it is a discrete ladder threshold that is meant to stand in for the onset of irreversible slip once the domain cost exceeds the canonical level.
proof idea
Definition-heavy module. Domain cost and the canonical threshold are introduced as defs; non-negativity, equilibrium vanishing, and positivity of the threshold are short lemmas. YieldStrengthCert is a structure packing those properties, with cert and cert_inhabited supplying a concrete witness. No long tactic scripts or external analytic estimates; the load-bearing content is the packaging of ladder cost into a reusable certificate.
why it matters in Recognition Science
Gives the Materials domain a first-class RS object for yield: strength as a positive threshold on domain cost rather than an empirical fit. It sits downstream of Constants and Cost and is intended to feed later materials claims (hardness, fracture, or alloy trends) once those modules exist. In the broader forcing picture it is an application layer on top of T5–T6 (J-uniqueness and $\varphi$), not a step in the T0–T8 chain itself. With empty used_by edges today, its role is infrastructural: close the gap between abstract ladder rungs and a certifiable macroscopic stress scale.
scope and limits
- Does not derive continuum elastoplasticity or dislocation dynamics.
- Does not predict numerical MPa values for specific alloys without further rung data.
- Does not prove uniqueness of the canonical threshold beyond the packaged positivity lemmas.
- Does not connect yield to temperature, strain rate, or grain size.
- Does not feed any recorded downstream theorem yet (used_by is empty).