The classification theorem (A7)

Theorem thm:classification: for a pair-source scenario with binary observations, some finite order of the Navascués–Wolfe test (equivalently of the ancestral-independence test, equivalently of the recursively expressible test) equals the compatible set iff every connected component is a double-star (classification_NW_lib, classification_AI, classification_exp), with the nontermination half nontermination_of_not_doubleStar assembled from the cycle and five-path witnesses, transport, exhaustion, and local flips. Everything here is proved.

theorem TriangleInflation.Graph.nontermination_of_not_doubleStar (Γ : PairGraph) (hnot : ¬IsDoubleStarForest Γ.G) (t : ℕ) (ht : 1 ≤ t) : ∃ (P : GTarget Γ), IsLaw P ∧ (∀ (w : Γ.V → Bool), 0 < P w) ∧ GExpFeasible Γ t P ∧ ¬GCompatible Γ P

AUDIT-NOTES A7, the nontermination half. A pair graph with a component that is not a double star carries, at every order, a full-support target that passes the recursively expressible test and is incompatible. Full support comes from independent local flips at every copied observation, which preserve symmetry and all AI products.

theorem TriangleInflation.Graph.classification_NW_lib (Γ : PairGraph) : (∃ (t : ℕ), 1 ≤ t ∧ ∀ (P : GTarget Γ), IsLaw P → (GNWFeasible Γ t P ↔ GCompatible Γ P)) ↔ IsDoubleStarForest Γ.G

AUDIT-NOTES A7, the classification theorem for the Navascués–Wolfe hierarchy: some finite order of the hierarchy equals the compatible set exactly when every connected component of the graph is a double star.

The plain name TriangleInflation.Graph.classification_NW is reserved for the registry statement, which PalomarSolutions/TriangleInflationClassification.lean declares and discharges by this theorem; Comparator identifies the Challenge and the Solution by that one name.

theorem TriangleInflation.Graph.classification_AI (Γ : PairGraph) : (∃ (t : ℕ), 1 ≤ t ∧ ∀ (P : GTarget Γ), IsLaw P → (GAIFeasible Γ t P ↔ GCompatible Γ P)) ↔ IsDoubleStarForest Γ.G

AUDIT-NOTES A7 for the ancestral-independence hierarchy.

theorem TriangleInflation.Graph.classification_exp (Γ : PairGraph) : (∃ (t : ℕ), 1 ≤ t ∧ ∀ (P : GTarget Γ), IsLaw P → (GExpFeasible Γ t P ↔ GCompatible Γ P)) ↔ IsDoubleStarForest Γ.G

AUDIT-NOTES A7 for the recursively expressible hierarchy.