totalRecoveryCost_zero
The total J-cost of recovering a zero-bit key is zero. Researchers deriving lower bounds on symmetric-key attacks in the Recognition Science framework cite this base case to anchor the cost function before proving monotonicity and doubling properties. The proof is a one-line wrapper that unfolds the definition and simplifies the resulting arithmetic product.
claimLet totalRecoveryCost(n) be the total J-cost of recovering an n-bit key, defined as n times the per-bit J-cost. Then totalRecoveryCost(0) = 0.
background
In the RS Cryptographic Hardness Bound module the total recovery cost is defined by totalRecoveryCost(n : ℕ) : ℝ := (n : ℝ) * perBitCost, where perBitCost equals log φ and represents the canonical J-cost per discrimination on the recognition substrate. This definition implements the additive cost over the binary search tree that enumerates 2^n candidates, as required by the σ-conservation condition. The upstream result totalRecoveryCost supplies the explicit multiplicative form used throughout the module.
proof idea
The proof is a one-line wrapper that unfolds totalRecoveryCost and applies simp to reduce the product 0 * perBitCost to zero.
why it matters in Recognition Science
This zero case is referenced by rSCryptographicBoundCert to complete the certificate that bundles positivity, strict monotonicity, and doubling for the full cryptographic bound. It supplies the base of the induction chain that yields J_min(n) = n · log φ, the structural lower bound stated in the module. The result touches the open falsifier of any attack that would reduce recovery cost below this additive J-cost on an RS-compatible substrate.
scope and limits
- Does not compute the numerical value of perBitCost or log φ.
- Does not prove positivity or monotonicity for positive n.
- Does not address attacks outside the classical binary-search enumeration model.
- Does not derive the J-function or recognition composition law.
Lean usage
theorem zero_cost_anchor : totalRecoveryCost 0 = 0 := totalRecoveryCost_zeroformal statement (Lean)
52theorem totalRecoveryCost_zero : totalRecoveryCost 0 = 0 := by
proof body
One-line wrapper that applies unfold.
53 unfold totalRecoveryCost; simp
54