aggregateThroughput_strict_mono
plain-language theorem explainer
The theorem shows aggregate throughput in a Z-matched transceiver mesh rises strictly with node count. Engineers scaling recognition networks cite it to guarantee that each added node increases total capacity by exactly T_node. The tactic proof unfolds the linear definition, casts the natural-number order to reals, and applies the multiplication inequality under the positivity of T_node.
Claim. Let $T(N) = N · T_{node}$ with $T_{node} > 0$. Then $T(N) < T(M)$ whenever $N, M ∈ ℕ$ and $N < M$.
background
The Z-Matched Recognition-Transceiver Mesh module treats a network of N phantom-cavity transceivers whose (Z, Θ)-channels are independent and distance-decoupled. Aggregate throughput is defined directly as the product of node count with the per-node coefficient T_node. The upstream result T_node_pos records the strict positivity 0 < T_node by norm_num after unfolding the coefficient.
proof idea
The tactic unfolds aggregateThroughput to expose multiplication by T_node. It introduces the cast (N : ℝ) < (M : ℝ) via exact_mod_cast. The final exact step invokes mul_lt_mul_iff_of_pos_right instantiated at T_node_pos to obtain the strict inequality.
why it matters
The result is referenced inside zMatchedTransceiverMeshCert to supply the strict-monochromaticity witness for the engineering certificate. It completes the linearity claim listed in the module's theorem block for track J9, confirming that throughput scales exactly with node count under channel independence. The module falsifier notes that sublinear scaling in a deployed mesh of four or more nodes would refute the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.