HighTcCert
plain-language theorem explainer
HighTcCert packages the three core predictions of the phi-ladder model for high-T_c materials: exactly five families, strictly monotonic critical temperatures along the ladder, and equilibrium phonon coupling with J-cost zero at unit argument. Materials theorists working on cuprate and related superconductors would cite this structure when verifying RS-native predictions against experiment. The declaration is a plain structure definition that directly encodes the three properties without further computation or lemmas.
Claim. A high-T_c certificate is a structure asserting that the set of high-T_c families has cardinality five, that the critical temperature satisfies $T_c(k) < T_c(k+1)$ for all natural numbers $k$, and that the J-cost of the unit phonon coupling vanishes: $J(1) = 0$.
background
The module develops the Recognition Science prediction that high-T_c superconductivity arises from phi-ladder phonon screening, with T_c scaling as phi^k on rung k. HighTcFamily enumerates the five canonical families: cuprates, iron-based, nickelates, heavy-fermion, and organic superconductors. The critical temperature is defined by criticalTemp k := phi^k, making the monotonicity condition immediate from the growth of the exponential. Jcost is the Recognition cost function imported from the Cost module, and the equilibrium condition Jcost 1 = 0 fixes the phonon coupling at the canonical point.
proof idea
The declaration is a structure definition whose fields are the three required properties. No tactics or lemmas are applied; the structure simply records the statements five_families, tc_mono, and phonon_at_equilibrium for later use in highTcCert.
why it matters
HighTcCert supplies the certificate that is instantiated by highTcCert to close the high-T_c module. It encodes the framework claim that configDim D = 5 for the five families and that the phi-ladder produces the observed monotonic rise in T_c. The construction ties directly to the RS_PAT_008-010 phonon screening predictions and the eight-tick octave structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.