securityLevelRatio
plain-language theorem explainer
The definition sets the spacing factor between successive security levels on the log base two key length ladder to the square root of phi. Researchers constructing phi-ladder key lengths within Recognition Science cite this constant when mapping NIST-style recommendations to geometric progressions. It enters as a direct real square root applied to phi with no additional reduction steps.
Claim. The security level spacing on the log base two key length ladder equals $sqrt(phi)$, where phi is the self-similar fixed point of the forcing chain.
background
The module treats cryptographic key lengths as following a phi-ladder structure in which successive recommended lengths (80-bit, 112-bit, 128-bit, 192-bit, 256-bit) exhibit ratios approximating powers of phi. The local setting assumes the log2-key-length ladder has phi-spaced rungs, with the concrete prediction that the ratio of successive security levels is phi to the power one half. Phi itself is the fixed point forced by the self-similar equation in the unified forcing chain.
proof idea
This is a one-line definition that directly sets the security level ratio to the real square root of phi.
why it matters
The definition supplies the base ratio that populates the KeyLengthCert structure and enables the separate proofs that the ratio is positive and exceeds one. It realizes the phi-step spacing on the log2-key-length ladder described in the module documentation, consistent with the phi fixed point (T6) and eight-tick octave (T7) from the forcing chain. It touches the open question of whether post-quantum standardization will require key sizes that depart from this ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.