totalRecoveryCost_double
plain-language theorem explainer
Doubling the input key length exactly doubles the total J-cost of key recovery in the RS model. Researchers deriving information-theoretic security bounds cite this to establish linear scaling of attack cost with bit length. The proof is a one-line algebraic reduction that substitutes the linear definition of total recovery cost and simplifies via ring arithmetic.
Claim. For every natural number $n$, the total J-cost of recovering a $2n$-bit key equals twice the total J-cost of recovering an $n$-bit key, where total J-cost is defined as $n$ times the per-bit J-cost.
background
The RS Cryptographic Hardness Bound module derives structural lower bounds for symmetric key recovery on the recognition substrate. The upstream definition states: Total J-cost of recovering an n-bit key (additive over bits). It is realized as totalRecoveryCost n := (n : ℝ) * perBitCost, with perBitCost equal to log φ from the J-uniqueness fixed point. The module setting is Track F11 of Plan v5, proving J_min(n) = n · log φ as the minimum information cost under σ-conservation.
proof idea
The proof unfolds the definition of totalRecoveryCost to expose multiplication by perBitCost, applies push_cast to align the natural-number scaling with reals, and invokes the ring tactic to confirm the identity 2n · c = 2 · (n · c).
why it matters
This result is assembled into the master statement cryptography_one_statement, which packages positivity, additivity over bits, and doubling. It directly supports the canonical exponential separation between key sizes in the RS framework. The module falsifier remains any demonstrated attack reducing J-cost below n · log φ per recovered bit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.