IndisputableMonolith.Engineering.CoherenceProtectedQKDLinkBudget

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Coherence-Protected QKD Link Budget (Track J7 of Plan v5)
   7
   8## Status: THEOREM (engineering derivation)
   9
  10Phantom-cavity-protected QKD link (RS_PAT_040) achieves bit-rate
  11`R(L) = R_0 · φ^(-L/L_φ)` where `L_φ` is the φ-rung attenuation
  12length. Each `L_φ` of fiber attenuates the rate by `1/φ ≈ 0.618`.
  13
  14## Falsifier
  15
  16QKD link deployed with phantom-cavity protection showing fiber-loss
  17attenuation outside `1/φ` per `L_φ` of fiber to within 5%.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Engineering
  22namespace CoherenceProtectedQKDLinkBudget
  23
  24open Constants
  25
  26noncomputable section
  27
  28/-! ## §1. Link rate ladder -/
  29
  30/-- Reference link rate at zero distance. -/
  31def R_0 : ℝ := 1
  32
  33/-- Link rate at φ-rung `n` (after `n · L_φ` km of fiber). -/
  34def linkRate (n : ℕ) : ℝ := R_0 / phi ^ n
  35
  36theorem linkRate_zero : linkRate 0 = R_0 := by
  37  unfold linkRate; simp
  38
  39theorem linkRate_pos (n : ℕ) : 0 < linkRate n := by
  40  unfold linkRate R_0
  41  exact div_pos one_pos (pow_pos phi_pos _)
  42
  43theorem linkRate_strict_anti {n m : ℕ} (h : n < m) :
  44    linkRate m < linkRate n := by
  45  unfold linkRate
  46  have hp1 : 0 < phi ^ n := pow_pos phi_pos _
  47  have h_pow : phi ^ n < phi ^ m := pow_lt_pow_right₀ one_lt_phi h
  48  -- R_0 / φ^m < R_0 / φ^n  ↔  φ^n < φ^m (since R_0 > 0).
  49  have h_R_pos : (0 : ℝ) < R_0 := by unfold R_0; norm_num
  50  exact div_lt_div_of_pos_left h_R_pos hp1 h_pow
  51
  52theorem linkRate_succ (n : ℕ) :
  53    linkRate (n + 1) = linkRate n / phi := by
  54  unfold linkRate
  55  rw [pow_succ]
  56  field_simp
  57
  58/-! ## §2. Attenuation factor per L_φ -/
  59
  60/-- Per-rung attenuation factor `= 1/φ ≈ 0.618`. -/
  61def attenuationPerRung : ℝ := 1 / phi
  62
  63theorem attenuationPerRung_pos : 0 < attenuationPerRung :=
  64  div_pos one_pos phi_pos
  65
  66theorem attenuationPerRung_lt_one : attenuationPerRung < 1 := by
  67  unfold attenuationPerRung
  68  rw [div_lt_one phi_pos]; exact one_lt_phi
  69
  70theorem attenuationPerRung_band :
  71    (0.617 : ℝ) < attenuationPerRung ∧ attenuationPerRung < 0.622 := by
  72  unfold attenuationPerRung
  73  have h1 := phi_gt_onePointSixOne
  74  have h2 := phi_lt_onePointSixTwo
  75  refine ⟨?_, ?_⟩
  76  · rw [lt_div_iff₀ phi_pos]; linarith
  77  · rw [div_lt_iff₀ phi_pos]; linarith
  78
  79/-! ## §3. Master certificate -/
  80
  81structure CoherenceProtectedQKDLinkBudgetCert where
  82  rate_zero : linkRate 0 = R_0
  83  rate_pos : ∀ n, 0 < linkRate n
  84  rate_strict_anti : ∀ {n m : ℕ}, n < m → linkRate m < linkRate n
  85  rate_succ : ∀ n, linkRate (n + 1) = linkRate n / phi
  86  attenuation_pos : 0 < attenuationPerRung
  87  attenuation_lt_one : attenuationPerRung < 1
  88  attenuation_band : (0.617 : ℝ) < attenuationPerRung ∧ attenuationPerRung < 0.622
  89
  90def coherenceProtectedQKDLinkBudgetCert :
  91    CoherenceProtectedQKDLinkBudgetCert where
  92  rate_zero := linkRate_zero
  93  rate_pos := linkRate_pos
  94  rate_strict_anti := @linkRate_strict_anti
  95  rate_succ := linkRate_succ
  96  attenuation_pos := attenuationPerRung_pos
  97  attenuation_lt_one := attenuationPerRung_lt_one
  98  attenuation_band := attenuationPerRung_band
  99
 100/-- **QKD ONE-STATEMENT.** Link rate `R(n) = R_0 · φ^(-n)`,
 101strictly anti-monotonic; per-rung attenuation `1/φ ∈ (0.617, 0.622)`. -/
 102theorem qkd_one_statement :
 103    (∀ n, linkRate (n + 1) = linkRate n / phi) ∧
 104    (∀ {n m : ℕ}, n < m → linkRate m < linkRate n) ∧
 105    (0.617 : ℝ) < attenuationPerRung ∧ attenuationPerRung < 0.622 :=
 106  ⟨linkRate_succ, @linkRate_strict_anti,
 107   attenuationPerRung_band.1, attenuationPerRung_band.2⟩
 108
 109end
 110
 111end CoherenceProtectedQKDLinkBudget
 112end Engineering
 113end IndisputableMonolith
 114