totalRecoveryCost_succ
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that the per-bit cost is positive.
- Does not extend the equality to real-valued key lengths.
- Does not incorporate specific attack algorithms or quantum effects.
- Does not derive the value of the golden ratio or substrate properties.
Lean usage
theorem example (n : ℕ) : totalRecoveryCost (n + 1) = totalRecoveryCost n + perBitCost := totalRecoveryCost_succ nformal statement (Lean)
55theorem totalRecoveryCost_succ (n : ℕ) :
56 totalRecoveryCost (n + 1) = totalRecoveryCost n + perBitCost := by
proof body
One-line wrapper that applies unfold.
57 unfold totalRecoveryCost; push_cast; ring
58