IndisputableMonolith.CondensedMatter.MottTransitionFromJCost
Formalizes the Mott metal-insulator transition as a threshold crossing of a domain cost built from the Recognition Science J-functional. Condensed-matter theorists working in RS units would cite the certificate and the nonnegativity/equilibrium lemmas. The module packages definitions, positivity facts, and an inhabited certificate rather than a deep derivation from microscopic Hamiltonians.
claimA domain cost $C$ is defined from the RS $J$-cost on positive scale ratios; $C$ vanishes at equilibrium and is nonnegative. A canonical positive threshold $T_\ast$ marks the Mott transition. A certificate package asserts that the transition is the crossing of $C$ through $T_\ast$, and that package is inhabited.
background
Recognition Science forces a unique nonnegative cost $J(x)=(x+x^{-1})/2-1$ on positive ratios (T5), with fixed point structure tied to $\varphi$. Condensed-matter applications treat local scale ratios and domain walls as carriers of that cost.
This module sits in the CondensedMatter layer and imports only Constants (RS time quantum and related units) and Cost (the $J$-cost API). Sibling definitions introduce a domain cost functional, record that it is zero at equilibrium and nonnegative everywhere, fix a canonical positive threshold, and wrap the transition claim in a certificate type with an explicit inhabitant.
The intended physical reading is the classical Mott picture: below threshold the system is insulating (cost-dominated localization), above it metallic (delocalized). No lattice Hamiltonian or Hubbard $U$ is axiomatized here; the cost and threshold stand in for that physics in RS-native language.
proof idea
Definition-and-certificate module. Domain cost is introduced as a def from the imported $J$-cost; equilibrium vanishing and nonnegativity are short lemmas off Cost facts. The canonical threshold is a positive constant def with a positivity proof. MottTransitionCert is a structure bundling the cost/threshold relation; cert and cert_inhabited supply a concrete instance so downstream code can assume the package without rebuilding it.
why it matters in Recognition Science
Gives the RS stack a named condensed-matter landing point for the Mott transition driven by $J$-cost rather than by an external Hubbard parameter. Downstream use is not yet wired in this graph (used_by empty), so the module is a leaf certificate: it makes the claim citable and inhabitable inside Lean without closing a larger forcing-chain step.
It touches the T5 $J$-uniqueness landmark by treating domain energetics as pure $J$-cost, and keeps constants in the RS-native style of the Constants import. Open work is linking the certificate to explicit lattice or continuum models and to measurable critical ratios on the $\varphi$-ladder.
scope and limits
- Does not derive Mott physics from a Hubbard or lattice Hamiltonian.
- Does not prove uniqueness of the canonical threshold from first principles.
- Does not connect the certificate to experimental critical doping or pressure.
- Does not feed a named parent theorem in the current dependency graph.
- Does not address dynamical or finite-temperature transition rates.