Canonical paths of the actual planarization compiler

The executable compiler uses the canonical unit paths of the existing CNF incidence graph. These shared certificates serve both continuous geometry and logical wire correctness.

Main results

• Cslib.Complexity.SAT.PlanarCompile.paths_eq_unitPaths, .occurrencePath_eq_unitPath: exact agreement with the canonical graph layout.

• Cslib.Complexity.SAT.PlanarCompile.occurrence_index_lt, .incidenceGraph_edge_idxOf: valid literal-incidence indices and the edges they select.

• Cslib.Complexity.SAT.PlanarCompile.occurrencePath_endpoints, .occurrencePath_nodup: actual endpoints and uniqueness of all listed points.

• Cslib.Complexity.SAT.PlanarCompile.occurrencePath_unit, .occurrencePath_last_unit: unit adjacency, including the final-literal lookups.

• Cslib.Complexity.SAT.PlanarCompile.occurrencePath_ne_nil, .occurrencePath_length_ge_two: paths contain a genuine unit step before the original clause center.

• Cslib.Complexity.SAT.PlanarCompile.occurrencePaths_eq_paths: indexed source occurrences select exactly the emitted canonical paths in their original order.

References

These certificates refer to the original canonical path construction in the imported compiler.

theorem Cslib.Complexity.SAT.PlanarCompile.paths_eq_unitPaths (φ : Logic.PL.CNF ℕ) : paths φ = (incidenceGraph φ).unitPaths

The executable compiler uses exactly the canonical unit paths certified by the layout API.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePath_eq_unitPath (φ : Logic.PL.CNF ℕ) (o : Logic.PL.Occurrence ℕ) : occurrencePath φ o = (incidenceGraph φ).unitPath (List.idxOf o (Logic.PL.occurrences φ))

Literal-occurrence indexing selects the same path in the compiler and canonical layout.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrence_index_lt {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : List.idxOf o (Logic.PL.occurrences φ) < (incidenceGraph φ).edges.length

Every actual occurrence indexes an existing incidence edge.

theorem Cslib.Complexity.SAT.PlanarCompile.incidenceGraph_edge_idxOf {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : (incidenceGraph φ).edges[List.idxOf o (Logic.PL.occurrences φ)] = (List.idxOf o.2.2.1 φ.distinctVars, φ.distinctVars.length + o.1)

The incidence edge indexed by an actual occurrence joins its variable to its clause.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePath_nodup {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : List.Nodup (occurrencePath φ o)

Every actual occurrence path is duplicate-free, without an extra supplied path witness.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePath_unit {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) {e : Orthogonal.Point × Orthogonal.Point} (he : e ∈ List.consecutivePairs (occurrencePath φ o)) : Orthogonal.length e.1 e.2 = 1

Every consecutive step in the actual compiler path is a unit grid displacement.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePath_ne_nil {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : occurrencePath φ o ≠ []

Every actual selected path contains at least one point.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePath_endpoints {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : List.head? (occurrencePath φ o) = some (Orthogonal.Layout.center (List.idxOf o.2.2.1 φ.distinctVars)) ∧ List.getLast? (occurrencePath φ o) = some (Orthogonal.Layout.center (φ.distinctVars.length + o.1))

Actual occurrence paths start at the variable's source-grid center and end at their clause.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePath_length_ge_two {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : 2 ≤ List.length (occurrencePath φ o)

Actual literal paths contain at least one unit step, so final-literal lookups are in range.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePath_last_unit {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : have r := occurrencePath φ o; Orthogonal.length (List.getD r (List.length r - 2) (0, 0)) (List.getLastD r (0, 0)) = 1

The last two actual unit-path points are adjacent, including with the compiler's defaults.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePaths_eq_paths (φ : Logic.PL.CNF ℕ) : List.map (occurrencePath φ) (Logic.PL.occurrences φ) = paths φ

Enumerating source occurrences selects all actual paths in their original order.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePath_mem_paths {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : occurrencePath φ o ∈ paths φ

An actual occurrence selects a member of the canonical path list.