Matching actual local and exterior clause-box endpoints

The selected local source slot ends at precisely the same integer point as the normalized, scaled, trimmed original incidence. The far endpoint is the common actual source-variable vertex, including when different source literal positions use the same variable.

Main results

• clauseGeometry_source_point: actual local source-placeholder position.
• positiveExterior_endpoints: exact collar and shared-variable endpoints.

References

These finite-coordinate matching and indexing proofs are original.

theorem Cslib.Complexity.SAT.ExactOne.collared_variablePoint (g : LocalGeometry) (s : PortAssignment) {v : ℕ} (hv : v < g.variablePositions.length) : (collaredPrefixGeometry g s).variablePosition v = if v ∈ g.terminalVariables then collarOuterPort (s.side (terminalIndex g v)) else collarPoint (collarReflected s) (g.variablePosition v)

A valid local variable index resolves to its moved source port or its affine core point.

theorem Cslib.Complexity.SAT.ExactOne.collared_variablePoint_terminal (g : LocalGeometry) (s : PortAssignment) {v : ℕ} (hv : v < g.variablePositions.length) (ht : v ∈ g.terminalVariables) : (collaredPrefixGeometry g s).variablePosition v = collarOuterPort (s.side (terminalIndex g v))

An exposed local variable resolves to its prescribed outer collar midpoint.

theorem Cslib.Complexity.SAT.ExactOne.collared_clausePoint (g : LocalGeometry) (s : PortAssignment) {i : ℕ} (hi : i < g.clausePositions.length) : (collaredPrefixGeometry g s).clausePosition i = collarPoint (collarReflected s) (g.clausePosition i)

Every actual local clause position receives the common affine core placement.

theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_source_point (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) (j : Fin 3) (hj : ↑j < List.length (profileSource (clauseProfile c))) : (clauseGeometry φ d i c).variablePosition (List.idxOf (Sum.inl (Sum.inl ↑j)) (profileVariables (clauseProfile c))) = collarOuterPort ((clausePorts φ d i).side j)

The local source-slot position is the selected outer collar midpoint.

theorem Cslib.Complexity.SAT.ExactOne.positiveExterior_head {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (j : Fin 3) (hj : ↑j < List.length φ[i]) : List.head? (positiveExterior φ d i ↑j) = some (positiveBoxOrigin φ d i + collarOuterPort ((clausePorts φ d i).side j))

The exterior source incidence begins at the actual selected collar midpoint.

theorem Cslib.Complexity.SAT.ExactOne.positiveExterior_last {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i j : ℕ} (hi : i < List.length φ) (hj : j < List.length φ[i]) : List.getLast? (positiveExterior φ d i j) = some (positiveVariablePoint φ d (Sum.inl (Sum.inl φ[i][j].1)))

The exterior route ends at the actual shared source-variable vertex.

theorem Cslib.Complexity.SAT.ExactOne.positiveExterior_endpoints {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (j : Fin 3) (hj : ↑j < List.length φ[i]) : List.head? (positiveExterior φ d i ↑j) = some (positiveBoxOrigin φ d i + collarOuterPort ((clausePorts φ d i).side j)) ∧ List.getLast? (positiveExterior φ d i ↑j) = some (positiveVariablePoint φ d (Sum.inl (Sum.inl φ[i][j].1)))

Actual inherited exterior routes have exactly the local port and common variable endpoints.