Documentation

LeanPool.InflationTermination.TriangleInflation.Graph.Classification

The classification theorem (A7) #

Statements split from the original Statements.lean skeleton (one file per proving task). The mathematics is AUDIT-NOTES A7 and papers/.../sections/13-classification.tex.

The four theorems below are proved by assembling the results of the other files in this directory, together with the bridging lemmas of the first three sections: connectivity of the named cycle and path scenarios, the fact that a target passing the order-t test is a law, the total variation cost of a local flip, and the passage to a connected component.

A7: the classification theorem #

Bridging lemmas: connectivity of the named scenarios #

source
theorem TriangleInflation.Graph.cycleAdj_connected (m : ℕ) (hm : 3 ≤ m) :
(cycleAdj m).Connected

The cycle graph is connected.

source
theorem TriangleInflation.Graph.pathAdj_five_connected :
(pathAdj 5).Connected

The five-vertex path graph is connected.

Bridging lemmas: pushforwards, laws and total variation #

source
theorem TriangleInflation.Graph.isLaw_of_gAIFeasible (Γ : PairGraph) (t : ℕ) (ht : 1 ≤ t) (P : GTarget Γ) (h : GAIFeasible Γ t P) :
IsLaw P

A target that passes the order-t ancestral-independence test, t ≥ 1, is a law: the witness restricted to one copied original scenario has the target as its law.

source
theorem TriangleInflation.Graph.distToCompatible_le (Γ : PairGraph) (P Q : GTarget Γ) (hQ : GCompatible Γ Q) :
distToCompatible Γ P ≤ dTV P Q

The distance to the compatible set is at most the distance to any compatible law.

Bridging lemmas: how far a local flip moves a law #

source
theorem TriangleInflation.Graph.dTV_flipLaw_le {ι : Type} [Fintype ι] [DecidableEq ι] (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) (P : (ι → Bool) → ℝ) (hP : IsLaw P) :
dTV P (flipLaw η P) ≤ ↑(Fintype.card ι) * η

Independent flips with probability η move a law by at most |ι| η in total variation.

Bridging lemmas: passing to a connected component #

source
theorem TriangleInflation.Graph.exists_bad_component (Γ : PairGraph) (hnot : ¬IsDoubleStarForest Γ.G) :
∃ (C : Γ.G.ConnectedComponent), ¬IsDoubleStarForest C.toSimpleGraph

If no connected component is a double star, neither is the graph.

source
noncomputable def TriangleInflation.Graph.componentPairGraph (Γ : PairGraph) (C : Γ.G.ConnectedComponent) :
PairGraph

The pair-source scenario carried by one connected component.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TriangleInflation.Graph.componentPairGraph_embed (Γ : PairGraph) (C : Γ.G.ConnectedComponent) :
    ∃ (ρ : (componentPairGraph Γ C).V → Γ.V), Function.Injective ρ ∧ ∀ (a b : (componentPairGraph Γ C).V), (componentPairGraph Γ C).G.Adj a b ↔ Γ.G.Adj (ρ a) (ρ b)

    The inclusion of a component scenario into the ambient scenario is an induced embedding.