pith. machine review for the scientific record. sign in
def definition def or abbrev high

totalRecoveryCost

show as:
view Lean formalization →

Recognition Science models the total J-cost of recovering an n-bit symmetric key as n scaled by the per-bit discrimination cost. Cryptographers bounding hardness on RS substrates cite this scaling when deriving exponential separation between key lengths. The definition is a direct multiplicative construction that inherits additivity and strict monotonicity for all downstream theorems in the module.

claimThe total J-cost of recovering an $n$-bit key equals $n$ times the per-bit J-cost, i.e., $n · log φ$ where $log φ$ is the canonical recognition cost of one discrimination.

background

The RS Cryptographic Hardness Bound module derives a structural lower bound on key-recovery attacks using σ-conservation on the recognition substrate. The minimum cost satisfies J_min(n) = n · log φ, obtained by enumerating 2^n candidates at log φ J-cost per discrimination with additivity over the binary search tree. perBitCost is defined as Real.log phi and supplies the canonical RS bit-cost (J-cost of one bit of recognition).

proof idea

Direct definition that casts n to ℝ and multiplies by perBitCost. No lemmas or tactics are invoked beyond the upstream definition of perBitCost.

why it matters in Recognition Science

This supplies the total-cost function required by the master certificate RSCryptographicBoundCert and the one-statement theorem cryptography_one_statement. It realizes the module claim that recovery cost is additive over bits and doubles exactly when key size doubles, consistent with the J-cost accounting and phi-ladder structure of the Recognition framework. It touches the open falsifier of an attack achieving cost below n · log φ per recovered bit.

scope and limits

formal statement (Lean)

  50def totalRecoveryCost (n : ℕ) : ℝ := (n : ℝ) * perBitCost

proof body

Definition body.

  51

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.