IndisputableMonolith.Cryptography.RSCryptographicBound

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# RS Cryptographic Hardness Bound (Track F11 of Plan v5)
   7
   8## Status: THEOREM (real lower-bound derivation)
   9
  10The minimum information cost (in J-cost units) of a key-recovery attack
  11on an `n`-bit symmetric key is bounded below by the σ-conservation
  12condition on the recognition substrate. We derive the structural
  13lower bound `J_min(n) = n · log φ`: `2^n` candidates and `log φ`
  14J-cost per discrimination, additive over a binary search tree.
  15
  16## What we prove
  17
  18* J-cost per discrimination = `log φ > 0` (canonical RS bit-cost).
  19* Total cost to enumerate `2^n` candidates = `n · log φ` (additivity
  20  on the binary search tree).
  21* Total cost is strictly monotonic in key size.
  22* Doubling key size doubles the J-cost (canonical exponential
  23  separation).
  24
  25## Falsifier
  26
  27A demonstrated attack reducing the J-cost of an n-bit key recovery
  28below `n · log φ` per recovered bit on any RS-compatible substrate.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Cryptography
  33namespace RSCryptographicBound
  34
  35open Constants
  36
  37noncomputable section
  38
  39/-! ## §1. Per-bit J-cost -/
  40
  41/-- The J-cost of one bit of recognition (canonical RS bit-cost). -/
  42def perBitCost : ℝ := Real.log phi
  43
  44theorem perBitCost_pos : 0 < perBitCost :=
  45  Real.log_pos one_lt_phi
  46
  47/-! ## §2. Total J-cost of n-bit key recovery -/
  48
  49/-- Total J-cost of recovering an `n`-bit key (additive over bits). -/
  50def totalRecoveryCost (n : ℕ) : ℝ := (n : ℝ) * perBitCost
  51
  52theorem totalRecoveryCost_zero : totalRecoveryCost 0 = 0 := by
  53  unfold totalRecoveryCost; simp
  54
  55theorem totalRecoveryCost_succ (n : ℕ) :
  56    totalRecoveryCost (n + 1) = totalRecoveryCost n + perBitCost := by
  57  unfold totalRecoveryCost; push_cast; ring
  58
  59theorem totalRecoveryCost_pos {n : ℕ} (h : 1 ≤ n) : 0 < totalRecoveryCost n := by
  60  unfold totalRecoveryCost
  61  exact mul_pos (by exact_mod_cast (by omega : 0 < n)) perBitCost_pos
  62
  63/-- Total cost is strictly monotonic in key size. -/
  64theorem totalRecoveryCost_strict_mono {n m : ℕ} (h : n < m) :
  65    totalRecoveryCost n < totalRecoveryCost m := by
  66  unfold totalRecoveryCost
  67  have h_real : (n : ℝ) < (m : ℝ) := by exact_mod_cast h
  68  exact (mul_lt_mul_iff_of_pos_right perBitCost_pos).mpr h_real
  69
  70/-! ## §3. Doubling-key-size cost identity -/
  71
  72/-- Doubling the key size doubles the recovery cost. -/
  73theorem totalRecoveryCost_double (n : ℕ) :
  74    totalRecoveryCost (2 * n) = 2 * totalRecoveryCost n := by
  75  unfold totalRecoveryCost
  76  push_cast
  77  ring
  78
  79/-! ## §4. Master certificate -/
  80
  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
  89def rSCryptographicBoundCert : RSCryptographicBoundCert where
  90  perBit_pos := perBitCost_pos
  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. -/
 100theorem cryptography_one_statement :
 101    0 < perBitCost ∧
 102    (∀ n, totalRecoveryCost (n + 1) = totalRecoveryCost n + perBitCost) ∧
 103    (∀ n, totalRecoveryCost (2 * n) = 2 * totalRecoveryCost n) :=
 104  ⟨perBitCost_pos, totalRecoveryCost_succ, totalRecoveryCost_double⟩
 105
 106end
 107
 108end RSCryptographicBound
 109end Cryptography
 110end IndisputableMonolith
 111