totalRecoveryCost_double
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish the positivity of perBitCost.
- Does not derive the explicit value of perBitCost.
- Does not address attacks outside the RS substrate.
- Does not bound costs under quantum computation.
Lean usage
theorem cryptography_one_statement : 0 < perBitCost ∧ (∀ n, totalRecoveryCost (n + 1) = totalRecoveryCost n + perBitCost) ∧ (∀ n, totalRecoveryCost (2 * n) = 2 * totalRecoveryCost n) := ⟨perBitCost_pos, totalRecoveryCost_succ, totalRecoveryCost_double⟩formal statement (Lean)
73theorem totalRecoveryCost_double (n : ℕ) :
74 totalRecoveryCost (2 * n) = 2 * totalRecoveryCost n := by
proof body
Term-mode proof.
75 unfold totalRecoveryCost
76 push_cast
77 ring
78
79/-! ## §4. Master certificate -/
80