aggregateThroughput
plain-language theorem explainer
Aggregate throughput for N nodes equals N times the per-node throughput T_node in a Z-matched transceiver mesh. Network engineers cite it when predicting linear capacity scaling for phantom-cavity arrays. The definition is a direct cast-and-multiply that enables immediate algebraic reductions in additivity and doubling lemmas.
Claim. The aggregate throughput $T(N)$ of a mesh with $N$ nodes is $T(N) = N · T_0$, where $T_0$ is the dimensionless per-node throughput reference.
background
The Z-Matched Recognition-Transceiver Mesh module models networks of phantom-cavity transceivers whose (Z, Θ)-channels are independent and distance-decoupled. T_node is the constant 1 serving as the per-node throughput reference in dimensionless units. This setting rests on Foundation.ZThetaSpatialDecoupling, which supplies the constant pairwise latency used in the module's one-statement summary.
proof idea
The definition is a direct multiplication of the cast natural number N by the constant T_node. No lemmas are invoked; the body is an abbrev that unfolds immediately for ring and cast tactics in downstream proofs.
why it matters
This definition supplies the base expression for mesh_one_statement, which packages linearity, doubling at 2N, and constant latency into a single engineering claim. It completes the J9 track derivation that aggregate throughput grows linearly with node count, matching the Recognition framework's prediction of distance-decoupled channels. No scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.