aggregateThroughput_strict_mono
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not bound throughput when nodes share spectrum or introduce interference.
- Does not extend the inequality to real-valued node counts.
- Does not fold latency or energy cost into the throughput comparison.
- Does not treat finite-size corrections for small N.
Lean usage
example (h : 3 < 5) : aggregateThroughput 3 < aggregateThroughput 5 := aggregateThroughput_strict_mono hformal statement (Lean)
67theorem aggregateThroughput_strict_mono {N M : ℕ} (h : N < M) :
68 aggregateThroughput N < aggregateThroughput M := by
proof body
Tactic-mode proof.
69 unfold aggregateThroughput
70 have h_real : (N : ℝ) < (M : ℝ) := by exact_mod_cast h
71 exact (mul_lt_mul_iff_of_pos_right T_node_pos).mpr h_real
72
73/-- Linearity: throughput at 2N is exactly twice throughput at N. -/