cert
plain-language theorem explainer
Canonical inhabitant of the Anderson-localization certificate: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Condensed-matter readers of the RS metal-insulator band cite this pack. It is a pure structure assembly wiring three already-proved lemmas; no new algebra.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical Anderson threshold is strictly positive.
background
The module treats the disorder-driven metal-insulator (Anderson) transition as a threshold on a J-cost of the conductance ratio. In Recognition Science the unique nonnegative cost compatible with the Recognition Composition Law is $J(x)=(x+x^{-1})/2-1$, minimized at equilibrium $x=1$.
Here domainCost is that cost evaluated on a pair of positive scale parameters (mobility edge vs Fermi level, or analogous ratio). Equilibrium means the two arguments coincide, so the ratio is 1 and $J=0$. The canonical threshold is the positive RS scale at which localization is predicted (tied to $J(\varphi)$ in the module narrative).
AndersonLocCert is the three-field structure that packages exactly those structural facts: diagonal vanishing, nonnegativity, and threshold positivity. Upstream, nonnegativity of recognition cost is the standard $J\ge 0$ fact from ObserverForcing.
proof idea
Definitional structure inhabitant, not a tactic proof. The three fields are filled by name:
- diagonal vanishing from
domainCost_at_equilibrium; - nonnegativity from
domainCost_nonneg(itself resting on $J$-cost nonnegativity); - threshold positivity from
canonicalThreshold_pos. No further rewriting or case analysis.
why it matters
Gives a single named certificate that the Anderson-from-J-cost development is structurally well-posed: cost geometry is a true cost (zero only at equilibrium, nonnegative) and the predicted threshold sits above zero. The module presents this as a structural theorem (zero sorry, zero axiom) for the disorder-driven transition at $J$-cost equal to $J(\varphi)$ on the conductance ratio.
No downstream dependents are recorded yet; the sibling cert_inhabited and any later condensed-matter corollaries are the natural consumers. Framework landmarks in play are T5 $J$-uniqueness and the golden-ratio fixed point that sets the numerical band. Empirical data outside the RS prediction band is the stated structural falsifier for the surrounding claim, not for this packing itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.