Pith. sign in
module module moderate

IndisputableMonolith.Materials.DislocationDensityFromJCost

show as:
view Lean formalization →

Materials module that ties dislocation onset to the Recognition Science J-cost. It defines a domain cost from J, records equilibrium vanishing and nonnegativity, fixes a positive canonical threshold, and packages them in an inhabited dislocation certificate. Materials workers in the RS stack would cite the certificate and threshold facts. The file is mostly definitions plus elementary positivity lemmas from Cost.

claimIntroduce a domain cost $C$ built from the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$, with $C=0$ at equilibrium and $C\ge 0$ everywhere; a canonical threshold $\theta>0$ for dislocation onset; and a certificate packing these facts into an inhabited materials witness.

background

Recognition Science measures mismatch by the J-cost $J(x)=\frac{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. In the materials reading, lattice defects are excess recognition cost above a perfect, equilibrium configuration.

This module lives in the Materials domain. It imports Constants (RS-native units, including the time quantum $\tau_0=1$ tick) and Cost (the shared J-cost API). Domain cost specializes J to a materials domain variable; the canonical threshold is the positive level at which that cost is treated as forcing a dislocation-density response rather than elastic accommodation.

proof idea

Definition-led module, not a deep derivation. domainCost is introduced from the Cost layer; domainCost_at_equilibrium and domainCost_nonneg record the equilibrium zero and nonnegativity inherited from J. canonicalThreshold is a fixed positive scale, with canonicalThreshold_pos the positivity lemma. DislocationCert is a structure bundling those facts; cert and cert_inhabited supply a canonical inhabited instance. No heavy tactic proof: the argument is packaging and elementary inheritance from Cost.

why it matters in Recognition Science

Puts dislocation density on the same J-cost footing as other RS observables, so later materials claims can inherit T5 J-uniqueness and the RCL without re-deriving cost calculus. The graph currently lists no downstream consumers; the module is infrastructure for density-from-cost theorems still to be wired. It does not touch the eight-tick octave, $D=3$, or the alpha band, but it extends the cost core into condensed-matter language. Open follow-on: a proved map from excess domain cost above threshold to a quantitative dislocation density.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)