Pith. sign in
module module moderate

IndisputableMonolith.Materials.CoercivityFromPhiLadder

show as:
view Lean formalization →

Packages a materials-domain cost from the RS phi-ladder and a coercivity certificate around a canonical positive threshold. Defines domainCost, proves nonnegativity, fixes canonicalThreshold > 0, and supplies an inhabited CoercivityCert. Materials or condensed-matter readers citing RS energy lower bounds use this layer. Structure is definitional plus short positivity lemmas from the Cost import.

claimOn material domains the module defines a cost $C$ built from the RS $J$-cost along the $\varphi$-ladder, a canonical threshold $\theta>0$, and a coercivity certificate asserting a lower bound of $C$ by $\theta$ (with an inhabited instance of that certificate type).

background

Recognition Science measures mismatch by the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced at T5 of the unified chain. Scales sit on the $\varphi$-ladder: successive rungs multiply by the golden ratio fixed point forced at T6. The Cost import supplies that $J$-calculus; Constants supplies the RS tick $\tau_0=1$.

This materials module lifts pointwise $J$ to a domain-level functional domainCost, then isolates a single positive scale canonicalThreshold against which coercivity is certified. Coercivity here means a quantitative lower bound: domain cost cannot fall below the threshold on the admissible class, so the configuration cannot collapse to zero recognition cost without paying a fixed ladder gap.

Sibling lemmas record evaluation at equality cases, nonnegativity of the domain cost, and positivity of the threshold, then wrap them in the structure CoercivityCert.

proof idea

Definition-first module, not a deep derivation. domainCost is introduced and related to pointwise evaluation by domainCost_at_eq; nonnegativity domainCost_nonneg follows from nonnegativity of $J$. canonicalThreshold is a closed-form positive scale on the phi-ladder; canonicalThreshold_pos is a short positivity proof. CoercivityCert packages the lower-bound claim; cert and cert_inhabited supply a concrete inhabited instance so downstream code can assume the certificate without reconstructing constants.

why it matters in Recognition Science

Places the T5/T6 cost-and-phi core into the Materials domain of the monolith: coercivity of domain energy is not an extra postulate but a certificate read off the phi-ladder gap. No downstream edges are recorded yet (used_by empty), so the module is presently a leaf API for materials arguments rather than an internal lemma factory. It is the natural hook for later claims that magnetic or structural switching barriers sit at fixed RS rungs (Berry threshold $\varphi^{-1}$, dream fraction $\varphi^{-3}$, or mass-ladder gaps), once those statements are formalized against CoercivityCert.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)