high_tc_superconductivity_from_ledger
plain-language theorem explainer
The declaration defines the high-Tc superconductivity ledger condition as the requirement that the self-similar fixed point satisfies 1 < phi < 2. Condensed matter researchers modeling superconductivity through Recognition Science cite this when connecting structural constraints to the phi-ladder and mass formula. It is introduced as a direct definition with no proof obligations or external hypotheses.
Claim. High-temperature superconductivity holds from the ledger precisely when the self-similar fixed point satisfies $1 < phi < 2$.
background
Recognition Science forces the self-similar fixed point phi at T6 of the unified forcing chain as the unique positive solution to the fixed-point equation induced by the J-cost function. The CondensedMatter.HighTcSuperconductivityStructure module encodes high-Tc structural input by binding it to bounds on this phi, consistent with the Recognition Composition Law and the eight-tick octave. The upstream Constants module supplies the definition of phi together with the supporting inequalities used in sibling results.
proof idea
The declaration is a definition that directly equates the proposition to the conjunction of the two strict inequalities on phi. No lemmas or tactics are applied; the body is the literal interval condition.
why it matters
This supplies the core proposition referenced by the glass transition ledger condition, the high-Tc superconductivity structure theorem, and the room-temperature superconductivity derivations that extract the separate bounds. It embeds the T6 phi-forcing step into condensed-matter applications, ensuring alignment with the phi-ladder mass formula and the alpha inverse band. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.