criticalTempMono
plain-language theorem explainer
Monotonicity of the critical temperature on the phi-ladder holds for every natural number rung index. Condensed matter theorists applying Recognition Science predictions to cuprates and related materials would cite this result when ordering transition temperatures by rung. The argument is a direct term reduction that unfolds the power definition and closes via the inequality 1 < phi together with positivity of powers.
Claim. For every natural number $k$, the critical temperature on the phi-ladder satisfies $T_c(k) < T_c(k+1)$, where $T_c(k) := phi^k$.
background
The module treats high-Tc superconductor transitions via phi-ladder phonon screening, with the explicit claim that T_c scales as phi^k for rung index k. The definition criticalTemp k := phi^k encodes the prediction that higher rungs produce higher transition temperatures, matching observed values such as 93 K for YBa2Cu3O7 at the appropriate rung. Upstream, the lemma one_lt_phi supplies the strict inequality 1 < phi that drives the ordering; the canonical arithmetic object and band operation supply the surrounding logical setting but are not invoked in the local argument.
proof idea
The proof is a term-mode reduction. It unfolds criticalTemp to expose the power, obtains positivity of phi^k, rewrites the successor via pow_succ, and closes with linarith on the inequality obtained by multiplying the base inequality 1 < phi by the positive power.
why it matters
The result is assigned directly into the highTcCert record, which certifies the five high-Tc families together with the monotonic T_c sequence and phonon equilibrium. It supplies the rung-ordering step required by the phi-ladder model (RS_PAT_008-010) inside the Recognition framework, where phi is the self-similar fixed point forced at T6. The proof is complete and touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.