keyLength80
plain-language theorem explainer
The declaration supplies the standard 80-bit symmetric key length as the natural number 80 inside the Recognition Science cryptography module. Researchers modeling φ-spaced security ladders cite it as the base rung when constructing sequences whose successive ratios approximate powers of φ. It is introduced by a direct constant assignment with no further computation.
Claim. The standard 80-bit symmetric key length is the natural number $80$.
background
The KeyLengthFromPhiLadder module places cryptographic key lengths on a φ-ladder derived from Recognition Science. The module document states that RS predicts canonical security-level ladders with rungs at $2^{φ^k}$ bit keys and φ-spaced log-scale security levels; successive NIST lengths (80-bit to 112-bit, etc.) are shown to have ratios approximating φ^0.5, φ, and similar powers. Standard lengths such as 80 bits therefore serve as base cases for the log₂-key-length ladder that doubles approximately every decade under the inverse Moore's law for brute-force complexity.
proof idea
The declaration is a direct constant definition assigning the value 80.
why it matters
It anchors the lowest rung of the key-length sequence that the module uses to illustrate φ-step patterns in security levels. The definition supports downstream constructions such as keyLength_doubling and KeyLengthCert, which in turn realize the module's claim that the ratio pattern is approximately φ-step. It touches the open falsifier stated in the module document: any post-quantum standardization that departs significantly from the φ-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.