# Theorem 2 establishes that applying standard constraint-based algorithms such as PC or GES (Algorithm 1) to G^+ is sound and complete: oriented edges correspond to true causal relations, while unoriented edges may reflect the presence of selection (Section 3, Theorem 2, Algorithm 1).

**Verdict: VERIFIED under the theorem's population faithfulness premise.**

The exact audit computes the CPDAG of every `G^+`, then checks all three printed clauses. Orientation completeness is not inferred from undirected notation: the code searches all source models with the same CPDAG and requires an alternative relation for each unoriented edge.

| Clause | Passed | Tested |
| --- | ---: | ---: |
| adjacency soundness and completeness | 52,128 | 52,128 |
| orientation soundness | 2,640 | 2,640 |
| unoriented-edge completeness | 39,030 | 39,030 |
| CPDAG implementation vs causal-learn | 600 | 600 |

PC and GES are also executed in the 750-run native Section 5 pipeline. Those finite results are deliberately not used to erase Theorem 2's premise: at `N=5,000`, estimated CIs do not always equal population CIs.

## Destructive control

A compelled orientation is reversed in every one of 328 eligible sampled models. The source-direction and non-selection-head checker rejects 328/328 corruptions.

## Evidence

Exact clauses: `outputs/exact_graph_audit.json`. Independent CPDAG oracle: `outputs/oracle_gates.json`. Native PC/GES: `outputs/synthetic_native_pipeline.json`. Control: `outputs/destructive_controls.json`.

## Limitations

The verified theorem assumes sufficiently large samples and faithfulness. The package separately reports poor finite-sample orientation soundness, so this verdict must not be read as a universal `N=5,000` guarantee.