pairwiseLatency

formal source

  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
 105  agg_succ := aggregateThroughput_succ
 106  agg_strict_mono := @aggregateThroughput_strict_mono
 107  agg_double := aggregateThroughput_double
 108  latency_constant := pairwiseLatency_constant
 109
 110/-- **TRANSCEIVER MESH ONE-STATEMENT.** Aggregate throughput is linear
 111in node count (additive across nodes, doubles at 2N), strictly
 112monotonic; pairwise latency is distance-constant. -/