zMatchedTransceiverMeshCert
plain-language theorem explainer
The definition constructs a certificate asserting linear aggregate throughput T(N) = N · T_node with T_node > 0, strict monotonicity, exact doubling at 2N, zero base case, and distance-independent pairwise latency for a Z-matched transceiver mesh. Network engineers deriving scaling bounds from Recognition Science would cite the certificate to certify mesh performance. It is assembled by direct record instantiation that assigns each field from the module's supporting lemmas on positivity, successor addition, monotonicity, doubling, and latency r
Claim. Let $T(N)$ be aggregate throughput for $N$ nodes with per-node throughput $T_0 > 0$, and let $L(d)$ be pairwise latency at separation $d$. The certificate asserts $T(0) = 0$, $T(N+1) = T(N) + T_0$ for all $N$, $T$ strictly increasing on naturals, $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 derives engineering performance for a mesh of N Z-matched phantom-cavity transceivers. Aggregate throughput is defined as $T(N) = N · T_0$ where each (Z, Θ)-channel is independent and distance-decoupled; pairwise latency is constant per the spatial decoupling result. The structure packages six properties: positivity of $T_0$, positivity of per-pair latency, the zero base case, the successor step, strict monotonicity, exact doubling, and distance invariance of latency.
proof idea
The definition is a direct record construction that populates each field of the target structure by referencing the corresponding sibling theorem: T_node_pos supplies the positivity field, latency_per_pair_pos supplies the latency positivity field, aggregateThroughput_zero supplies the base case, aggregateThroughput_succ supplies the successor step, aggregateThroughput_strict_mono supplies monotonicity, aggregateThroughput_double supplies the doubling identity, and pairwiseLatency_constant supplies the latency invariance field.
why it matters
This definition supplies the single-statement certificate for the engineering derivation of transceiver mesh performance. It directly implements the module claims that aggregate throughput is linear in node count and pairwise latency is distance-constant, closing the engineering track with the explicit falsifier of sublinear throughput by more than 10% in a deployed mesh of four or more nodes. No downstream uses are recorded in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.