mesh_one_statement
plain-language theorem explainer
Aggregate throughput in a Z-matched transceiver mesh grows linearly with node count via additive increments of T_node and exact doubling at 2N, while pairwise latency stays independent of separation. Engineers designing RS_PAT_042 networks cite the result for scaling guarantees. The proof is a term-mode construction that assembles three prior component results into the required conjunction.
Claim. Let $T(N)$ denote aggregate throughput for $N$ nodes with per-node throughput $T_0 = 1$, and let $L(d)$ denote pairwise latency at separation $d$. Then $T(N+1) = T(N) + T_0$, $T(2N) = 2T(N)$, and $L(d_1) = L(d_2)$ for all real $d_1, d_2$.
background
The Z-Matched Recognition-Transceiver Mesh module models a network of $N$ phantom-cavity transceivers (RS_PAT_042) in which each $(Z, Θ)$-channel is independent and distance-decoupled. Per-node throughput $T_0$ is the dimensionless reference value 1. Aggregate throughput is defined by the function $T(N) := N · T_0$. Pairwise latency is defined as the constant value latency_per_pair for any separation $d$, per the distance-decoupling property stated in the module.
proof idea
The proof is a one-line term-mode wrapper that directly supplies the three component results aggregateThroughput_succ, aggregateThroughput_double, and pairwiseLatency_constant to form the conjunction.
why it matters
The declaration supplies the single-statement summary of the engineering derivation on Track J9 of Plan v5. It records the linear scaling of aggregate throughput and the distance-independent latency required for RS_PAT_042 meshes. No downstream results depend on it in the current graph, so the statement functions as a terminal engineering claim. The module doc-comment supplies the explicit falsifier of sublinear throughput exceeding 10 percent in a deployed mesh of four or more nodes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.