KeyLengthCert
plain-language theorem explainer
KeyLengthCert is the structure type collecting the positivity and strict inequality of the security-level ratio together with the doubling relation between fixed 128-bit and 256-bit keys on the φ-ladder. Researchers auditing RS-derived cryptographic standards would cite it when checking that recommended key sizes obey the predicted spacing. The declaration is a direct structure definition with no lemmas or computational reduction.
Claim. The type of certificates for the cryptographic key-length ladder is the structure whose fields assert that the security-level ratio $r = √φ$ satisfies $0 < r$ and $1 < r$, together with the equality $128 × 2 = 256$.
background
In the Recognition Science treatment of cryptography, key lengths sit on a φ-ladder whose successive security levels are spaced by factors of √φ. The upstream definitions fix keyLength128 as the natural number 128, keyLength256 as 256, and securityLevelRatio as the real number √φ, described in the module as the security level spacing on the log₂-key-length ladder. The module doc states that cryptographic security levels double in key length approximately every decade, with the RS prediction that the canonical ladder has rungs at 2^(φ^k) bit keys and ratios approximating φ-steps.
proof idea
This is a structure definition that directly packages the three required field propositions: positivity and strict inequality for the security level ratio, plus the arithmetic doubling relation between the fixed key lengths. No lemmas are applied; the declaration serves as the type whose inhabitants are later constructed in the sibling definition cert.
why it matters
This structure provides the bundled certificate type that is instantiated in the downstream definition cert and then shown to be inhabited by the theorem cert_inhabited. It fills the role of a structural theorem in the cryptography module, supporting the claim that key lengths follow the φ-ladder as predicted by the Recognition Science forcing chain (T5 J-uniqueness and T6 phi fixed point). The module doc identifies the falsifier as any NIST PQC standardization departing significantly from this structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.