cert
plain-language theorem explainer
This definition assembles a KeyLengthCert by supplying three properties on the security level ratio and key lengths derived from the phi-ladder. Cryptographers working with Recognition Science predictions for symmetric key sizes would cite it to certify the doubling relation and ratio bounds. The construction is a direct field assignment from three sibling theorems that establish positivity, the strict inequality above one, and the exact doubling.
Claim. Let $r$ be the security-level ratio on the phi-ladder. The certificate asserts $0 < r$, $1 < r$, and $k_{128} = 2 k_{256}$ where $k_n$ denotes the recommended bit length for security level $n$.
background
The module models cryptographic key lengths via the phi-ladder, with rungs at powers of two spaced by phi factors. SecurityLevelRatio is defined as the square root of phi, yielding the approximate step between successive NIST-style key lengths (80, 112, 128, 192, 256 bits). KeyLengthCert is the structure that packages the three required properties: positivity of the ratio, the ratio exceeding one, and the exact doubling from 128-bit to 256-bit keys.
proof idea
The definition is a one-line wrapper that constructs the KeyLengthCert record by assigning the three fields to the theorems securityLevelRatio_pos, securityLevelRatio_gt_one, and keyLength_doubling. Those theorems unfold the ratio and length definitions then apply norm_num together with the positivity and ordering properties of the square root and phi.
why it matters
The certificate supplies the concrete object required by the structural theorem in the cryptography module, anchoring the phi-ladder prediction that key lengths double at phi-spaced intervals. It directly supports the module's claim that recommended sizes follow 2^(phi^k) scaling and supplies the falsifier test against future NIST PQC standards that deviate from this pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.