cert
plain-language theorem explainer
Packages the three positivity and vanishing properties of the Anderson-impurity domain cost into a single Kondo-temperature certificate. Anyone citing the RS Kondo scale T_K = D_0 exp(-1/J(φ)) uses this bundle as the structural witness. Construction is a direct record assembly from three already-proved sibling lemmas.
Claim. There exists a certificate recording that the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), is nonnegative for positive arguments, and that the canonical Kondo threshold is strictly positive.
background
The module derives the Kondo temperature from the Recognition Science J-cost. In the standard formula $T_K = D_0\exp(-1/(J\rho))$, RS identifies the dimensionless coupling with the forced cost value $J(\varphi)\approx 0.118$ at the recognition transition, giving $T_K\sim D_0 e^{-8.47}$ (order a few kelvin for $D_0\sim 10^4,\mathrm{K}$).
The domain cost is the local cost functional on the impurity model; the certificate structure KondoTempCert packages three elementary facts about it: diagonal vanishing, nonnegativity for positive mass/energy arguments, and positivity of the canonical threshold. Upstream, nonnegativity of recognition-event cost follows from nonnegativity of the J-cost on positive reals (ObserverForcing).
proof idea
One-line record construction. The three fields of the certificate structure are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity), and canonicalThreshold_pos (threshold positivity). No further reasoning is required.
why it matters
Gives a single inhabited certificate that the structural hypotheses needed for the RS Kondo-temperature claim hold. The module is marked structural (0 sorry, 0 axiom) and ties the condensed-matter Kondo scale to the forced J-cost at $\varphi$ (T5/T6 of the forcing chain). With no downstream dependents yet, this is the local witness object that later physics lemmas can assume rather than re-proving the three cost facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.