aggregateThroughput_succ
plain-language theorem explainer
The theorem establishes that aggregate throughput of an N-node Z-matched transceiver mesh increases exactly by the per-node throughput T_node when the node count reaches N+1. Engineers deriving linear scaling for Recognition Science meshes cite this to confirm additive node contributions. The proof is a one-line wrapper that unfolds the aggregate throughput definition and applies algebraic simplification via casting and the ring tactic.
Claim. For every natural number $N$, the aggregate throughput $T(N+1)$ of an $(N+1)$-node mesh equals the aggregate throughput $T(N)$ of an $N$-node mesh plus the per-node throughput $T_0$, where $T(N) := N · T_0$ and $T_0 = 1$.
background
The Z-Matched Recognition-Transceiver Mesh module derives engineering properties for a network of N Z-matched phantom-cavity transceivers. Each (Z, Θ)-channel is independent and distance-decoupled per Foundation.ZThetaSpatialDecoupling, yielding aggregate throughput linear in node count. The per-node throughput T_node is the dimensionless reference value 1. The aggregate throughput function is defined directly as aggregateThroughput N := (N : ℝ) * T_node.
proof idea
The proof is a one-line wrapper that unfolds the definition of aggregateThroughput, applies push_cast to convert the natural number addition into a real, and invokes the ring tactic to obtain the required equality.
why it matters
This declaration supplies the successor step for the mesh_one_statement theorem, which packages linearity, doubling at 2N, and constant pairwise latency into a single summary. It also populates the zMatchedTransceiverMeshCert certificate. The result confirms the additive composition of independent channels predicted by the module's engineering derivation, aligning with Recognition Science's emphasis on linear scaling in transceiver meshes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.