ZMatchedTransceiverMeshCert
plain-language theorem explainer
The ZMatchedTransceiverMeshCert structure assembles the core properties of a Z-matched transceiver mesh: positive per-node throughput, linear aggregate throughput in node count, and distance-independent pairwise latency. Engineers modeling recognition-based communication meshes cite it to certify that throughput scales exactly as N times the per-node value. The definition is realized as a record that directly packages the module's existing throughput recurrence and constant-latency lemmas.
Claim. A certificate for a Z-matched transceiver mesh consists of the assertions $T_0 > 0$, $0 < L$, the aggregate throughput function satisfying $T(0) = 0$ and $T(N+1) = T(N) + T_0$ for all $N$, strict monotonicity of $T$, the doubling identity $T(2N) = 2T(N)$, and pairwise latency independent of node-pair distance.
background
In the Z-Matched Recognition-Transceiver Mesh module the per-node throughput is the dimensionless constant $T_0 := 1$. Aggregate throughput at $N$ nodes is defined by $T(N) := N · T_0$. Per-pair latency is the fixed value $L := 0.07$, and pairwise latency is defined to return exactly this value for any separation $d$. The module states that a mesh of $N$ Z-matched phantom-cavity transceivers achieves aggregate throughput linear in $N$ because each (Z, Θ)-channel is independent and distance-decoupled.
proof idea
The structure is a plain record whose fields are filled by direct reference to the module's prior definitions and lemmas: T_node_pos supplies the positivity of $T_0$, aggregateThroughput_zero and aggregateThroughput_succ supply the base and successor cases, aggregateThroughput_strict_mono supplies monotonicity, and the constant definition of pairwiseLatency supplies distance independence.
why it matters
This certificate is the central record for the linear-scaling claim in the Z-matched mesh derivation and is consumed directly by zMatchedTransceiverMeshCert. It completes the engineering step of Track J9, confirming that throughput grows exactly as $N · T_0$ with constant latency. Within Recognition Science it instantiates the distance-decoupling property that supports mesh performance independent of spatial separation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.