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