CoherenceCoupling
plain-language theorem explainer
The coherence coupling structure encodes the requirement that electron-phonon coupling lies on the phi-ladder at an integer rung index, with the coupling constant positive and equal to phi to the power of the rung. Condensed matter theorists modeling room temperature superconductivity would cite this when applying the coherence quantum to Cooper pair formation. It appears as a direct structure definition carrying the positivity and quantization predicates.
Claim. A coherence coupling consists of an integer rung index $r ∈ ℤ$, a positive real coupling constant $g > 0$, and the quantization condition $g = φ^r$.
background
The module derives room-temperature superconductivity conditions from the φ-ladder energy structure. Pairing energy takes the form $E_n = E_{coh} · φ^n$ where the coherence quantum satisfies $E_{coh} = φ^{-5}$ eV, exceeding thermal energy at 300 K. The coherence condition requires the coupling constant to sit exactly on this ladder at integer rung.
proof idea
The declaration is a structure definition that directly encodes the four fields: rung index, coupling value, positivity predicate, and quantization equality. No lemmas or tactics are applied.
why it matters
This structure supplies the input type for the theorems establishing positive critical temperature from rung and positive coupling value. It implements the first step in the EN-002 hierarchy of coherence, temperature, and pressure conditions. The rung index connects to upstream anchor and integration-gap definitions that fix active edges per tick at unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.