aggregateThroughput
plain-language theorem explainer
Aggregate throughput for an N-node Z-matched transceiver mesh equals N times the unit per-node throughput. Engineers deriving linear scaling for recognition-based networks cite this base relation to establish additivity and monotonicity. It is introduced as a direct multiplication by the constant reference value.
Claim. Let $T(N)$ denote aggregate throughput for $N$ nodes in a Z-matched mesh. Then $T(N) = N · T_{node}$ where $T_{node} = 1$ is the dimensionless per-node throughput.
background
The Z-Matched Recognition-Transceiver Mesh module treats a network of N phantom-cavity transceivers whose (Z, Θ)-channels remain independent and distance-decoupled. Per-node throughput is introduced as the constant reference value 1 in dimensionless units. This definition supplies the base quantity used by all subsequent linearity statements in the module.
proof idea
Direct definition that multiplies the cast node count by the constant T_node.
why it matters
This definition supplies the common term for aggregateThroughput_succ, aggregateThroughput_double, aggregateThroughput_strict_mono and mesh_one_statement. It fills the engineering derivation track that asserts linear scaling of throughput with node count and constant pairwise latency. The module falsifier is a deployed mesh of n ≥ 4 nodes whose measured throughput falls more than 10 % below the linear prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.