Source-boundary prefixes for local clause replacements

Each source placeholder is moved from its private local position to the corresponding boundary port. Its sole incidence is extended through the reversed access route. The old placeholder is then an ordinary interior bend, rather than a graph vertex. The finite certificates check the actual resulting prefixes, including simplicity and the restriction that a route can touch the box boundary only at its own variable endpoint.

Main definitions

• LocalGeometry.toPrefix: move source placeholders to boundary ports and extend their incidences.
• LocalGeometry.PrefixCheck: finite continuous certificates for such route prefixes.

Main results

• LocalGeometry.prefix_boundary_contact: only the variable endpoint can touch the boundary.

References

These are original geometric certificates for the cited exact-one clause constructions.

def Cslib.Complexity.SAT.ExactOne.LocalGeometry.segmentRouteContactCheck (allowed : List Orthogonal.Point) (r s : Orthogonal.Route) : Bool

Check only consecutive segment pairs for two proper routes after a bounding-box precheck. Listed points already belong to such segments, so including their separate degenerate pieces would duplicate this work.

theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.segmentRouteContactCheck_sound {allowed : List Orthogonal.Point} {r s : Orthogonal.Route} (hr : 2 ≤ List.length r) (hs : 2 ≤ List.length s) (h : segmentRouteContactCheck allowed r s = true) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support r) (hq : p ∈ Orthogonal.support s) : ∃ q ∈ allowed, p = Orthogonal.realPoint q

Consecutive-segment checking controls the full real support of proper routes.

def Cslib.Complexity.SAT.ExactOne.LocalGeometry.boundaryRoute (g : LocalGeometry) : Orthogonal.Route

The closed polygonal boundary of a local cell.

def Cslib.Complexity.SAT.ExactOne.LocalGeometry.toPrefix (g : LocalGeometry) : LocalGeometry

Move each source placeholder to its boundary port and extend its unique incidence through the old placeholder position. terminalVariables retains the boundary placeholders' indices.

def Cslib.Complexity.SAT.ExactOne.LocalGeometry.PrefixCheck (g : LocalGeometry) : Prop

A finite certificate for local incidence routes whose source ends lie on the cell boundary. Full route contacts, nonincident vertices and the complete cell boundary are checked.

@[instance_reducible]

instance Cslib.Complexity.SAT.ExactOne.LocalGeometry.instDecidablePrefixCheck (g : LocalGeometry) : Decidable g.PrefixCheck

theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.prefix_incidence_endpoints {g : LocalGeometry} (h : g.PrefixCheck) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) : e.clauseIndex < g.clausePositions.length ∧ e.variableIndex < g.variablePositions.length ∧ List.head? e.route = some (g.clausePosition e.clauseIndex) ∧ List.getLast? e.route = some (g.variablePosition e.variableIndex)

Every checked prefix has its prescribed clause and variable endpoints.

theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.prefix_incidence_orthogonal {g : LocalGeometry} (h : g.PrefixCheck) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) : Orthogonal.IsOrthogonal e.route

Every checked prefix is properly orthogonal.

theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.prefix_incidence_isSimple {g : LocalGeometry} (h : g.PrefixCheck) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) : Orthogonal.IsSimple e.route

Every checked prefix is simple on its full continuous support.

theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.prefix_incidence_bounds {g : LocalGeometry} (h : g.PrefixCheck) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) (p : Orthogonal.Point) : p ∈ e.route → 0 ≤ p.1 ∧ p.1 ≤ ↑g.size ∧ 0 ≤ p.2 ∧ p.2 ≤ ↑g.size

Every point listed in a checked prefix lies in its closed cell.

theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.prefix_incidence_length {g : LocalGeometry} (h : g.PrefixCheck) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) : 2 ≤ List.length e.route

Every checked prefix has at least one proper consecutive segment.

theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.prefix_routes_contact {g : LocalGeometry} (h : g.PrefixCheck) {e f : LocalIncidence} (he : e ∈ g.incidenceRoutes) (hf : f ∈ g.incidenceRoutes) (hne : e ≠ f) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support e.route) (hq : p ∈ Orthogonal.support f.route) : ∃ q ∈ g.commonEndpoints e f, p = Orthogonal.realPoint q

Checked prefixes meet only at shared graph endpoints.

theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.prefix_variable_not_mem_support {g : LocalGeometry} (h : g.PrefixCheck) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) {v : Fin g.variablePositions.length} (hv : ↑v ≠ e.variableIndex) : Orthogonal.realPoint (g.variablePosition ↑v) ∉ Orthogonal.support e.route

A checked prefix avoids every nonincident variable vertex.

theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.prefix_clause_not_mem_support {g : LocalGeometry} (h : g.PrefixCheck) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) {i : Fin g.clausePositions.length} (hi : ↑i ≠ e.clauseIndex) : Orthogonal.realPoint (g.clausePosition ↑i) ∉ Orthogonal.support e.route

A checked prefix avoids every nonincident clause vertex.

theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.prefix_boundary_contact {g : LocalGeometry} (h : g.PrefixCheck) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support e.route) (hq : p ∈ Orthogonal.support g.boundaryRoute) : p = Orthogonal.realPoint (g.variablePosition e.variableIndex)

The variable endpoint is the only permitted contact with the full cell boundary.