aggregateThroughput_pos
plain-language theorem explainer
The theorem shows that aggregate throughput T(N) for an N-node Z-matched transceiver mesh is strictly positive for every natural number N at least 1. Engineers modeling recognition-based mesh networks cite it to guarantee non-zero capacity under the linear scaling T(N) = N · T_node. The proof is a one-line term application that unfolds the definition and invokes multiplication positivity on the cast of the node-count hypothesis together with the already-established positivity of T_node.
Claim. For every natural number $N$ satisfying $N ≥ 1$, the aggregate throughput $T(N) = N · T_{node}$ obeys $0 < T(N)$, where $T_{node}$ is the per-node throughput of a single Z-matched phantom-cavity transceiver.
background
The module treats a mesh of N Z-matched phantom-cavity transceivers whose aggregate throughput is defined by the product of node count and the fixed per-node throughput T_node. The upstream theorem T_node_pos records that T_node is positive and corresponds to the dimensionless coefficient of the distance-independent (Z, Θ)-channel latency ℏ_C / (2 · ΔE) ≈ 0.07 µs. The local setting is the engineering derivation track J9 of Plan v5, in which each (Z, Θ)-channel between matched nodes remains independent.
proof idea
The term proof first unfolds the definition of aggregateThroughput, exposing the product (N : ℝ) · T_node. It then applies the multiplication-positivity lemma mul_pos to the cast of the hypothesis 1 ≤ N (which supplies 0 < N) and the already-proved result T_node_pos.
why it matters
This result establishes the first bullet of the module's stated goals: aggregate throughput is linear in node count and strictly positive. It supports the claim that adding a node increases throughput by exactly T_node with no distance-dependent penalties, consistent with the ZThetaSpatialDecoupling foundation. No downstream uses are recorded yet, but the declaration closes the positivity half of the linear-scaling argument for the transceiver-mesh model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.