Certified source-boundary prefixes for positive exact-one profiles

The actual fifteen positive replacement profiles have their source incidences extended to the cell boundary. The resulting finite certificates include all full real route contacts, simplicity, nonincident vertices and the isolation of the cell boundary.

Main definitions

• profilePrefixGeometry: the actual profile with source endpoints at boundary ports.

Main results

• profilePrefixGeometry_check: full continuous certificates for all fifteen boundary profiles.
• profilePrefixGeometry_signature: exact alignment with the positive formula compiler.

References

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

theorem Cslib.Complexity.SAT.ExactOne.profilePrefixGeometry_check (p : ClauseProfile) : (profilePrefixGeometry p).PrefixCheck

All fifteen source-boundary prefix drawings have full continuous certificates.

theorem Cslib.Complexity.SAT.ExactOne.profilePrefixGeometry_signature (p : ClauseProfile) : List.map (fun (e : LocalIncidence) => (e.clauseIndex, e.variableIndex)) (profilePrefixGeometry p).incidenceRoutes = profileSignature p

Extending source incidences preserves the exact logical incidence signature.

theorem Cslib.Complexity.SAT.ExactOne.profilePrefixGeometry_terminal_position (p : ClauseProfile) (i : Fin (List.length (profileSource p))) : (profilePrefixGeometry p).variablePosition ((profileGeometry p).terminalVariables.getD (↑i) 0) = (profileGeometry p).boundaryPorts.getD ↑i (0, 0)

Each exposed source position is exactly its assigned boundary port after extension.

theorem Cslib.Complexity.SAT.ExactOne.profilePrefixGeometry_auxiliary_interior (p : ClauseProfile) (i : Fin (profilePrefixGeometry p).variablePositions.length) : ↑i ∉ (profilePrefixGeometry p).terminalVariables → have q := (profilePrefixGeometry p).variablePosition ↑i; 0 < q.1 ∧ q.1 < 180000 ∧ 0 < q.2 ∧ q.2 < 180000

All auxiliary variables remain strictly inside the profile cell.

theorem Cslib.Complexity.SAT.ExactOne.profilePrefixGeometry_clause_interior (p : ClauseProfile) (q : Orthogonal.Point) : q ∈ (profilePrefixGeometry p).clausePositions → 0 < q.1 ∧ q.1 < 180000 ∧ 0 < q.2 ∧ q.2 < 180000

All actual clause vertices remain strictly inside the profile cell.

theorem Cslib.Complexity.SAT.ExactOne.profilePrefixGeometry_terminal_degree (p : ClauseProfile) (v : ℕ) : v ∈ (profilePrefixGeometry p).terminalVariables → List.count v (List.map (fun (e : LocalIncidence) => e.variableIndex) (profilePrefixGeometry p).incidenceRoutes) = 1

Source-boundary extension preserves the single incidence at every source placeholder.

theorem Cslib.Complexity.SAT.ExactOne.profilePrefixGeometry_costs (p : ClauseProfile) : (profilePrefixGeometry p).variablePositions.length ≤ 29 ∧ (profilePrefixGeometry p).clausePositions.length ≤ 22 ∧ (profilePrefixGeometry p).incidenceRoutes.length ≤ 66 ∧ (List.map (fun (e : LocalIncidence) => List.length e.route - 1) (profilePrefixGeometry p).incidenceRoutes).sum ≤ 113 ∧ (List.map (fun (e : LocalIncidence) => Orthogonal.wireLength e.route) (profilePrefixGeometry p).incidenceRoutes).sum ≤ 652600 ∧ (profilePrefixGeometry p).size = 180000

The actual finite prefix tables have constant vertex, route, segment and wire costs.