perBitCost_pos
Positivity of the per-bit J-cost log phi follows from the golden ratio exceeding unity and supplies the positive unit for RS key-recovery lower bounds. Cryptographers and RS theorists cite it to anchor the n log phi hardness statement for symmetric keys. The argument is a direct term application of the real logarithm positivity lemma to the definition of perBitCost.
claim$0 < log phi$, where $phi$ denotes the golden ratio and perBitCost is defined as the natural logarithm of $phi$.
background
In the RS Cryptographic Hardness Bound module the per-bit cost is introduced as the J-cost of one discrimination step on the recognition substrate. J-cost itself is the cost function induced by a multiplicative recognizer or observer forcing event, given explicitly by Cost.Jcost on the state. The upstream lemma one_lt_phi records the elementary inequality 1 < phi, which is the sole hypothesis needed for the logarithm to be positive. The module derives the structural lower bound J_min(n) = n log phi from sigma-conservation and additivity over a binary search tree of 2^n candidates.
proof idea
The proof is a one-line term wrapper that invokes Real.log_pos on the upstream fact one_lt_phi, directly yielding positivity of log phi which equals perBitCost by definition.
why it matters in Recognition Science
This theorem supplies the first conjunct of the cryptography_one_statement, which packages per-bit positivity together with totalRecoveryCost_succ and totalRecoveryCost_double to certify the full RS cryptographic bound. It fills the module's opening claim that J-cost per discrimination equals log phi greater than zero. In the wider framework it provides the positive bit-cost unit required for the exponential separation of key sizes, consistent with the phi-ladder and the self-similar fixed point.
scope and limits
- Does not compute a numerical value for perBitCost.
- Does not address attacks outside RS-compatible substrates.
- Does not prove uniqueness of the bit-cost unit.
- Does not bound concrete algorithmic running times.
formal statement (Lean)
44theorem perBitCost_pos : 0 < perBitCost :=
proof body
Term-mode proof.
45 Real.log_pos one_lt_phi
46
47/-! ## §2. Total J-cost of n-bit key recovery -/
48
49/-- Total J-cost of recovering an `n`-bit key (additive over bits). -/