pith. sign in
module module high

IndisputableMonolith.CondensedMatter.HighTcSuperconductivityStructure

show as:
view Lean formalization →

The module defines high-Tc superconductivity structures within Recognition Science and derives the implication that such structures force the lower bound 1 < phi. Condensed-matter researchers extending RS to superconductivity cite it to anchor phi-ladder consistency before treating glass transitions or room-temperature cases. The argument imports the RS time quantum and assembles the bound through four sibling lemmas on ledger-derived structures.

claimHigh-Tc superconductivity structure implies $1 < phi$.

background

The module belongs to the CondensedMatter domain and imports IndisputableMonolith.Constants, whose sole documented content is the RS time quantum τ₀ = 1 tick. Recognition Science builds all physics from the J-cost functional J(x) = (x + x^{-1})/2 - 1 together with the phi-ladder fixed point; the present module places high-Tc structures on that ladder via ledger constructions. The supplied module doc-comment states the central claim: high-Tc structure implies the lower bound 1 < phi.

proof idea

This is a definition module, no proofs. It contains four sibling declarations that introduce the ledger-derived high-Tc structure and then state the two-sided bounds on phi; each bound is a direct implication from the structure definition.

why it matters in Recognition Science

The module supplies the high-Tc structure imported by GlassTransitionStructure and RoomTemperatureSuperconductivityStructure. It therefore occupies the chain step that converts a ledger-based superconductivity definition into the phi bounds required by later condensed-matter applications of Recognition Science.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)