securityLevelRatio_pos
plain-language theorem explainer
The theorem establishes that the security level ratio, defined as the square root of phi, is strictly positive. Researchers modeling cryptographic key lengths on the phi-ladder cite this result to confirm the multiplicative spacing exceeds zero. The proof is a one-line wrapper that unfolds the definition and applies the square-root positivity lemma to the known positivity of phi.
Claim. $0 < sqrt(phi)$ where $phi$ is the golden ratio fixed point of the Recognition Science forcing chain.
background
The module develops cryptographic key lengths from the phi-ladder in Recognition Science. Successive recommended key lengths follow ratios approximating powers of phi, with the security level ratio introduced as the square root of phi to quantify spacing on the log base 2 key-length ladder. The upstream definition states: Security level spacing on log₂-key-length ladder: φ^(1/2), given explicitly as the noncomputable definition securityLevelRatio := Real.sqrt phi. This sits inside the broader RS prediction that the canonical security-level ladder has rungs at 2^(φ^k) bit keys.
proof idea
one-line wrapper that unfolds securityLevelRatio and applies Real.sqrt_pos.mpr to phi_pos.
why it matters
This positivity result supplies the ratio_pos field to the KeyLengthCert record that certifies the phi-ladder predictions for key lengths such as 80, 128, and 256 bits. It supports the structural theorem of the cryptography module by confirming the ratio exceeds zero, consistent with the phi fixed point from the unified forcing chain. The module doc flags post-quantum cryptography standardization as a falsifier if key sizes depart significantly from the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.