A linear point-count bound for a geometric phase

The polynomial factor contains only depths and scalar bit widths. In particular, the full 2^width point list is charged once, rather than being raised to a power as part of a record-width estimate.

theorem Algebraic.MassProduction.Nonuniform.GeometricPhase.costBound_le_linear {menuDepth requestDepth width dimension routingDepth requestWidth height : ℕ} (heightBound : 2 * menuDepth + requestDepth + width + dimension * width + routingDepth + requestWidth + 3 ≤ height) : costBound menuDepth requestDepth width dimension routingDepth requestWidth ≤ 10000 * (Sorting.networkRecords (menuDepth + requestDepth + width) + Sorting.networkRecords routingDepth) * height ^ 5

A phase is linear in generated and routed point counts, with a fifth degree polynomial in its bit widths and sorting depths.