undercoolingThreshold
plain-language theorem explainer
UndercoolingThreshold assigns to each natural number k the real value phi raised to k. Crystallographers applying the Recognition Science phi-ladder to Burton-Cabrera-Frank growth models cite this when deriving the Walton scaling for successive crystal habits. The definition is a direct power expression that supplies the base for the adjacent-habit ratio.
Claim. The critical undercooling threshold for the k-th crystal habit is given by $phi^k$, where $phi$ is the golden ratio fixed point.
background
The module Crystal Growth from Phi-Ladder models crystal growth rate via the Burton-Cabrera-Frank relation v proportional to exp(-E_step/kT). Critical undercooling Delta T for each habit follows the phi-ladder, with five canonical habits (cubic through trigonal) corresponding to configDim D=5. The module states that adjacent critical undercooling ratios equal phi approximately 1.618 and match the empirical Walton relation where thresholds scale as phi^n.
proof idea
Direct definition as phi to the power k with no lemmas or tactics applied.
why it matters
This definition supplies the phi-ladder scaling used by CrystalGrowthCert, whose phi_ratio field asserts that undercoolingThreshold(k+1) divided by undercoolingThreshold(k) equals phi for every k. It translates the T6 self-similar fixed point into crystallography and supports the five-habit certification. The downstream undercoolingRatio theorem unfolds the definition to prove the ratio identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.