IndisputableMonolith.Engineering.ZMatchedTransceiverMesh

declarations in this module (16)

• def T_node L39
• theorem T_node_pos L41
• def latency_per_pair L45
• theorem latency_per_pair_pos L47
• def aggregateThroughput L53
• theorem aggregateThroughput_zero L55
• theorem aggregateThroughput_succ L58
• theorem aggregateThroughput_pos L62
• theorem aggregateThroughput_strict_mono L67
• theorem aggregateThroughput_double L74
• def pairwiseLatency L82
• theorem pairwiseLatency_constant L84
• theorem pairwiseLatency_pos L87
• structure ZMatchedTransceiverMeshCert L92
• def zMatchedTransceiverMeshCert L101
• theorem mesh_one_statement L113