AndersonLoc4Cert
plain-language theorem explainer
Certificate bundle for the 3D Anderson localization transition derived from J-cost: diagonal vanishing of domain cost, nonnegativity for positive arguments, and a strictly positive canonical threshold. Cited by anyone invoking the structural W_c ~ J(φ)^{-1} × bandwidth claim. Pure structure definition; proofs live in the field witnesses.
Claim. A certificate for the 3D Anderson localization transition from $J$-cost is a triple of facts: (i) domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ whenever $r\neq 0$; (ii) domain cost is nonnegative for positive mass and energy, $0<m$, $0<e$ $\Rightarrow$ $0\le\mathrm{domainCost}(m,e)$; (iii) the canonical threshold is strictly positive.
background
The module treats the 3D Anderson localization–delocalization transition as a structural consequence of Recognition Science J-cost. Disorder criticality is placed at $W_c\sim J(\varphi)^{-1}$ times the bandwidth energy scale (numerically about $8.47$ in the stated units). Status is structural: zero sorry, zero axiom.
Domain cost is the module-local cost functional on mass/energy pairs built from the RS cost $J$. The upstream nonnegativity theorem states that the cost of any recognition event is nonnegative, via $J$-cost nonnegativity on positive states. The canonical threshold is the positive scale against which disorder strength is compared for the localization edge.
This structure does not compute the transition; it packages the three algebraic side-conditions the later certificate and inhabitance proofs must discharge.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the downstream cert definition, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed interface for the module’s structural Anderson-localization theorem from J-cost. Downstream, cert assembles a concrete inhabitant and cert_inhabited records Nonempty of the certificate type, closing the zero-sorry structural claim.
In the RS forcing picture the cost side leans on T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and nonnegativity of recognition cost; the threshold side encodes the localization edge at $W=J(\varphi)^{-1}$ times bandwidth. The structure is the hinge between those cost lemmas and the physics-facing certificate, without yet asserting the numerical $8.47$ factor or continuum spectral theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.