def
definition
latency_per_pair
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Engineering.ZMatchedTransceiverMesh on GitHub at line 45.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
42
43/-- Per-pair (Z, Θ)-channel latency = `ℏ_C / (2 · ΔE) ≈ 0.07 µs`,
44distance-independent. We record the dimensionless coefficient. -/
45def latency_per_pair : ℝ := 0.07
46
47theorem latency_per_pair_pos : 0 < latency_per_pair := by
48 unfold latency_per_pair; norm_num
49
50/-! ## §2. Aggregate throughput -/
51
52/-- Aggregate throughput at `N` nodes. -/
53def aggregateThroughput (N : ℕ) : ℝ := (N : ℝ) * T_node
54
55theorem aggregateThroughput_zero : aggregateThroughput 0 = 0 := by
56 unfold aggregateThroughput; simp
57
58theorem aggregateThroughput_succ (N : ℕ) :
59 aggregateThroughput (N + 1) = aggregateThroughput N + T_node := by
60 unfold aggregateThroughput; push_cast; ring
61
62theorem aggregateThroughput_pos {N : ℕ} (h : 1 ≤ N) :
63 0 < aggregateThroughput N := by
64 unfold aggregateThroughput
65 exact mul_pos (by exact_mod_cast (by omega : 0 < N)) T_node_pos
66
67theorem aggregateThroughput_strict_mono {N M : ℕ} (h : N < M) :
68 aggregateThroughput N < aggregateThroughput M := by
69 unfold aggregateThroughput
70 have h_real : (N : ℝ) < (M : ℝ) := by exact_mod_cast h
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