totalRecoveryCost_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish computational feasibility or runtime of any concrete attack.
- Does not depend on the internal structure of the cryptographic primitive beyond bit length.
- Does not address quantum or non-classical computational models.
- Does not supply matching upper bounds on recovery cost.
formal statement (Lean)
59theorem totalRecoveryCost_pos {n : ℕ} (h : 1 ≤ n) : 0 < totalRecoveryCost n := by
proof body
Term-mode proof.
60 unfold totalRecoveryCost
61 exact mul_pos (by exact_mod_cast (by omega : 0 < n)) perBitCost_pos
62
63/-- Total cost is strictly monotonic in key size. -/