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