IndisputableMonolith.Cryptography.RSCryptographicBound
Module defines the J-cost of one bit of recognition as the canonical RS bit-cost, together with total recovery cost accumulation and a bound certificate. Researchers deriving information recovery limits in RS cryptography would cite these results. The module consists of base definitions followed by inductive lemmas on natural-number cost sums.
claimJ-cost of one bit of recognition (canonical RS bit-cost): $J_b$. Total recovery cost: totalRecoveryCost$(n) = n J_b$ for $n$ bits.
background
Recognition Science derives all physics from the J-function obeying the Recognition Composition Law. The module imports the fundamental RS time quantum τ₀ = 1 tick from Constants and cost primitives from the Cost module. It specializes these to cryptographic bit costs, defining perBitCost as the J-cost for one bit and totalRecoveryCost via recursion on bit count.
proof idea
This is a definition module with supporting lemmas. Definitions establish perBitCost and totalRecoveryCost. Lemmas prove positivity, zero and successor cases, strict monotonicity, and doubling via induction on the natural numbers.
why it matters in Recognition Science
The module supplies the bit-level cost foundation for RSCryptographicBoundCert and cryptography_one_statement. It operationalizes the J-cost into cryptographic bounds, connecting to the forcing chain steps T5-T8 for information recovery limits.
scope and limits
- Does not compute numerical values for specific key lengths.
- Does not incorporate external cryptographic assumptions beyond RS J-cost.
- Does not address multi-bit interactions beyond additive recovery cost.
- Does not extend to non-RS units or non-recognition bits.
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