`zMatchedTransceiverMeshCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Engineering.ZMatchedTransceiverMesh
domain: Engineering
line: 101 · 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 101.

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

formal source

  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. -/
 113theorem mesh_one_statement :
 114    (∀ N, aggregateThroughput (N + 1) = aggregateThroughput N + T_node) ∧
 115    (∀ N, aggregateThroughput (2 * N) = 2 * aggregateThroughput N) ∧
 116    (∀ d₁ d₂, pairwiseLatency d₁ = pairwiseLatency d₂) :=
 117  ⟨aggregateThroughput_succ, aggregateThroughput_double, pairwiseLatency_constant⟩
 118
 119end
 120
 121end ZMatchedTransceiverMesh
 122end Engineering
 123end IndisputableMonolith

papers checked against this theorem

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