phi_ladder_tc_monotone
plain-language theorem explainer
The critical temperature on the φ-ladder satisfies T_c(n+1) > T_c(n) for every integer n. Materials scientists modeling room-temperature superconductivity cite this monotonicity to select higher rungs for elevated transition temperatures. The term proof unfolds the definition T_c_rung n = φ^n, rewrites the power-addition rule, and applies the elementary inequality 1 < φ together with positivity of powers.
Claim. For every integer $n$, the critical temperature satisfies $T_c(n) < T_c(n+1)$, where $T_c(n) := φ^n$ in Recognition Science units.
background
In the EN-002 module, room-temperature superconductivity follows from the φ-ladder structure of coherence energies. The sibling definition T_c_rung n := φ^n encodes the scaling E_coh · φ^n / k_B in native units, with the coherence quantum E_coh = φ^{-5} exceeding k_B T_room. This rests on the upstream lemma one_lt_phi establishing 1 < φ and the lemma phi_ne_zero ensuring the base is nonzero.
proof idea
The proof is a one-line wrapper that unfolds T_c_rung, rewrites zpow_add_one₀ using phi_ne_zero, invokes one_lt_phi to obtain 1 < φ, establishes positivity of φ^n via zpow_pos, and concludes with lt_mul_of_one_lt_right.
why it matters
This is EN-002.5 in the room-temperature superconductivity derivation and feeds the en002_certificate that closes the full chain. It guarantees arbitrarily high critical temperatures on higher rungs, consistent with the φ fixed point in the forcing chain. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.