cryptography_one_statement
plain-language theorem explainer
The cryptography_one_statement theorem establishes that the per-bit recognition cost is positive and equal to the natural logarithm of phi, that total recovery cost increases additively with each additional bit, and that doubling the key length exactly doubles the total cost. Researchers deriving information-theoretic lower bounds on symmetric-key recovery would cite this result as the canonical RS hardness statement. The proof is a direct term that packages the positivity, successor, and doubling lemmas into a single conjunction.
Claim. Let $c = 0 < 0$ denote the per-bit J-cost. Then $0 < c$, the total J-cost $J(n)$ of recovering an $n$-bit key satisfies $J(n+1) = J(n) + c$ for all natural numbers $n$, and $J(2n) = 2J(n)$.
background
In the RS Cryptographic Hardness Bound module the per-bit J-cost is defined as the natural logarithm of the golden ratio phi. The total recovery cost for an n-bit key is n times this per-bit cost, representing the additive J-cost over a binary search tree of 2^n candidates. This builds on the Recognition Science framework where J-cost measures information discrimination cost, with phi arising as the self-similar fixed point in the forcing chain.
proof idea
The proof is a term-mode wrapper that constructs the required conjunction by directly supplying the three component results: the positivity of perBitCost from Real.log_pos one_lt_phi, the additivity under successor from unfolding the definition and ring simplification, and the doubling property similarly obtained by unfolding and algebraic cancellation.
why it matters
This declaration provides the compact one-statement form of the cryptographic bound, directly supporting the claim in the module documentation that the minimum information cost of an n-bit key recovery is n log phi. It aligns with the Recognition Science landmarks of J-uniqueness and the phi fixed point, offering a concrete falsifiable prediction for any attack on RS-compatible substrates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.