RSCryptographicBoundCert
plain-language theorem explainer
The structure packages positivity of the per-bit J-cost with additivity, positivity, strict monotonicity, and exact doubling for the total recovery cost of an n-bit key. A cryptographer or complexity theorist would cite it when establishing the linear scaling of attack cost with key length in J-cost units on an RS substrate. The definition assembles these six properties directly from the definitions of per-bit cost as the natural logarithm of phi and total cost as n times that value.
Claim. Let $c = log φ > 0$ be the J-cost of one bit of recognition. Let $C(n)$ be the total J-cost of recovering an $n$-bit key. The structure certifies $C(0) = 0$, $C(n+1) = C(n) + c$ for every natural number $n$, $C(n) > 0$ for all $n ≥ 1$, strict monotonicity of $C$, and $C(2n) = 2C(n)$ for every $n$.
background
In the Recognition Science cryptographic hardness track the minimum information cost of a key-recovery attack on an n-bit symmetric key is bounded below by the σ-conservation condition on the recognition substrate. The per-bit cost is the J-cost of one discrimination step, defined as the natural logarithm of the golden ratio phi. The total recovery cost is then defined as the product of bit length n and this per-bit cost, giving an additive lower bound over the binary search tree of 2^n candidates.
proof idea
This is a structure definition that bundles six field declarations stating the required properties of the per-bit cost and total recovery cost functions. Each property follows immediately by unfolding the definitions of per-bit cost as log phi and total recovery cost as n multiplied by that value, followed by elementary real arithmetic.
why it matters
The structure supplies the certificate used to construct the main rSCryptographicBoundCert instance in the same module. It packages the structural lower bound J_min(n) = n log phi for key recovery as stated in the module's description of the RS cryptographic hardness bound. Within the framework this supports the exact doubling of J-cost when key size doubles, providing the canonical exponential separation required for Track F11.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.