keyLength_doubling
plain-language theorem explainer
The equality 128 times 2 equals 256 holds directly from the fixed definitions of the two key lengths. Cryptographers modeling security ladders under the Recognition Science φ-ladder would cite this to confirm the canonical doubling step. The proof is a one-line wrapper that unfolds the constant definitions and normalizes the arithmetic.
Claim. $128 times 2 equals 256$
background
The module constructs cryptographic key lengths from the φ-ladder of Recognition Science, where security levels follow φ-spaced ratios on a log2 scale. The constants keyLength128 and keyLength256 are defined as the natural numbers 128 and 256 respectively. This doubling relation fits the documented pattern of approximate φ-steps between recommended key sizes such as 128-bit to 256-bit.
proof idea
The proof is a one-line wrapper that unfolds the definitions of keyLength128 and keyLength256, then applies norm_num to confirm the arithmetic identity.
why it matters
This theorem supplies the key_doubling field required by the KeyLengthCert structure, which certifies the structural properties of the φ-ladder in the cryptography module. It directly supports the RS prediction that key lengths double consistently with φ-spaced security levels, closing a basic verification step in the ladder without new axioms or hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.