Documentation

CslibFrontier.Computability.Complexity.Problems.SAT.Planar.PathData

Canonical incidence-path data #

The retained shared data consist of bounded unit paths, selected crossing cells, and the common macrocell coordinates. No clauses, formula, or drawing are assembled here.

Main definitions #

Main results #

References #

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

source
def Cslib.Complexity.SAT.PlanarCompile.budget (φ : Logic.PL.CNF ℕ) :
ℕ

The explicit linear per-route expansion budget.

Instances For
    source
    def Cslib.Complexity.SAT.PlanarCompile.paths (φ : Logic.PL.CNF ℕ) :
    List Orthogonal.Route

    Unit paths in the order of the original literal occurrences.

    Instances For
      source
      def Cslib.Complexity.SAT.PlanarCompile.occurrencePath (φ : Logic.PL.CNF ℕ) (o : Logic.PL.Occurrence ℕ) :
      Orthogonal.Route

      The path of a particular original literal occurrence.

      Instances For
        source
        def Cslib.Complexity.SAT.PlanarCompile.crossingSites (φ : Logic.PL.CNF ℕ) :
        List Orthogonal.Point

        Actual occupied crossing candidates, excluding every declared graph vertex center. First-occurrence selection ensures exactly one local gadget per selected square.

        Instances For
          source
          theorem Cslib.Complexity.SAT.PlanarCompile.mem_crossingSites (φ : Logic.PL.CNF ℕ) (p : Orthogonal.Point) :
          p ∈ crossingSites φ ↔ p ∈ (incidenceGraph φ).crossingCandidates (incidenceGraph φ).canonicalPorts ∧ p ∉ (incidenceGraph φ).orthogonalPositions ∧ 2 ≤ (List.filter (fun (r : Orthogonal.Route) => List.contains r p) (paths φ)).length

          The selected cells are exactly occupied nonvertex candidates.

          source
          theorem Cslib.Complexity.SAT.PlanarCompile.crossingSites_nodup (φ : Logic.PL.CNF ℕ) :
          (crossingSites φ).Nodup

          Every selected square receives exactly one template.

          source
          def Cslib.Complexity.SAT.PlanarCompile.side (p q : Orthogonal.Point) :
          Fin 4

          Side facing a neighboring square, in left/right/bottom/top order. Only unit neighbors are used by the correctness theorem.

          Instances For
            source
            theorem Cslib.Complexity.SAT.PlanarCompile.side_cardinal (p : Orthogonal.Point) :
            side p (p - (1, 0)) = 0 ∧ side p (p + (1, 0)) = 1 ∧ side p (p - (0, 1)) = 2 ∧ side p (p + (0, 1)) = 3

            The side lookup recovers each of the four cardinal unit neighbors.

            source
            def Cslib.Complexity.SAT.PlanarCompile.center (p : Orthogonal.Point) :
            Orthogonal.Point

            The center of a square of side 240 indexed by an integer grid point.

            Instances For
              source
              theorem Cslib.Complexity.SAT.PlanarCompile.unit_neighbor_cases {p q : Orthogonal.Point} (h : Orthogonal.length p q = 1) :
              q = p + (-1, 0) ∨ q = p + (1, 0) ∨ q = p + (0, -1) ∨ q = p + (0, 1)

              Unit-adjacent integer cells differ by exactly one of the four cardinal displacements.

              source
              theorem Cslib.Complexity.SAT.PlanarCompile.shared_cellPort {p q : Orthogonal.Point} (h : Orthogonal.length p q = 1) :
              Orthogonal.cellPort 120 p (side p q) = Orthogonal.cellPort 120 q (side q p)

              Neighboring unit cells use exactly the same geometric midpoint for their shared port.