totalRecoveryCost_strict_mono
Total J-cost of n-bit key recovery increases strictly with key length. Cryptographers deriving RS-based hardness bounds cite this to confirm exponential separation between key sizes. The argument unfolds the definition of totalRecoveryCost and applies the order-preservation lemma for multiplication by a positive constant.
claimLet $n, m$ be natural numbers with $n < m$. Then $n c < m c$, where $c = perBitCost = log phi > 0$ and totalRecoveryCost$(k) := k c$.
background
The RS Cryptographic Hardness Bound module derives a structural lower bound on information cost for symmetric key recovery from sigma-conservation on the recognition substrate. totalRecoveryCost n is defined as n multiplied by perBitCost, with perBitCost established as log phi by perBitCost_pos via Real.log_pos one_lt_phi. This additivity models J-cost over the binary search tree enumerating 2^n candidates.
proof idea
Unfolds totalRecoveryCost to expose multiplication by perBitCost. Casts the hypothesis n < m to reals with exact_mod_cast. Applies mul_lt_mul_iff_of_pos_right instantiated at perBitCost_pos to obtain the strict inequality.
why it matters in Recognition Science
The result is packaged into rSCryptographicBoundCert, which collects the full certificate for the cryptographic bound in Track F11. It supplies the monotonicity clause required for the module's claim that total cost is strictly monotonic in key size and that doubling key size doubles J-cost. This aligns with J-uniqueness and the phi-ladder additivity in the forcing chain.
scope and limits
- Does not address Turing-machine computational complexity.
- Does not extend to asymmetric or quantum key recovery.
- Does not supply an upper bound on recovery cost.
- Applies only within the RS recognition substrate model.
formal statement (Lean)
64theorem totalRecoveryCost_strict_mono {n m : ℕ} (h : n < m) :
65 totalRecoveryCost n < totalRecoveryCost m := by
proof body
Tactic-mode proof.
66 unfold totalRecoveryCost
67 have h_real : (n : ℝ) < (m : ℝ) := by exact_mod_cast h
68 exact (mul_lt_mul_iff_of_pos_right perBitCost_pos).mpr h_real
69
70/-! ## §3. Doubling-key-size cost identity -/
71
72/-- Doubling the key size doubles the recovery cost. -/