perBitCost
plain-language theorem explainer
The definition supplies the base J-cost per bit of recognition as the natural logarithm of the golden ratio. Workers on cryptographic lower bounds within Recognition Science cite this quantity when establishing additive recovery costs over n-bit keys. It is supplied directly as a constant without proof steps or reductions.
Claim. The J-cost of one bit of recognition equals $log phi$, where $phi$ is the self-similar fixed point of the recognition composition law.
background
The module derives a structural lower bound on the J-cost of symmetric key recovery under sigma-conservation on the recognition substrate. J-cost quantifies recognition effort per discrimination step, and the per-bit value follows from additivity along the binary search tree over 2^n candidates. The module imports phi from the constants library and the underlying cost function from the cost library.
proof idea
The declaration is a direct definition setting the value to the real logarithm of phi.
why it matters
This supplies the unit cost appearing in the total recovery cost definition and in the master certificate RSCryptographicBoundCert. It supports the one-statement theorem that packages positivity of the per-bit cost, additivity of total cost, and exact doubling under key size doubling. The result realizes the F11 track requirement for an exponential separation in recovery cost within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.