totalRecoveryCost_pos
plain-language theorem explainer
For natural numbers n at least 1 the total J-cost of recovering an n-bit key is strictly positive. Researchers deriving structural lower bounds on symmetric-key attacks in Recognition Science cite this to confirm that enumeration over 2^n candidates cannot be cost-free. The proof is a one-line wrapper that unfolds the product definition and applies mul_pos to the cast of n together with the already-proved positivity of per-bit cost.
Claim. For every natural number $n$ with $ngeq 1$, the total J-cost satisfies $0 < n cdot log phi$, where $phi>1$ is the golden ratio and the product is the additive J-cost of recovering an n-bit key.
background
In this module the per-bit cost is the natural logarithm of the golden ratio, shown positive by Real.log_pos applied to one_lt_phi. The total recovery cost is defined as the real-number product of n with that per-bit value, implementing additivity of J-cost over the binary search tree of 2^n candidates. The local setting is Track F11 of the cryptographic hardness bound, which derives a structural lower bound J_min(n) = n log phi from sigma-conservation on the recognition substrate.
proof idea
The proof unfolds the definition totalRecoveryCost n := (n : Real) * perBitCost, then applies mul_pos to the positivity of the cast of n (discharged by omega from the hypothesis 1 <= n) and the upstream theorem perBitCost_pos.
why it matters
This result supplies the total_pos field inside the rSCryptographicBoundCert record that bundles all required properties for the cryptographic bound. It completes the positivity step in the derivation of J_min(n) = n log phi, linking directly to the J-cost definition used throughout the Recognition framework and to the positivity of log phi that originates in the phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.