highTcCert
plain-language theorem explainer
The highTcCert definition constructs the HighTcCert structure by populating its three fields with the enumerated family count, the monotonicity of critical temperature, and the canonical phonon coupling. Condensed-matter researchers modeling cuprate and iron-based superconductors would cite it to anchor RS-native predictions of T_c near 93 K on specific phi-rungs. The definition is a direct structure constructor that assigns the fields from highTcFamilyCount, criticalTempMono, and phonon_coupling_canonical.
Claim. The certificate is the structure instance asserting that exactly five high-$T_c$ families exist, that critical temperature increases strictly with phi-ladder rung index, and that phonon coupling sits at the equilibrium J-cost of zero.
background
The module treats high-$T_c$ superconductivity as a consequence of phi-ladder phonon screening. It states that the product of critical temperature and phonon lifetime approximates phi to an integer power, with the J-cost of coupling confined to the narrow canonical interval (0.11, 0.13) for all observed families. Five families (cuprates, iron-based, nickelates, heavy-fermion, organic) are identified with configuration dimension D = 5.
proof idea
The definition is a direct structure constructor. It supplies the cardinality field from highTcFamilyCount, the monotonicity field from criticalTempMono (which reduces the inequality to positivity of phi powers), and the equilibrium coupling field from phonon_coupling_canonical (which reduces to the unit J-cost identity).
why it matters
This definition terminates the high-$T_c$ module by supplying a concrete certificate that realizes the phi-ladder prediction for T_c. It connects to the Recognition Science forcing chain through J-uniqueness and the eight-tick octave, and it encodes the claim that phonon screening occurs at the canonical band. No downstream uses are recorded, leaving open its insertion into larger material-simulation theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.