Rectilinear planarity testing of series-parallel graphs with maximum degree four, in the variable embedding setting, had a best known bound of O(n^2) time. The quadratic cost arises because spirality sets at SPQ*-tree nodes need not be intervals.

Spirality sets are represented as unions of arithmetic progressions of step two (pieces). A Key Lemma shows that light P2-nodes with a light child do not increase the number of pieces, which gives a 36^{4k} bound on pieces per node, where k is the number of degree-4 vertices. The Key Lemma, the combinatorial bounds, algorithm correctness and the fixed-root cost model are formalized in Lean 4 with Mathlib, with SPQ*-trees as an inductive type. Some steps are not formalized: correspondence of the rules to rectilinear representations, Lemmas 4 and 5, re-rooting, and tree construction.

Rectilinear planarity is testable in 2^{O(k)}·n time, which is subquadratic when k=o(log n). The Lean file contains no sorry and uses only the standard axioms.