Constant-factor coordinate bounds for the actual positive drawing compiler

Every emitted vertex and route point is bounded on the actual drawing lists. The source drawing is dilated by positiveScale = 1080000, and every local replacement lies in a side-540000 square. The source axis translation and the endpoint cuts fit within the same constant margin. These bounds do not require geometric validity of the input drawing.

Main results

• positiveDrawing_fits: an input rectangle of width W and height H yields an actual output rectangle with sides positiveScale * (W + 1) and positiveScale * (H + 1).

References

The explicit coordinate and finite-output bounds are original.

theorem Cslib.Complexity.SAT.ExactOne.positiveExterior_points_fits {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} {W H : ℕ} (hd : Graph.drawingFits d W H) (i j : ℕ) (q : Orthogonal.Point) : q ∈ positiveExterior φ d i j → 0 ≤ q.1 ∧ q.1 ≤ ↑positiveScale * (↑W + 1) ∧ 0 ≤ q.2 ∧ q.2 ≤ ↑positiveScale * (↑H + 1)

Every point of the actual inherited exterior route fits the enlarged source rectangle.

theorem Cslib.Complexity.SAT.ExactOne.positiveDrawing_fits (φ : Logic.PL.CNF ℕ) {d : Graph.OrthogonalDrawing} {W H : ℕ} (hd : Graph.drawingFits d W H) : Graph.drawingFits (positiveDrawing φ d) (positiveScale * (W + 1)) (positiveScale * (H + 1))

The actual emitted drawing expands both source grid sides by only a fixed factor. This holds for every finite input drawing, including malformed inputs handled by default lookups.