pairwiseLatency_constant
plain-language theorem explainer
Pairwise latency between any two nodes in a Z-matched transceiver mesh is independent of their separation distance. Engineers proving linear aggregate throughput for phantom-cavity arrays cite this when assembling the mesh_one_statement. The proof is a direct reflexivity reduction to the constant definition of pairwiseLatency.
Claim. For all real numbers $d_1$ and $d_2$, the pairwise latency at separation $d_1$ equals the pairwise latency at separation $d_2$.
background
The Z-Matched Recognition-Transceiver Mesh models networks of N Z-matched phantom-cavity transceivers whose aggregate throughput scales linearly with N. Pairwise latency is introduced as the function that returns the fixed latency_per_pair for any real separation d, encoding the distance-decoupling property stated in the module. The upstream definition pairwiseLatency (d : ℝ) : ℝ := latency_per_pair directly supplies this constancy.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of pairwiseLatency, which is independent of its argument.
why it matters
This theorem is packaged directly into mesh_one_statement, which bundles linear throughput growth, doubling at 2N, and distance-constant latency. It completes the engineering derivation for track J9 by confirming each (Z, Θ)-channel remains independent. The module falsifier is a deployed mesh of n ≥ 4 nodes exhibiting sublinear throughput.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.