`mesh_one_statement`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Engineering.ZMatchedTransceiverMesh on GitHub at line 113.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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.