keyLength256
plain-language theorem explainer
The definition sets the 256-bit cryptographic key length to the natural number 256. Researchers constructing RS-derived security ladders cite this constant when certifying doubling relations between successive NIST levels. It is introduced as a direct constant definition with no computation or lemmas required.
Claim. Let $k_{256}$ denote the recommended key length in bits for the 256-bit security level. Then $k_{256} = 256$.
background
The module models cryptographic security levels with key lengths whose successive ratios approximate powers of the golden ratio on the log scale, as stated in the module documentation: the ratio of successive recommended key lengths follows approximately φ^0.5 per NIST security level, with concrete examples 128 → 192 at ratio 1.50 ≈ φ and 192 → 256 at ratio 1.33 ≈ φ^0.6. The RS prediction asserts that the canonical ladder has rungs at 2^(φ^k) bit keys. This definition supplies the uppermost rung at 256 bits, consistent with the structural claim of zero sorry and zero axiom in the module.
proof idea
The declaration is a direct definition that assigns the constant 256 to the 256-bit key length. No lemmas or tactics are invoked; the value is supplied verbatim for unfolding in sibling declarations.
why it matters
This constant supplies the top rung of the key-length ladder and is referenced inside the KeyLengthCert structure to certify the doubling relation keyLength128 * 2 = keyLength256. It realizes the module's claim that cryptographic security levels follow the φ-ladder structure, directly supporting the Recognition Science prediction of φ-spaced log-scale security levels. The sibling theorem keyLength_doubling depends on unfolding this definition to verify the doubling property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.