aggregateThroughput_double
plain-language theorem explainer
The theorem establishes that aggregate throughput of a Z-matched transceiver mesh exactly doubles when node count doubles. Network engineers deriving performance bounds for recognition-based meshes cite this linearity to confirm scalable channel independence. The proof is a one-line algebraic reduction that unfolds the throughput definition and applies casting plus the ring tactic.
Claim. Let $T(N)$ denote aggregate throughput for a mesh of $N$ nodes. Then $T(2N) = 2 T(N)$.
background
The module derives engineering properties for a network of $N$ Z-matched phantom-cavity transceivers. Aggregate throughput is defined as $T(N) := N · T_node$, where each (Z, Θ)-channel contributes independently and distance-decoupled latency equals the constant 0.07 per the latency_per_pair definition. The module setting states that this yields linear scaling in node count, with pairwise latency independent of separation per Foundation.ZThetaSpatialDecoupling.
proof idea
The proof unfolds the definition of aggregateThroughput, applies push_cast to the natural-number multiplication, and closes with the ring tactic.
why it matters
It supplies the doubling clause inside mesh_one_statement, which packages successor additivity, doubling, and constant latency into a single summary theorem. The result also populates the zMatchedTransceiverMeshCert structure. This completes the linearity claim in the J9 engineering track of the Recognition Science framework, where channel contributions remain additive without distance dependence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.