Geometry of canonical incidence paths

Shared unit-step, directed-port and midpoint uniqueness certificates support the paired compiler without retaining the obsolete directed-output formula or its drawing.

Main results

• Cslib.Complexity.SAT.PlanarCompile.paths_shared_step_index.
• Cslib.Complexity.SAT.PlanarCompile.pathPorts_nodup.
• Cslib.Complexity.SAT.PlanarCompile.pathMidpoints_nodup.
• Cslib.Complexity.SAT.PlanarCompile.clause_cell_not_mem_crossingSites.
• Cslib.Complexity.SAT.PlanarCompile.clause_cell_not_mem_path_dropLast.

References

These are the shared canonical incidence-path constructions and certificates.

theorem Cslib.Complexity.SAT.PlanarCompile.paths_shared_step_index {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {i j : ℕ} (hi : i < (paths φ).length) (hj : j < (paths φ).length) {p q : Orthogonal.Point} (he : (p, q) ∈ List.consecutivePairs ((paths φ).getD i [])) (hf : (p, q) ∈ List.consecutivePairs ((paths φ).getD j []) ∨ (q, p) ∈ List.consecutivePairs ((paths φ).getD j [])) : i = j

Two actual canonical paths cannot share a unit grid edge, even in opposite directions. This count-free uniqueness statement also applies to the final step into a clause cell.

theorem Cslib.Complexity.SAT.PlanarCompile.side_injective_on_unit_neighbors {p q t : Orthogonal.Point} (hq : Orthogonal.length p q = 1) (ht : Orthogonal.length p t = 1) (hside : side p q = side p t) : q = t

At a unit neighbor, the facing side determines the neighbor itself.

theorem Cslib.Complexity.SAT.PlanarCompile.pathPorts_nodup {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) : (List.flatMap (fun (r : Orthogonal.Route) => List.flatMap (fun (e : Orthogonal.Point × Orthogonal.Point) => [(e.1, side e.1 e.2), (e.2, side e.2 e.1)]) (List.consecutivePairs r)) (paths φ)).Nodup

All directed cell ports in the actual canonical paths are distinct. Both halves of every unit step are included, even the final clause-directed half. No path witness is assumed.

theorem Cslib.Complexity.SAT.PlanarCompile.cellPort_step_eq_cases {p q a b : Orthogonal.Point} (hpq : Orthogonal.length p q = 1) (hab : Orthogonal.length a b = 1) (h : Orthogonal.cellPort 120 p (side p q) = Orthogonal.cellPort 120 a (side a b)) : p = a ∧ q = b ∨ p = b ∧ q = a

Equal boundary midpoints identify the same unordered unit grid edge.

theorem Cslib.Complexity.SAT.PlanarCompile.pathMidpoints_nodup {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) : (List.flatMap (fun (r : Orthogonal.Route) => List.map (fun (e : Orthogonal.Point × Orthogonal.Point) => Orthogonal.cellPort 120 e.1 (side e.1 e.2)) (List.consecutivePairs r)) (paths φ)).Nodup

One geometric midpoint per actual unit step gives a duplicate-free list. This includes final steps, so any prefix selection used for binary clauses remains distinct.

theorem Cslib.Complexity.SAT.PlanarCompile.center_injective : Function.Injective center

Distinct integer cells have distinct displayed centers.

theorem Cslib.Complexity.SAT.PlanarCompile.clause_cell_not_mem_crossingSites (φ : Logic.PL.CNF ℕ) {i : ℕ} (hi : i < List.length φ) : Orthogonal.Layout.center (φ.distinctVars.length + i) ∉ crossingSites φ

Original clause cells are declared source centers and are never selected as crossings.

theorem Cslib.Complexity.SAT.PlanarCompile.clause_cell_not_mem_path_dropLast {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) {i : ℕ} (hi : i < List.length φ) : Orthogonal.Layout.center (φ.distinctVars.length + i) ∉ List.dropLast (occurrencePath φ o)

No source clause center is used as a signal cell before a path's final endpoint.