IndisputableMonolith.Cryptography.RSCryptographicBound
This module defines the J-cost of one bit of recognition as the canonical RS bit-cost unit. Researchers deriving cryptographic recovery bounds or information-theoretic costs in the Recognition Science framework would cite it when scaling from single-bit costs to total recovery. The module establishes this through definitions of per-bit and total costs together with lemmas on positivity, monotonicity, and doubling that follow directly from the J-function properties.
claimThe J-cost of one bit of recognition is the canonical RS bit-cost $c_{bit}$, with total recovery cost for $n$ bits given by the cumulative function $C(n)$ satisfying $C(0)=0$, $C(n+1)=C(n)+c_{bit}$, and $C(n)>0$ for $n>0$.
background
The module imports Constants, where the fundamental RS time quantum is defined as τ₀ = 1 tick, and the Cost module, which supplies the J-cost function and its algebraic properties. It introduces perBitCost as the base J-cost per recognition bit and totalRecoveryCost as the additive extension to multiple bits. These rest on the recognition composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and the positivity of J at the relevant arguments.
proof idea
This is a definition module whose argument consists of a core definition for the per-bit J-cost followed by a chain of lemmas. The lemmas establish positivity of perBitCost, zero and successor cases for totalRecoveryCost, strict monotonicity, and a doubling identity, each obtained by direct algebraic reduction using the J-function rules imported from Cost.
why it matters in Recognition Science
This module supplies the bit-level cost foundation that feeds the one-statement cryptographic bound (cryptography_one_statement) within the same module. It realizes the J-cost at the information scale, linking directly to the J-uniqueness step (T5) and the self-similar fixed point phi in the forcing chain while providing the cost yardstick for RS-native cryptographic bounds.
scope and limits
- Does not compute explicit numerical values for the bit cost in RS units.
- Does not address security reductions against concrete cryptographic attacks.
- Does not extend the cost model to multi-party or distributed recognition scenarios.
- Does not incorporate external standards such as AES or RSA bit lengths.
depends on (2)
declarations in this module (11)
-
def
perBitCost -
theorem
perBitCost_pos -
def
totalRecoveryCost -
theorem
totalRecoveryCost_zero -
theorem
totalRecoveryCost_succ -
theorem
totalRecoveryCost_pos -
theorem
totalRecoveryCost_strict_mono -
theorem
totalRecoveryCost_double -
structure
RSCryptographicBoundCert -
def
rSCryptographicBoundCert -
theorem
cryptography_one_statement