pith. machine review for the scientific record. sign in
def definition def or abbrev

zMatchedTransceiverMeshCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 101def zMatchedTransceiverMeshCert : ZMatchedTransceiverMeshCert where
 102  T_node_pos := T_node_pos

proof body

Definition body.

 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. -/

depends on (13)

Lean names referenced from this declaration's body.