Pith. sign in
module module moderate

IndisputableMonolith.Physics.Anderson_Impurity2

show as:
view Lean formalization →

Module packaging the Anderson impurity / Kondo-temperature side of Recognition Science: a domain cost built from the RS J-cost, a canonical positive threshold, and a certificate type that the Kondo scale sits above that threshold. Condensed-matter and RS-constants readers cite it for the certified inequality. Structure is definitions plus short nonnegativity and positivity lemmas, not a long derivation.

claimOn the Anderson impurity side-channel one defines a domain cost $C$ from the RS cost $J$, a canonical threshold $\theta>0$, and a certificate asserting that the Kondo temperature scale obeys $T_K \ge \theta$ (with inhabitation of that certificate type).

background

Recognition Science measures mismatch with the unique cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law and the T5 uniqueness step. The Cost import supplies that $J$; Constants supplies the RS tick $\tau_0=1$ and the golden-ratio ladder used elsewhere for mass and coupling scales.

The Anderson impurity model is the standard single-orbital impurity coupled to a conduction bath; its low-energy physics is controlled by the Kondo temperature $T_K$. This module does not re-derive the Kondo RG. It only installs an RS-native cost on the impurity domain, a fixed positive threshold built from that cost, and a Prop-level certificate that the physical Kondo scale clears the threshold.

Sibling names indicate the local API: domainCost and its evaluation/nonnegativity facts, canonicalThreshold with positivity, and KondoTempCert / cert / cert_inhabited as the certificate bundle.

proof idea

Definition-heavy module. Domain cost is assembled from the imported $J$-cost; equality-at-a-point and nonnegativity are short algebraic or order facts. The canonical threshold is a closed-form positive quantity; positivity is a one-line arithmetic check. The Kondo certificate is a structure or Prop packaging the inequality against that threshold, with an inhabitation lemma showing the certificate type is non-empty under the module's hypotheses. No deep tactic scripts; mostly defs and thin lemmas.

why it matters in Recognition Science

Places the Anderson/Kondo scale inside the same cost-and-threshold language used for other RS physics certificates (mass ladder, coupling bands, eight-tick timing). Downstream graph is currently empty, so this module is a leaf API: it exposes KondoTempCert for later condensed-matter or constants-audit theorems rather than feeding a named parent in-tree today.

Framework contact is indirect: $J$ uniqueness (T5), the RS tick from Constants, and the general pattern of positive thresholds on $\phi$-scaled quantities. It does not itself force $D=3$, the eight-tick octave, or the $\alpha^{-1}$ band; those live upstream in the forcing chain and constants modules.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)