pairwiseLatency_pos
plain-language theorem explainer
The theorem shows that distance-decoupled latency between any pair of Z-matched transceivers is strictly positive. Engineers modeling mesh networks under Recognition Science cite it to confirm that per-pair delays stay bounded away from zero independent of separation. The proof is a direct one-line application of the base latency positivity result via the definition that returns the same constant for every distance.
Claim. For every real number $d$, the distance-decoupled latency $L(d)$ satisfies $0 < L(d)$, where $L(d)$ equals the fixed base latency value for any separation $d$.
background
The Z-Matched Recognition-Transceiver Mesh models networks of phantom-cavity transceivers whose (Z, Θ)-channels are independent and distance-decoupled. Pairwise latency is defined to return the constant base value regardless of node-pair separation, following the spatial decoupling property. This rests on the upstream result that the base latency per pair is positive, established by unfolding its definition and applying numerical normalization.
proof idea
The proof is a one-line wrapper that applies the positivity theorem for the base latency per pair, using the definition that pairwise latency equals that base value for any distance.
why it matters
This result completes the proof that per-pair latency is constant and positive, which is required for the linear aggregate throughput property stated in the module. It fills the engineering derivation step supporting distance-decoupled channels in the master certificate. The module lists no open questions attached to this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.