phonon_coupling_canonical
plain-language theorem explainer
The declaration fixes the J-cost at zero for unit argument, which sets the equilibrium point for phonon coupling in the phi-ladder model of high-Tc transitions. Materials theorists modeling cuprate or iron-based superconductors would cite it to anchor the canonical band condition where screening triggers superconductivity. The proof is a direct one-line wrapper that invokes the unit lemma for Jcost.
Claim. The J-cost function satisfies $J(1)=0$, where $J(x)=(x-1)^2/(2x)$.
background
The module treats high-Tc superconductivity via phi-ladder phonon screening, with Tc predictions tied to rung index k and J-cost of the coupling scale. J-cost quantifies the defect at scale x; the upstream lemma Jcost_unit0 states Jcost 1 = 0 by simplification of the squared-ratio expression. The local setting requires five canonical families (configDim D=5) and places the canonical band at J(phi) in (0.11,0.13) for known materials.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_unit0 from the Cost module.
why it matters
This supplies the phonon_at_equilibrium field inside the HighTcCert definition, which records the five-family count and critical-temperature monotonicity. It closes the equilibrium anchor for the phi-ladder superconductivity model and aligns with the Recognition Science requirement that J-cost vanish at the unit scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.