Double-star forests carry the reconstruction data

The graph-theoretic step of the double-star reconstruction (AUDIT-NOTES A3, Theorem thm:doublestar in the binary case): every double-star forest carries a DSStruct (exists_dsStruct), and hence order-two Navascués–Wolfe feasibility characterizes compatibility on such scenarios (doubleStar_terminates). Everything here is proved.

The graph-theoretic input

The one step of AUDIT-NOTES A3 that the audited library leaves open: a double-star forest carries the combinatorial data of a DSStruct. Each component is a tree of diameter at most three with at least two vertices, so its vertices of degree at least two are pairwise adjacent (otherwise two private neighbours are at distance at least four) and there are at most two of them (three would close a triangle). Take those as the two centres when there are two; when there is one, promote one of its neighbours to the second centre; when there is none, the component is a single source and both of its ends are centres. Every remaining vertex has degree one and is joined to one of the two centres.

DSStructAux carries that argument: DSStructAux.exists_centre is the combinatorial statement for one component, DSStructAux.CentreData packages the choice of centres for every component, and DSStructAux.CentreData.toDSStruct reads the fields of a DSStruct off it.

def TriangleInflation.Graph.DSStructAux.Big {V : Type u_1} (G : SimpleGraph V) (v : V) : Prop

A vertex with two distinct neighbours.

Equations

• TriangleInflation.Graph.DSStructAux.Big G v = ∃ (x : V) (y : V), G.Adj v x ∧ G.Adj v y ∧ x ≠ y

theorem TriangleInflation.Graph.DSStructAux.down_unique {V : Type u_1} {G : SimpleGraph V} (hac : G.IsAcyclic) {z u n n' : V} (hr : G.Reachable z u) (h1 : G.Adj u n) (h2 : G.Adj u n') (hd1 : G.dist z u = G.dist z n + 1) (hd2 : G.dist z u = G.dist z n' + 1) : n = n'

In a forest, a vertex has at most one neighbour closer to a given vertex.

theorem TriangleInflation.Graph.DSStructAux.exists_up {V : Type u_1} {G : SimpleGraph V} (hac : G.IsAcyclic) {z u : V} (hu : Big G u) (hr : G.Reachable z u) : ∃ (x : V), G.Adj u x ∧ G.dist z x = G.dist z u + 1

A vertex with two neighbours has one strictly farther from any given vertex.

theorem TriangleInflation.Graph.DSStructAux.dist_le_one_of_big {V : Type u_1} {G : SimpleGraph V} (hac : G.IsAcyclic) (hdiam : ∀ (u v : V), G.Reachable u v → G.dist u v ≤ 3) {u v : V} (hu : Big G u) (hv : Big G v) (huv : G.Reachable u v) : G.dist u v ≤ 1

Two vertices of degree at least two in a double-star forest are at distance at most one.

theorem TriangleInflation.Graph.DSStructAux.no_triangle {V : Type u_1} {G : SimpleGraph V} (hac : G.IsAcyclic) {a b c : V} (hab : G.Adj a b) (hac' : G.Adj a c) (hbc : G.Adj b c) : False

A forest has no triangle.

theorem TriangleInflation.Graph.DSStructAux.adj_of_big {V : Type u_1} {G : SimpleGraph V} (hac : G.IsAcyclic) (hdiam : ∀ (u v : V), G.Reachable u v → G.dist u v ≤ 3) {u v : V} (hu : Big G u) (hv : Big G v) (huv : G.Reachable u v) (hne : u ≠ v) : G.Adj u v

Two distinct vertices of degree at least two in a double-star forest are adjacent.

theorem TriangleInflation.Graph.DSStructAux.nbr_eq_or_big {V : Type u_1} {G : SimpleGraph V} {a u c : V} (hau : G.Reachable u a) (hne : u ≠ a) (huniq : ∀ (x : V), G.Adj u x → x = c) : c = a ∨ Big G c

The neighbour of a degree-one vertex is either the base point or has degree at least two.

theorem TriangleInflation.Graph.DSStructAux.exists_unique_nbr {V : Type u_1} {G : SimpleGraph V} (hiso : ∀ (v : V), ∃ (w : V), G.Adj v w) {u : V} (hu : ¬Big G u) : ∃ (c : V), G.Adj u c ∧ ∀ (x : V), G.Adj u x → x = c

A vertex that is not Big has exactly one neighbour.

theorem TriangleInflation.Graph.DSStructAux.exists_centre {V : Type u_1} {G : SimpleGraph V} (hac : G.IsAcyclic) (hdiam : ∀ (u v : V), G.Reachable u v → G.dist u v ≤ 3) (hiso : ∀ (v : V), ∃ (w : V), G.Adj v w) (r : V) : ∃ (ab : V × V), G.Adj ab.1 ab.2 ∧ G.Reachable r ab.1 ∧ ∀ (u : V), G.Reachable r u → u = ab.1 ∨ u = ab.2 ∨ ∃ (c : V), (c = ab.1 ∨ c = ab.2) ∧ G.Adj u c ∧ ∀ (x : V), G.Adj u x → x = c

The combinatorics of a double-star forest. Every component of a double-star forest without isolated vertices has two adjacent centres, and every other vertex of the component has exactly one neighbour, which is one of the two centres.

Incidence

theorem TriangleInflation.Graph.DSStructAux.mem_inc_iff {Γ : PairGraph} (v : Γ.V) (e : Γ.Edge) : e ∈ Γ.inc v ↔ v ∈ ↑e

theorem TriangleInflation.Graph.DSStructAux.edge_adj {Γ : PairGraph} {e : Γ.Edge} {p q : Γ.V} (h : ↑e = s(p, q)) : Γ.G.Adj p q

theorem TriangleInflation.Graph.DSStructAux.reach_of_mem_edge {Γ : PairGraph} {e : Γ.Edge} {v v' : Γ.V} (h : v ∈ ↑e) (h' : v' ∈ ↑e) : Γ.G.Reachable v v'

Centre data

structure TriangleInflation.Graph.DSStructAux.CentreData (Γ : PairGraph) : Type

The two centres of the component of each vertex of a double-star forest.

• A : Γ.V → Γ.V

  The first centre of the component.

• B : Γ.V → Γ.V

  The second centre of the component.

• adj (v : Γ.V) : Γ.G.Adj (self.A v) (self.B v)
• reachA (v : Γ.V) : Γ.G.Reachable v (self.A v)
• constA (u v : Γ.V) : Γ.G.Reachable u v → self.A u = self.A v
• constB (u v : Γ.V) : Γ.G.Reachable u v → self.B u = self.B v
• cover (v : Γ.V) : v = self.A v ∨ v = self.B v ∨ ∃ (c : Γ.V), (c = self.A v ∨ c = self.B v) ∧ Γ.G.Adj v c ∧ ∀ (x : Γ.V), Γ.G.Adj v x → x = c

noncomputable def TriangleInflation.Graph.DSStructAux.compRep (Γ : PairGraph) (v : Γ.V) : Γ.V

A chosen representative of the component of a vertex.

Equations

• TriangleInflation.Graph.DSStructAux.compRep Γ v = ⋯.some

theorem TriangleInflation.Graph.DSStructAux.reachable_compRep (Γ : PairGraph) (v : Γ.V) : Γ.G.Reachable v (compRep Γ v)

theorem TriangleInflation.Graph.DSStructAux.compRep_eq (Γ : PairGraph) {u v : Γ.V} (h : Γ.G.Reachable u v) : compRep Γ u = compRep Γ v

theorem TriangleInflation.Graph.DSStructAux.exists_centreData (Γ : PairGraph) (hG : IsDoubleStarForest Γ.G) : Nonempty (CentreData Γ)

theorem TriangleInflation.Graph.DSStructAux.CentreData.reachB {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : Γ.G.Reachable v (C.B v)

theorem TriangleInflation.Graph.DSStructAux.CentreData.A_ne_B {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.A v ≠ C.B v

theorem TriangleInflation.Graph.DSStructAux.CentreData.A_A {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.A (C.A v) = C.A v

theorem TriangleInflation.Graph.DSStructAux.CentreData.B_A {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.B (C.A v) = C.B v

theorem TriangleInflation.Graph.DSStructAux.CentreData.A_B {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.A (C.B v) = C.A v

theorem TriangleInflation.Graph.DSStructAux.CentreData.B_B {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.B (C.B v) = C.B v

def TriangleInflation.Graph.DSStructAux.CentreData.mate {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : Γ.V

The mate of a vertex: the partner centre of a centre, the centre of a leaf.

Equations

• C.mate v = if v = C.A v then C.B v else if v = C.B v then C.A v else if Γ.G.Adj v (C.A v) then C.A v else C.B v

theorem TriangleInflation.Graph.DSStructAux.CentreData.mate_ctrA {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.mate (C.A v) = C.B v

theorem TriangleInflation.Graph.DSStructAux.CentreData.mate_ctrB {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.mate (C.B v) = C.A v

theorem TriangleInflation.Graph.DSStructAux.CentreData.mate_of_leaf {Γ : PairGraph} (C : CentreData Γ) {v : Γ.V} (h1 : v ≠ C.A v) (h2 : v ≠ C.B v) : Γ.G.Adj v (C.mate v) ∧ (C.mate v = C.A v ∨ C.mate v = C.B v) ∧ ∀ (x : Γ.V), Γ.G.Adj v x → x = C.mate v

theorem TriangleInflation.Graph.DSStructAux.CentreData.mate_adj {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : Γ.G.Adj v (C.mate v)

theorem TriangleInflation.Graph.DSStructAux.CentreData.mate_mem {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.mate v = C.A v ∨ C.mate v = C.B v

theorem TriangleInflation.Graph.DSStructAux.CentreData.mate_uniq {Γ : PairGraph} (C : CentreData Γ) {v : Γ.V} (h1 : v ≠ C.A v) (h2 : v ≠ C.B v) (x : Γ.V) : Γ.G.Adj v x → x = C.mate v

theorem TriangleInflation.Graph.DSStructAux.CentreData.A_mate {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.A (C.mate v) = C.A v

theorem TriangleInflation.Graph.DSStructAux.CentreData.B_mate {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.B (C.mate v) = C.B v

theorem TriangleInflation.Graph.DSStructAux.CentreData.mate_mate {Γ : PairGraph} (C : CentreData Γ) {v : Γ.V} (h : v = C.A v ∨ v = C.B v) : C.mate (C.mate v) = v

def TriangleInflation.Graph.DSStructAux.CentreData.edgeAt {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : Γ.Edge

The edge that carries a vertex: its unique source when it is a leaf, the centre source of its component when it is a centre.

Equations

• C.edgeAt v = ⟨s(v, C.mate v), ⋯⟩

def TriangleInflation.Graph.DSStructAux.CentreData.root {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : Γ.Edge

The centre source of the component of a vertex.

Equations

• C.root v = ⟨s(C.A v, C.B v), ⋯⟩

def TriangleInflation.Graph.DSStructAux.CentreData.leafB {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : Bool

Is the vertex a leaf?

Equations

• C.leafB v = decide (v ≠ C.A v ∧ v ≠ C.B v)

theorem TriangleInflation.Graph.DSStructAux.CentreData.leafB_true {Γ : PairGraph} (C : CentreData Γ) {v : Γ.V} : C.leafB v = true ↔ v ≠ C.A v ∧ v ≠ C.B v

theorem TriangleInflation.Graph.DSStructAux.CentreData.leafB_false {Γ : PairGraph} (C : CentreData Γ) {v : Γ.V} : C.leafB v = false ↔ v = C.A v ∨ v = C.B v

theorem TriangleInflation.Graph.DSStructAux.CentreData.edgeAt_val {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : ↑(C.edgeAt v) = s(v, C.mate v)

theorem TriangleInflation.Graph.DSStructAux.CentreData.edgeAt_inc {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.edgeAt v ∈ Γ.inc v

theorem TriangleInflation.Graph.DSStructAux.CentreData.edgeAt_inc_mate {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.edgeAt v ∈ Γ.inc (C.mate v)

theorem TriangleInflation.Graph.DSStructAux.CentreData.edgeAt_mem {Γ : PairGraph} (C : CentreData Γ) (v u : Γ.V) (h : C.edgeAt v ∈ Γ.inc u) : u = v ∨ u = C.mate v

theorem TriangleInflation.Graph.DSStructAux.CentreData.mate_not_leaf {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.leafB (C.mate v) = false

theorem TriangleInflation.Graph.DSStructAux.CentreData.mate_ne {Γ : PairGraph} (C : CentreData Γ) (v : Γ.V) : C.mate v ≠ v

theorem TriangleInflation.Graph.DSStructAux.CentreData.leaf_inc {Γ : PairGraph} (C : CentreData Γ) {v : Γ.V} (h : C.leafB v = true) : Γ.inc v = {C.edgeAt v}

theorem TriangleInflation.Graph.DSStructAux.CentreData.edgeAt_eq_iff {Γ : PairGraph} (C : CentreData Γ) (u v : Γ.V) : C.edgeAt u = C.edgeAt v ↔ u = v ∧ C.mate u = C.mate v ∨ u = C.mate v ∧ C.mate u = v

theorem TriangleInflation.Graph.DSStructAux.CentreData.fib_leaf {Γ : PairGraph} (C : CentreData Γ) {v : Γ.V} (h : C.leafB v = true) : {u : Γ.V | C.edgeAt u = C.edgeAt v} = {v}

theorem TriangleInflation.Graph.DSStructAux.CentreData.fib_ctr {Γ : PairGraph} (C : CentreData Γ) {v : Γ.V} (h : C.leafB v = false) : {u : Γ.V | C.edgeAt u = C.edgeAt v} = {v, C.mate v}

theorem TriangleInflation.Graph.DSStructAux.CentreData.root_leaf {Γ : PairGraph} (C : CentreData Γ) {v : Γ.V} (_h : C.leafB v = true) : C.root v = C.edgeAt (C.mate v)

theorem TriangleInflation.Graph.DSStructAux.CentreData.root_ctr {Γ : PairGraph} (C : CentreData Γ) {v : Γ.V} (h : C.leafB v = false) : C.root v = C.edgeAt v

theorem TriangleInflation.Graph.DSStructAux.CentreData.root_eq_of_reach {Γ : PairGraph} (C : CentreData Γ) {u v : Γ.V} (h : Γ.G.Reachable u v) : C.root u = C.root v

theorem TriangleInflation.Graph.DSStructAux.CentreData.comp_sourceDisjoint {Γ : PairGraph} (C : CentreData Γ) (y y' : Γ.Edge) (hy : y ≠ y') : Disjoint ({v : Γ.V | C.root v = y}.biUnion Γ.inc) ({v : Γ.V | C.root v = y'}.biUnion Γ.inc)

theorem TriangleInflation.Graph.DSStructAux.CentreData.edgeAt_surj {Γ : PairGraph} (C : CentreData Γ) (e : Γ.Edge) : ∃ (v : Γ.V), C.edgeAt v = e

noncomputable def TriangleInflation.Graph.DSStructAux.CentreData.toDSStruct {Γ : PairGraph} (C : CentreData Γ) : DSStruct Γ

The combinatorial data of a double-star forest carried by its centre data.

Equations

• One or more equations did not get rendered due to their size.

theorem TriangleInflation.Graph.exists_dsStruct (Γ : PairGraph) (hG : IsDoubleStarForest Γ.G) : Nonempty (DSStruct Γ)

Every double-star forest carries a DSStruct.

The double-star reconstruction

theorem TriangleInflation.Graph.doubleStar_terminates (Γ : PairGraph) (hG : IsDoubleStarForest Γ.G) (P : GTarget Γ) (hP : IsLaw P) : GNWFeasible Γ 2 P ↔ GCompatible Γ P

AUDIT-NOTES A3, the double-star reconstruction, in the binary case where the alphabet bound is T = 2. For a scenario whose components are all double stars, order-two Navascués–Wolfe feasibility already characterizes compatibility. The proof reconstructs a model: source-disjoint independence at order two makes the leaves independent, conditioning on the event that each leaf's two copies list both symbols gives the joint conditional law of the two centres, and that law is the source law of a fresh central source carrying the pair of response tables.