Pith. sign in
module module moderate

IndisputableMonolith.CondensedMatter.HighTcSuperconductivityStructure

show as:
view Lean formalization →

HighTcSuperconductivityStructure module shows that high-Tc superconductivity structures imply the bound 1 < phi. Condensed matter researchers applying Recognition Science to superconducting phases cite it for phi bounds. The module imports Constants and supplies the base for glass transition and room-temperature superconductivity modules.

claimHigh-Tc superconductivity structure implies the lower bound $1 < \phi$.

background

Recognition Science derives condensed matter from the J-cost equation and phi-ladder. This module resides in the CondensedMatter domain and imports IndisputableMonolith.Constants, where the fundamental RS time quantum satisfies $\tau_0 = 1$ tick.

The module introduces high-Tc superconductivity structure as a ledger object. Its doc-comment states that this structure implies the lower bound $1 < \phi$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module feeds GlassTransitionStructure and RoomTemperatureSuperconductivityStructure. It fills the step that high-Tc structure implies $1 < \phi$, connecting to T6 where phi is forced as the self-similar fixed point.

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)