phi_ladder_unbounded
plain-language theorem explainer
The φ-ladder of critical temperatures is unbounded above. For any positive real temperature T there exists an integer rung n such that T_c(n) > T. Researchers modeling room-temperature superconductivity cite this to show that arbitrarily high critical temperatures remain available on the ladder. The proof is a one-line wrapper that reduces the claim to the unbounded growth of powers of φ > 1.
Claim. For every real number $T > 0$ there exists an integer $n$ such that $T < T_c(n)$, where $T_c(n) := phi^n$ denotes the critical temperature on the $n$-th rung.
background
In the EN-002 module the critical temperature on rung $n$ is defined by the abbreviation $T_c_rung n := phi^n$ (normalized units). This definition sits inside the larger claim that superconductivity conditions follow from the φ-ladder energy structure with coherence quantum $E_coh = phi^{-5}$ eV. The immediate upstream fact is the lemma one_lt_phi, which establishes $1 < phi$ and thereby guarantees that integer powers of phi diverge to infinity.
proof idea
The term proof first unfolds the definition of $T_c_rung$ to replace the claim with $T < phi^n$. It then applies pow_unbounded_of_one_lt to the positive real $T$ and the fact one_lt_phi, obtaining a natural-number exponent. The final step coerces that exponent to an integer to satisfy the existential quantifier over ℤ.
why it matters
This is EN-002.6 and is invoked by the en002_certificate to close the room-temperature superconductivity derivation. It shows that the φ-ladder supplies critical temperatures at every scale once coherence is granted, directly supporting the ambient-superconductivity possibility stated in the module. No open scaffolding remains in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.