totalRecoveryCost_zero
plain-language theorem explainer
The base case establishes that the total J-cost of recovering a zero-bit key is zero. Cryptographers deriving RS lower bounds on key recovery cite this to anchor induction over bit length. The proof is a one-line wrapper that unfolds the additive definition of total J-cost and simplifies.
Claim. The total J-cost of recovering a 0-bit key equals zero: $J_0(0) = 0$.
background
The RS Cryptographic Hardness Bound module derives structural lower bounds on information cost for symmetric-key recovery using J-cost units. totalRecoveryCost(n) is defined as the additive total J-cost over n bits: totalRecoveryCost(n) := n · perBitCost, where perBitCost is the J-cost per discrimination (log φ in RS units). The upstream definition states: Total J-cost of recovering an n-bit key (additive over bits).
proof idea
One-line wrapper that unfolds totalRecoveryCost and applies simp.
why it matters
This zero case is referenced directly in rSCryptographicBoundCert as total_zero to assemble the full bound certificate. It anchors the derivation of J_min(n) = n · log φ and the monotonicity claims listed in the module status. It closes the base of the additive structure required for the exponential separation in the cryptographic hardness track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.