Native computation of canonical path data

Input natural labels and coordinates use binary encodings; syntactic positions and the subdivision budget use unary counters. These certificates compute only the shared paths, crossing cells, and occurrence lookup, with no geometric validity assumption.

Main results

• Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_budget.
• Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_paths.
• Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_crossingSites.
• Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_occurrencePath.

References

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

theorem Cslib.Complexity.SAT.PlanarCompile.computable_intAdd {α : Type} {enc : α ↪ List Bool} {f g : α → ℤ} (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc Turing.MultiTapeTM.encIntBin) (hg : Turing.MultiTapeTM.ComputableInPolyTime g enc Turing.MultiTapeTM.encIntBin) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => f a + g a) enc Turing.MultiTapeTM.encIntBin

Pointwise binary integer addition is polynomial-time computable.

theorem Cslib.Complexity.SAT.PlanarCompile.computable_natCast : Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => ↑n) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encIntBin

Casting a unary natural number to a binary integer is polynomial-time computable.

theorem Cslib.Complexity.SAT.PlanarCompile.computable_layoutCenter : Turing.MultiTapeTM.ComputableInPolyTime Orthogonal.Layout.center Turing.MultiTapeTM.encUnary Orthogonal.encPoint

Layout.center is computable in polynomial time from a unary index.

theorem Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_budget : Turing.MultiTapeTM.ComputableInPolyTime budget encCNF Turing.MultiTapeTM.encUnary

The budget is a linear expression in syntactic list lengths, computed as a unary counter.

theorem Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_paths : Turing.MultiTapeTM.ComputableInPolyTime paths encCNF (Turing.MultiTapeTM.encList Orthogonal.encRoute)

Canonical incidence routes have a native polynomial-time bounded unit expansion. The input labels and output coordinates are binary; only the step budget is unary.

theorem Cslib.Complexity.SAT.PlanarCompile.computable_distinctPoints : Turing.MultiTapeTM.ComputableInPolyTime (fun (l : Orthogonal.Route) => selectDistinct l (List.replicate (List.length l) true)) Orthogonal.encRoute Orthogonal.encRoute

Deduplicating a route via selectDistinct with an all-true mask is polynomial-time computable.

theorem Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_crossingSites : Turing.MultiTapeTM.ComputableInPolyTime crossingSites encCNF Orthogonal.encRoute

Occupied nonvertex crossing sites can be selected in native polynomial time.

theorem Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_occurrencePath : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CNF ℕ × Logic.PL.Occurrence ℕ) => occurrencePath p.1 p.2) (Turing.MultiTapeTM.encPair encCNF (Logic.PL.encOccurrence Turing.MultiTapeTM.encNat)) Orthogonal.encRoute

Looking up the path for a syntactic literal occurrence is native polynomial-time.