securityLevelRatio_gt_one
plain-language theorem explainer
The theorem shows that the security-level spacing ratio on the log base two key-length ladder exceeds one. Researchers building RS-derived cryptographic ladders cite it to confirm each successive security level is strictly larger than the prior. The proof is a term-mode reduction that unfolds the ratio definition and applies square-root monotonicity to the known inequality one less than phi.
Claim. Let $phi$ denote the golden ratio. The security-level spacing ratio on the log base two key-length ladder satisfies $1 < sqrt(phi)$.
background
The module constructs cryptographic key lengths from the phi-ladder. securityLevelRatio is defined as the square root of phi and represents the multiplicative spacing between successive recommended key lengths. Upstream one_lt_phi establishes that phi exceeds one, a basic property of the golden ratio obtained from its quadratic minimal polynomial or direct numerical comparison.
proof idea
The term proof unfolds securityLevelRatio to Real.sqrt phi. It rewrites the constant one on the left as Real.sqrt one, then applies Real.sqrt_lt_sqrt to the pair of inequalities zero less than one and one less than phi supplied by one_lt_phi.
why it matters
This result supplies the ratio_gt_one field inside the KeyLengthCert record. It supports the RS claim that key lengths follow a phi-spaced ladder, consistent with the self-similar fixed point and eight-tick octave in the forcing chain. The module doc notes that post-quantum standardization departing from this structure would falsify the prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.