Collared positive exact-one profiles

The twenty-four ordered injections into the four exterior directions are handled by the common annular collars. All geometry proofs reuse the fifteen inner-profile certificates and the twenty-four collar certificates; they do not repeat an exhaustive route-pair audit for every combination.

Main results

• collaredProfile_incidence_orthogonal, collaredProfile_incidence_isSimple: actual placed incidence routes remain proper and continuously simple.

References

These are original continuous gluing certificates for the exact-one replacement profiles.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_terminal_endpoint (p : ClauseProfile) (v : ℕ) : v ∈ (profilePrefixGeometry p).terminalVariables → (profilePrefixGeometry p).variablePosition v = innerTemplatePort (terminalIndex (profilePrefixGeometry p) v)

Every source endpoint of the actual inner prefix is its indexed north, west or east port.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_terminalIndex_injective (p : ClauseProfile) (v : ℕ) : v ∈ (profilePrefixGeometry p).terminalVariables → ∀ w ∈ (profilePrefixGeometry p).terminalVariables, terminalIndex (profilePrefixGeometry p) v = terminalIndex (profilePrefixGeometry p) w → v = w

Distinct exposed source variables have distinct collar indices.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_terminal_lt (p : ClauseProfile) (v : ℕ) : v ∈ (profilePrefixGeometry p).terminalVariables → v < (profilePrefixGeometry p).variablePositions.length

Every source placeholder has a valid local variable index.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_variable_bounds (p : ClauseProfile) (v : Fin (profilePrefixGeometry p).variablePositions.length) : have q := (profilePrefixGeometry p).variablePosition ↑v; 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000

Every listed variable of the inner template lies in its closed square.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_auxiliary_ne_terminal (p : ClauseProfile) (v : Fin (profilePrefixGeometry p).variablePositions.length) : ↑v ∉ (profilePrefixGeometry p).terminalVariables → ∀ w ∈ (profilePrefixGeometry p).terminalVariables, (profilePrefixGeometry p).variablePosition ↑v ≠ (profilePrefixGeometry p).variablePosition w

An auxiliary variable never occupies a source boundary port.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_clause_bounds (p : ClauseProfile) (i : Fin (profilePrefixGeometry p).clausePositions.length) : have q := (profilePrefixGeometry p).clausePosition ↑i; 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000

Every listed clause position lies in the inner template's closed square.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_incidence_points_bounds (p : ClauseProfile) (e : LocalIncidence) : e ∈ (profilePrefixGeometry p).incidenceRoutes → ∀ q ∈ e.2.2, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000

All listed incidence points lie in the inner square, independently of the expensive continuous pair-contact certificate.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_clause_ne_terminal (p : ClauseProfile) (i : Fin (profilePrefixGeometry p).clausePositions.length) (w : ℕ) : w ∈ (profilePrefixGeometry p).terminalVariables → (profilePrefixGeometry p).clausePosition ↑i ≠ (profilePrefixGeometry p).variablePosition w

No clause vertex occupies a source boundary port.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_terminal_unique (p : ClauseProfile) (e : LocalIncidence) : e ∈ (profilePrefixGeometry p).incidenceRoutes → e.2.1 ∈ (profilePrefixGeometry p).terminalVariables → ∀ f ∈ (profilePrefixGeometry p).incidenceRoutes, e.2.1 = f.2.1 → e = f

Each source placeholder belongs to exactly one local incidence.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_shared_variable_not_terminal (p : ClauseProfile) {e f : LocalIncidence} (he : e ∈ (profilePrefixGeometry p).incidenceRoutes) (hf : f ∈ (profilePrefixGeometry p).incidenceRoutes) (hne : e ≠ f) (hv : e.2.1 = f.2.1) : e.2.1 ∉ (profilePrefixGeometry p).terminalVariables

Two different incidences can share only an actual auxiliary variable, never a source placeholder that will be removed by the global drawing compiler.

def Cslib.Complexity.SAT.ExactOne.profileCollarRoute (p : ClauseProfile) (s : PortAssignment) (e : LocalIncidence) : Orthogonal.Route

The finite route actually used by the collared incidence constructor.

theorem Cslib.Complexity.SAT.ExactOne.profile_prefix_incidence_bounds (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {e : LocalIncidence} (he : e ∈ (profilePrefixGeometry p).incidenceRoutes) (q : Orthogonal.Point) : q ∈ e.2.2 → 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000

Every actual inner prefix lies in the common side-180000 square.

theorem Cslib.Complexity.SAT.ExactOne.collaredProfile_incidence_orthogonal (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e : LocalIncidence} (he : e ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) : Orthogonal.IsOrthogonal e.2.2

The actual collared incidence routes are properly orthogonal in every ordered port assignment. The profile certificate is supplied separately to keep the data compiler lightweight.

theorem Cslib.Complexity.SAT.ExactOne.collaredProfile_incidence_isSimple (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e : LocalIncidence} (he : e ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) : Orthogonal.IsSimple e.2.2

The actual collared incidence routes are simple over their full real support.

theorem Cslib.Complexity.SAT.ExactOne.profileCollarRoute_contact (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e f : LocalIncidence} (he : e ∈ (profilePrefixGeometry p).incidenceRoutes) (hf : f ∈ (profilePrefixGeometry p).incidenceRoutes) (hne : e ≠ f) {z : ℝ × ℝ} (hz : z ∈ Orthogonal.support (profileCollarRoute p s e)) (hw : z ∈ Orthogonal.support (profileCollarRoute p s f)) : ∃ q ∈ (profilePrefixGeometry p).commonEndpoints e f, z = collarReal (collarReflected s) (Orthogonal.realPoint q)

The annular connectors introduce no new contacts between different incidence routes. Every contact is the common affine placement of an original permitted local endpoint.

theorem Cslib.Complexity.SAT.ExactOne.profileCollarRoute_auxiliary_not_mem_support (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e : LocalIncidence} (he : e ∈ (profilePrefixGeometry p).incidenceRoutes) (v : Fin (profilePrefixGeometry p).variablePositions.length) (ht : ↑v ∉ (profilePrefixGeometry p).terminalVariables) (hv : ↑v ≠ e.2.1) : Orthogonal.realPoint (collarPoint (collarReflected s) ((profilePrefixGeometry p).variablePosition ↑v)) ∉ Orthogonal.support (profileCollarRoute p s e)

A collared incidence avoids every nonincident actual auxiliary vertex.

theorem Cslib.Complexity.SAT.ExactOne.profileCollarRoute_clause_not_mem_support (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e : LocalIncidence} (he : e ∈ (profilePrefixGeometry p).incidenceRoutes) (i : Fin (profilePrefixGeometry p).clausePositions.length) (hi : ↑i ≠ e.1) : Orthogonal.realPoint (collarPoint (collarReflected s) ((profilePrefixGeometry p).clausePosition ↑i)) ∉ Orthogonal.support (profileCollarRoute p s e)

A collared incidence avoids every nonincident actual clause vertex.

theorem Cslib.Complexity.SAT.ExactOne.profileCollarRoute_source_not_mem_support (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e : LocalIncidence} (he : e ∈ (profilePrefixGeometry p).incidenceRoutes) {v : ℕ} (ht : v ∈ (profilePrefixGeometry p).terminalVariables) (hv : v ≠ e.2.1) : Orthogonal.realPoint (collarOuterPort (s.side (terminalIndex (profilePrefixGeometry p) v))) ∉ Orthogonal.support (profileCollarRoute p s e)

A collared incidence avoids every other exposed source endpoint.

theorem Cslib.Complexity.SAT.ExactOne.profileCollarRoute_outer_boundary_contact (p : ClauseProfile) (h : (profilePrefixGeometry p).PrefixCheck) {s : PortAssignment} (hs : s.Distinct) {e : LocalIncidence} (he : e ∈ (profilePrefixGeometry p).incidenceRoutes) {z : ℝ × ℝ} (hz : z ∈ Orthogonal.support (profileCollarRoute p s e)) (hb : z ∈ Orthogonal.support collarBoundaryRoute) : e.2.1 ∈ (profilePrefixGeometry p).terminalVariables ∧ z = Orthogonal.realPoint (collarOuterPort (s.side (terminalIndex (profilePrefixGeometry p) e.2.1)))

A collared route can touch the complete outer perimeter only at its own source endpoint; an incidence to an internal auxiliary never touches that perimeter.