rSCryptographicBoundCert
The cryptographic bound certificate assembles the positivity of per-bit J-cost together with the zero, additive, positivity, strict monotonicity, and doubling properties of total recovery cost into a single structure. Researchers deriving information-theoretic lower bounds on symmetric-key attacks within Recognition Science would cite it to invoke the complete set of J-cost bounds at once. The definition is assembled by direct reference to the individual theorems establishing each property.
claimLet $c = log φ > 0$ be the per-bit J-cost and let $C(n)$ be the total J-cost of recovering an $n$-bit key. The certificate asserts $c > 0$, $C(0) = 0$, $C(n+1) = C(n) + c$ for all natural $n$, $C(n) > 0$ for $n ≥ 1$, $C(n) < C(m)$ whenever $n < m$, and $C(2n) = 2 C(n)$ for all $n$.
background
The module derives a structural lower bound on the J-cost of recovering an n-bit symmetric key from the recognition substrate's σ-conservation condition. Per-bit cost equals log φ, shown positive via the logarithm positivity theorem. Total cost is defined as n times this per-bit value, with additivity following from the recursive definition over the binary search tree of 2^n candidates.
proof idea
The definition populates the fields of the bound certificate structure by assigning each required property to its corresponding theorem: positivity of per-bit cost, zero at n=0, successor additivity, positivity for positive n, strict increase, and exact doubling. It functions as a direct bundling of these results with no additional reasoning steps.
why it matters in Recognition Science
This supplies the consolidated certificate for the RS cryptographic hardness bound in Track F11. It enables the one-statement summary that per-bit J-cost equals log φ > 0, total recovery cost is additive over bits, and doubling key size exactly doubles recovery cost. The module positions it as the master certificate whose falsifier would be an attack achieving lower J-cost on any RS-compatible substrate. It rests on the J-uniqueness and phi fixed-point properties of the Recognition Science forcing chain.
scope and limits
- Does not establish computational hardness beyond the information-theoretic J-cost bound.
- Does not apply to quantum or other non-classical computation models.
- Does not quantify the gap between the bound and practical attack costs.
- Does not cover multi-key or related-key attacks.
formal statement (Lean)
89def rSCryptographicBoundCert : RSCryptographicBoundCert where
90 perBit_pos := perBitCost_pos
proof body
Definition body.
91 total_zero := totalRecoveryCost_zero
92 total_succ := totalRecoveryCost_succ
93 total_pos := @totalRecoveryCost_pos
94 total_strict_mono := @totalRecoveryCost_strict_mono
95 total_double := totalRecoveryCost_double
96
97/-- **CRYPTOGRAPHY ONE-STATEMENT.** Per-bit J-cost = `log φ > 0`; total
98recovery cost is additive over bits; doubling key size exactly doubles
99recovery cost. -/