Pith. sign in
module module moderate

IndisputableMonolith.Materials.PhaseChangeMemoryFromJCost

show as:
view Lean formalization →

Materials module that ties phase-change memory (PCM) switching to the Recognition Science J-cost. It defines a domain cost, a canonical positive threshold, and a small certificate bundle asserting that the threshold is the natural J-derived switching scale. Cite it when linking RS cost geometry to nonvolatile memory phenomenology. Content is mostly definitions and elementary positivity or evaluation lemmas, not a deep existence proof.

claimOn the RS cost $J(x)=(x+x^{-1})/2-1$, the module introduces a domain cost $C$ for PCM-like two-state media, a canonical threshold $\theta>0$ built from $J$ (and RS constants), and a certificate that $\theta$ is the natural switching scale: $C$ is nonnegative, agrees with the intended evaluation at equality cases, and the threshold package is inhabited.

background

Recognition Science forces a unique nonnegative cost $J$ on ratios (T5): $J(x)=\cosh(\log x)-1$, obeying the Recognition Composition Law. Constants are taken in RS-native units via the Constants import ($\tau_0=1$ tick, and the usual $\phi$-ladder scalings elsewhere in the monolith). The Cost import supplies the shared $J$-API used across physics and materials layers.

This module sits in the Materials domain. The modeling idea is that a phase-change bit (amorphous vs crystalline, or two metastable domains) pays a $J$-cost to leave equilibrium; switching is declared when that cost crosses a canonical threshold rather than an ad hoc materials parameter. Sibling names indicate a domain cost, its value at distinguished points, nonnegativity, a positive canonical threshold, and a PCM threshold certificate type with an inhabited instance.

proof idea

Definition-and-certificate module, not a long derivation. It packages: (1) a domain-cost definition in terms of $J$; (2) evaluation and nonnegativity facts (likely direct from $J\ge 0$ and algebraic simplification); (3) a canonical threshold constant with a positivity lemma; (4) a small certificate structure (threshold package) and a proof that the certificate type is inhabited. Expect short tactic or term proofs discharging inequalities and definitional equalities, not analytic PDE or device-level kinetics.

why it matters in Recognition Science

Gives the monolith a materials-facing hook: PCM switching thresholds expressed in the same $J$-language as the forcing chain and RS constants, instead of purely empirical activation energies. Downstream used-by edges are empty in the graph snapshot, so this is presently a leaf materials layer: it consumes Cost and Constants and exposes domainCost, canonicalThreshold, and PCMThresholdCert for later device, memory, or condensed-matter developments. It does not itself close T0–T8; it applies the already-forced $J$ to a condensed-matter motif (two-domain cost crossing a $\phi$/$J$-native scale).

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)