pith. sign in
module module high

IndisputableMonolith.Cryptography.KeyLengthFromPhiLadder

show as:
view Lean formalization →

This module defines cryptographic key lengths derived from the phi-ladder in Recognition Science, with security levels spaced by phi to the power 1/2 on the log base 2 scale. It supplies concrete values for 80-bit, 128-bit, and 256-bit security along with a doubling property and a certification structure. Applied cryptographers or RS modelers would cite these definitions when mapping fundamental constants to practical key sizes. The module is built from definitions and elementary lemmas with no complex proofs.

claimThe security level ratio equals $sqrt(phi)$, where $phi$ is the self-similar fixed point. Key lengths satisfy keyLength80, keyLength128, keyLength256 with the doubling relation keyLength_doubling, and the whole construction is certified by KeyLengthCert.

background

Recognition Science obtains phi as the self-similar fixed point forced by J-uniqueness in the T5-T6 steps of the unified forcing chain. The module imports the RS time quantum tau_0 = 1 tick from Constants and the J-cost machinery from Cost. It places security levels on a log_2 key-length ladder whose spacing is fixed at phi^{1/2}, consistent with the eight-tick octave periodicity.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the cryptographic layer that converts the phi-ladder into discrete security parameters. It supports downstream use of the RCL and the D=3 spatial structure by furnishing ready-to-apply key lengths. No theorems yet depend on it, but it closes the interface between abstract RS constants and applied security.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (10)