totalRecoveryCost_strict_mono
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.