RSCryptographicBoundCert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the per-bit cost from the forcing chain or J-uniqueness.
- Does not prove that any concrete attack meets the lower bound.
- Does not treat quantum or non-symmetric key-recovery scenarios.
- Does not quantify substrate-dependent constant factors.
formal statement (Lean)
81structure RSCryptographicBoundCert where
82 perBit_pos : 0 < perBitCost
83 total_zero : totalRecoveryCost 0 = 0
84 total_succ : ∀ n, totalRecoveryCost (n + 1) = totalRecoveryCost n + perBitCost
85 total_pos : ∀ {n : ℕ}, 1 ≤ n → 0 < totalRecoveryCost n
86 total_strict_mono : ∀ {n m : ℕ}, n < m → totalRecoveryCost n < totalRecoveryCost m
87 total_double : ∀ n, totalRecoveryCost (2 * n) = 2 * totalRecoveryCost n
88