aggregateThroughput_double

formal source

  71  exact (mul_lt_mul_iff_of_pos_right T_node_pos).mpr h_real
  72
  73/-- Linearity: throughput at 2N is exactly twice throughput at N. -/
  74theorem aggregateThroughput_double (N : ℕ) :
  75    aggregateThroughput (2 * N) = 2 * aggregateThroughput N := by
  76  unfold aggregateThroughput; push_cast; ring
  77
  78/-! ## §3. Distance-decoupled latency -/
  79
  80/-- Distance-decoupled latency: returns `latency_per_pair` regardless
  81of node-pair separation `d`. -/
  82def pairwiseLatency (d : ℝ) : ℝ := latency_per_pair
  83
  84theorem pairwiseLatency_constant (d₁ d₂ : ℝ) :
  85    pairwiseLatency d₁ = pairwiseLatency d₂ := rfl
  86
  87theorem pairwiseLatency_pos (d : ℝ) : 0 < pairwiseLatency d :=
  88  latency_per_pair_pos
  89
  90/-! ## §4. Master certificate -/
  91
  92structure ZMatchedTransceiverMeshCert where
  93  T_node_pos : 0 < T_node
  94  latency_pos : 0 < latency_per_pair
  95  agg_zero : aggregateThroughput 0 = 0
  96  agg_succ : ∀ N, aggregateThroughput (N + 1) = aggregateThroughput N + T_node
  97  agg_strict_mono : ∀ {N M : ℕ}, N < M → aggregateThroughput N < aggregateThroughput M
  98  agg_double : ∀ N, aggregateThroughput (2 * N) = 2 * aggregateThroughput N
  99  latency_constant : ∀ d₁ d₂, pairwiseLatency d₁ = pairwiseLatency d₂
 100
 101def zMatchedTransceiverMeshCert : ZMatchedTransceiverMeshCert where
 102  T_node_pos := T_node_pos
 103  latency_pos := latency_per_pair_pos
 104  agg_zero := aggregateThroughput_zero