cryptography_one_statement
plain-language theorem explainer
Recognition Science derives a lower bound on the J-cost of recovering an n-bit key equal to n log φ. The statement asserts that the per-bit cost is positive, that total cost increases additively with each additional bit, and that doubling the key length exactly doubles the total cost. Researchers deriving cryptographic hardness from the recognition substrate cite this as the canonical structural bound. The proof is a term-mode wrapper that packages three prior lemmas on the cost function.
Claim. Let $c := log φ > 0$ be the J-cost of one bit of recognition. Define the total recovery cost of an n-bit key by $C(n) := n · c$. Then $0 < c$, $C(n+1) = C(n) + c$ for every natural number n, and $C(2n) = 2 · C(n)$ for every natural number n.
background
The module develops a lower bound on key-recovery cost from the Recognition Science J-cost functional equation. The per-bit cost equals the real logarithm of the golden ratio φ. The total recovery cost for an n-bit key is defined as n times the per-bit cost, making the quantity additive over bits by construction. The local theoretical setting is Track F11 of Plan v5, which derives the structural lower bound J_min(n) = n log φ from σ-conservation on the recognition substrate. The three properties packaged here are positivity, additivity under increment, and exact scaling under doubling.
proof idea
The proof is a term-mode wrapper that directly returns the triple consisting of the positivity lemma for the per-bit cost, the successor-additivity lemma, and the doubling lemma. No additional tactics or reductions are applied.
why it matters
This declaration collects the defining algebraic properties of the RS cryptographic hardness bound. It realizes the claim that the minimum information cost of n-bit key recovery is n log φ with the listed properties. The result supports derivations of exponential separation between key sizes. The falsifier for the broader claim remains a demonstrated attack that reduces the per-bit cost below log φ on an RS-compatible substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.