Condensed Matter Anderson Localization From Jcost Anderson Loc Cert

The certificate's actual scope

Anderson localization is the physics of electrons that stop conducting because disorder traps them. The declaration AndersonLocCert in the Recognition Science library is not a theorem about that physics. It is a small, verified structure that bundles three general facts about a cost function, and the library's own docstring says it proves nothing specific to Anderson localization. The name is a plan for where the idea was meant to go, not a result that got there.

The cost function in question is cost, a measure of the price of a recognition event, defined here as Jcost(measured / expected). The three facts the certificate bundles are: the cost is zero when the measured value equals the expected value; the cost is never negative for positive inputs; and the number phi minus 3/2 is positive. Each fact is proved in the machine-checked library of formal theorems, and together they inhabit the certificate structure. The certificate itself is nonempty, meaning those three facts are consistent and can be packaged together.

What the certificate does not do is connect those facts to a metal-insulator transition. The module defines domainCost as Jcost(m / e) without any reference to conductance, disorder, or a physical system. To make this a theorem about Anderson localization, the library would need a definition of m and e in that subject's own terms. That definition is absent. The docstring names a falsifier, empirical data outside the RS prediction band, but there is no prediction band here because there is no prediction.

The three proved facts are real and general. The cost vanishes at equilibrium, it is nonnegative, and the threshold number is positive. Those are the entire contents of the certificate. The leap from those facts to a claim about electrons in a disordered lattice is a research note, recorded in the source file, not a proved implication.

structure AndersonLocCert where
  cost_at_eq : ∀ r : ℝ, r ≠ 0 → domainCost r r = 0
  cost_nonneg : ∀ m e : ℝ, 0 < m → 0 < e → 0 ≤ domainCost m e
  threshold_pos : 0 < canonicalThreshold

theorem domainCost_at_equilibrium (r : ℝ) (h : r ≠ 0) :
    domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) :
    0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (measured expected : ℝ) : ℝ :=
  Jcost (measured / expected)

What this page does not claim

AndersonLocCert does not prove that Anderson localization occurs at any threshold. It does not predict a metal-insulator transition for any real material. It does not define what m and e mean in the context of disordered conductors.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/CondensedMatter/AndersonLocalizationFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: