cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical disorder threshold into a single Anderson-localization certificate. Anyone citing the 3D Anderson transition from J-cost will point at this witness. The body is a pure structure constructor that wires three sibling lemmas; no new mathematics is proved here.
Claim. There exists a certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module treats the 3D Anderson localization–delocalization transition as a structural consequence of the Recognition Science J-cost. In RS units the critical disorder sits at $W_c\sim J(\varphi)^{-1}$ times the bandwidth energy scale (numerically $\approx 8.47,W$).
The domain cost is the local cost functional used to compare mass and energy scales on the lattice; the certificate demands that it vanish when the two arguments coincide and stay nonnegative off the diagonal. The canonical threshold is the positive real that marks the onset of localization in this cost geometry.
Upstream, nonnegativity of recognition cost is already known from ObserverForcing (cost_nonneg: every recognition event has nonnegative J-cost). The three field lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos are proved earlier in the same file.
proof idea
One-line structure construction. The three fields of AndersonLoc4Cert are filled by the preexisting lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No tactics, no new calculation.
why it matters
Gives a single named inhabitant of the Anderson-localization certificate structure, so downstream statements can assume the cost geometry is well-formed without repeating the three side conditions. The module frames this as part of the structural (0-sorry) derivation of the 3D Anderson transition from J-cost, tying the critical disorder to $J(\varphi)^{-1}$ and thereby to the T5 uniqueness of $J$ and the T6 fixed point $\varphi$. No further parent theorems are recorded in the dependency graph yet; the certificate is the local packaging step that later localization claims are expected to consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.