tcAtRung_succ_ratio
plain-language theorem explainer
The critical temperature on the phi-ladder multiplies by exactly phi at each successive rung. Materials physicists building hydride superconductor models cite this to extrapolate from the MgB2 reference at rung zero toward room-temperature candidates at rung five. The proof is a direct term reduction that substitutes the power definition and closes by ring arithmetic.
Claim. $T_c(k+1) = T_c(k) · ϕ$, where $T_c(k) := T_{ref} · ϕ^k$ and $T_{ref}$ is the reference temperature at rung zero.
background
The module places candidate critical temperatures on the BCS pairing-strength phi-ladder, with each rung increase multiplying T_c by phi. The definition tcAtRung implements this as referenceTc multiplied by phi to the power k, anchoring rung zero at the observed 39 K of MgB2. This scaling follows from the self-similar fixed point phi in the Recognition Science framework.
proof idea
Unfold tcAtRung to expose the explicit power, rewrite the successor exponent via pow_succ, and reduce the resulting expression by ring.
why it matters
This supplies the one_step_ratio field inside the roomTCert certificate for the room-temperature candidate. It also feeds the adjacent-ratio and strictly-increasing theorems. In the framework it realizes the phi scaling forced at T6 of the unified forcing chain for the materials application.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.