T_node
plain-language theorem explainer
T_node supplies the dimensionless reference value of per-node throughput in the Z-matched transceiver mesh. Network modelers cite it to establish linear scaling of aggregate throughput with node count. The declaration is a direct constant assignment.
Claim. The per-node throughput reference is the real number $1$.
background
The module models a mesh of N Z-matched phantom-cavity transceivers whose (Z, Θ)-channels are independent and distance-decoupled. Aggregate throughput is defined as T(N) = N · T_node, with pairwise latency independent of separation. T_node is introduced as the base unit that makes throughput additive across nodes.
proof idea
One-line definition that assigns the constant value 1 to T_node.
why it matters
T_node anchors aggregateThroughput and the mesh_one_statement theorem that proves linearity, doubling at 2N, and strict monotonicity. It supplies the engineering base for the J9 track claim of distance-decoupled channels. The value 1 is the reference that lets T_node_pos and the certification structure record positivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.