keyLength128
plain-language theorem explainer
The definition supplies the natural number 128 as the key length for the 128-bit security level in the phi-ladder model. Researchers modeling brute-force complexity under Recognition Science cite this constant to anchor the doubling relation that reaches 256 bits. It appears in the KeyLengthCert structure and the keyLength_doubling theorem. The declaration is a direct constant assignment with no computation or lemmas.
Claim. The key length for the 128-bit security level is the natural number 128, written $k_{128} := 128$.
background
The module places cryptographic key lengths on a phi-ladder whose rungs scale by factors near phi in log2 space, matching the observed NIST progression 80 to 112 to 128 to 192 to 256. The local setting treats successive security levels as doubling in attack complexity roughly every decade, with the explicit ratio securityLevelRatio required to be positive and greater than one. This definition supplies the central rung used by the downstream KeyLengthCert structure to certify the doubling property.
proof idea
The declaration is a direct definition that assigns the literal natural number 128. No lemmas or tactics are invoked; the body is the constant itself.
why it matters
The constant is the base case for KeyLengthCert, whose fields include the doubling relation keyLength128 * 2 = keyLength256, and for the theorem keyLength_doubling that discharges the relation by unfolding both definitions and applying norm_num. It realizes the Recognition Science claim that the canonical security-level ladder has rungs at 2^(phi^k) bit keys with phi-spaced log-scale steps. The module falsifier is any post-quantum standardization whose key sizes depart significantly from this phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.