Pith. sign in
module module moderate

IndisputableMonolith.Materials.Polymorphism3_FromJCost

show as:
view Lean formalization →

Materials module that packages a domain cost built from the RS J-cost, a positive canonical threshold, and an inhabited three-way polymorphism certificate. Materials and condensed-matter workers in the RS stack cite it when tying phase or lattice multiplicity to the unique cost functional. Content is definitional scaffolding plus elementary nonnegativity and positivity facts, not a deep existence proof.

claimIntroduce a domain cost $C$ derived from the RS cost $J(x)=(x+x^{-1})/2-1$, a canonical threshold $\theta>0$, and a certificate type for three-way polymorphism: whenever domain-cost comparisons meet the threshold, a three-phase (or three-structure) multiplicity statement is certified and inhabited.

background

Recognition Science forces a unique nonnegative cost $J$ on positive reals (T5): $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, obeying the Recognition Composition Law. The Cost import supplies that functional; Constants supplies the RS-native tick and related units.

This Materials module lifts $J$ to a domain-level cost on material configurations or phase labels. Sibling objects include the domain cost itself, its evaluation identity, nonnegativity, a canonical threshold with positivity, and a certificate record Polymorphism3Cert together with an inhabited instance. The local setting is phenomenological packaging: three-way polymorphism (three coexisting structures or phases) is expressed as a threshold condition on that domain cost rather than as a microscopic free-energy minimization.

proof idea

Definition module with light lemmas, not a long derivation. Domain cost is defined from $J$; equality-at-evaluation and nonnegativity are immediate from corresponding $J$ properties. The canonical threshold is a positive constant (positivity lemma). The polymorphism certificate is a structure bundling those inequalities; inhabitation is a one-line constructor or default instance once the threshold facts are in hand.

why it matters in Recognition Science

Places three-way material polymorphism on the same J-cost footing as the forcing chain (T5 J-uniqueness), so phase multiplicity is not an extra postulate. No downstream used-by edges are recorded yet; the module is an entry point in the Materials domain for later theorems that consume Polymorphism3Cert when linking RS cost to concrete lattice or allotrope statements. It does not itself close mass-ladder or $\alpha$-band claims; it only supplies the cost-threshold language those claims may later use.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)