`T_node_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Engineering.ZMatchedTransceiverMesh
domain: Engineering
line: 41 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Engineering.ZMatchedTransceiverMesh on GitHub at line 41.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  38/-- Per-node throughput (dimensionless reference). -/
  39def T_node : ℝ := 1
  40
  41theorem T_node_pos : 0 < T_node := by unfold T_node; norm_num
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.