totalRecoveryCost_succ
plain-language theorem explainer
The recurrence shows that the total J-cost to recover an (n+1)-bit key is exactly the cost for n bits plus the per-bit J-cost. Researchers establishing the exponential separation in key recovery within Recognition Science would cite this additivity result. The proof is a one-line wrapper that unfolds the total cost definition and simplifies algebraically with the ring tactic.
Claim. For every natural number $n$, the total J-cost of recovering an $(n+1)$-bit key equals the total J-cost of recovering an $n$-bit key plus the J-cost per bit of recognition.
background
The module derives a structural lower bound on the information cost of key-recovery attacks on the recognition substrate. The per-bit J-cost is defined as the natural logarithm of the golden ratio, which is the canonical cost of one discrimination step. The total recovery cost for an $n$-bit key is the product of bit length with this per-bit cost, enforcing additivity over the binary search tree of candidates.
proof idea
This is a one-line wrapper proof. It unfolds the definition of total recovery cost, casts the natural number argument to a real, and applies the ring tactic to verify the algebraic identity by distributivity.
why it matters
This supplies the successor case for the one-statement cryptography summary and populates the cryptographic bound certificate. It supports the claims that total cost is strictly monotonic in key size and doubles exactly when key size doubles. In the Recognition Science framework it contributes to the derivation of the minimum cost $n$ times log phi for enumerating $2^n$ candidates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.