cert_inhabited
plain-language theorem explainer
The result establishes existence of a certificate for the phi-ladder key-length ratios by exhibiting an explicit witness. Cryptographers modeling RS-derived security levels or checking consistency with NIST ladders would cite it to anchor the structural claims. The proof is a one-line term that applies the structure constructor to the cert definition.
Claim. There exists a certificate $C$ such that the security-level ratio $r$ satisfies $0 < r$, $1 < r$, and the 128-bit key length doubled equals the 256-bit key length.
background
The module develops cryptographic key lengths from the phi-ladder in Recognition Science, predicting rungs at $2^{phi^k}$ bits with phi-spaced log-scale security levels. KeyLengthCert is the structure requiring a positive security-level ratio, a ratio exceeding one, and exact doubling from 128-bit to 256-bit keys. The upstream result is precisely this structure definition, which encodes the concrete ratio and doubling constraints used throughout the module.
proof idea
The proof is a term-mode construction that applies the structure constructor to the cert term, directly witnessing nonemptiness of KeyLengthCert.
why it matters
This declaration closes the structural theorem in the cryptography module by confirming the certificate is inhabited, supporting the RS prediction of phi-step spacing in the log2 key-length ladder. It directly addresses the module's falsifier concerning post-quantum standards that would depart from the ladder. No downstream uses are recorded, so the result stands as a self-contained existence anchor for the phi-ladder model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.