Ordinary-cell occupancy in the actual planarization paths

This module depends only on the executable compiler and canonical source layout. Both the continuous drawing proof and the literal-count proof can use it without importing each other.

Main results

• Cslib.Complexity.SAT.PlanarCompile.paths_filter_length_le_one: outside source centers and selected crossing cells, at most one actual path contains a given integer point.

References

This is an original consequence of the canonical path contact classification.

theorem Cslib.Complexity.SAT.PlanarCompile.paths_filter_length_le_one {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {p : Orthogonal.Point} (hp : p ∉ crossingSites φ) (hc : p ∉ (incidenceGraph φ).orthogonalPositions) : (List.filter (fun (r : Orthogonal.Route) => List.contains r p) (paths φ)).length ≤ 1

Away from source centers, an unselected ordinary cell belongs to at most one path.