Double-star reconstruction (A3)

AUDIT-NOTES A3 and paper Section sec:doublestar, in the binary case T = 2.

The analytic content of the reconstruction is proved here in full. Everything rests on one identity about a Navascués–Wolfe witness at order two, gTwist_law: after relabelling the copy indices of each source by an arbitrary permutation, the t rows read on the diagonal are still t independent copies of the target. From it follow, in order,

• blockMarg_union_of_sourceDisjoint — source-disjoint blocks of vertices are independent under the target (step (i) of the paper proof, and the pair-source form of AUDIT-NOTES A3(i)), and its iterate blockMarg_biUnion_of_sourceDisjoint;
• centreLeaf_mass — conditioning on the event that each leaf's two copies list the prescribed array, the joint law of the two centre observations is the conditional law of the two centres given the leaf values (steps (ii)–(iii), the finite-order step);
• DSStruct.ctrFactor_mul — the component identity that the reconstruction needs;
• gCompatible_of_localDecoder — a model whose responses are deterministic local readings of a decoder, packaged so that no dependent latent types appear;
• DSStruct.gCompatible_of_dsStruct — the reconstruction (step (iv)).

What is not proved here is the purely graph-theoretic step exists_dsStruct: that a double-star forest carries the combinatorial data DSStruct. That step, exists_dsStruct, and the theorem doubleStar_terminates assembled from it, live in InflationGraphOpen/DoubleStar.lean; everything in this file is proved.

Relabelling the copy indices

The whole finite-order content of the double-star reconstruction is a single identity about a Navascués–Wolfe witness: after relabelling the copy indices of each source by a permutation π, the t diagonal rows are still t independent copies of the target. Sections (i)–(iii) of the paper proof are all read off from it.

theorem TriangleInflation.Graph.gPerm_gPerm {Γ : PairGraph} {t : ℕ} (π ρ : Γ.Edge → Equiv.Perm (Fin t)) (o : GObs Γ t) : gPerm π (gPerm ρ o) = gPerm (fun (e : Γ.Edge) => Equiv.trans (ρ e) (π e)) o

Relabelling copied observations composes.

theorem TriangleInflation.Graph.gRelabel_gRelabel {Γ : PairGraph} {t : ℕ} (π ρ : Γ.Edge → Equiv.Perm (Fin t)) (ω : GAssign Γ t) : gRelabel π (gRelabel ρ ω) = gRelabel (fun (e : Γ.Edge) => Equiv.trans (π e) (ρ e)) ω

Relabelling assignments composes.

theorem TriangleInflation.Graph.gRelabel_refl {Γ : PairGraph} {t : ℕ} (ω : GAssign Γ t) : gRelabel (fun (x : Γ.Edge) => Equiv.refl (Fin t)) ω = ω

The identity relabelling.

def TriangleInflation.Graph.gRelabelEquiv {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) : GAssign Γ t ≃ GAssign Γ t

Relabelling by π is a bijection of assignments, with inverse the relabelling by π⁻¹.

Equations

• TriangleInflation.Graph.gRelabelEquiv π = { toFun := TriangleInflation.Graph.gRelabel π, invFun := TriangleInflation.Graph.gRelabel fun (e : Γ.Edge) => (π e)⁻¹, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TriangleInflation.Graph.gRelabelEquiv_apply {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) (ω : GAssign Γ t) : (gRelabelEquiv π) ω = gRelabel π ω

theorem TriangleInflation.Graph.pushforward_comp_gRelabel {Γ : PairGraph} {t : ℕ} {β : Type u_1} [DecidableEq β] {Δ : GAssign Γ t → ℝ} (hsym : GSymmetric t Δ) (π : Γ.Edge → Equiv.Perm (Fin t)) (F : GAssign Γ t → β) : (pushforward Δ fun (ω : GAssign Γ t) => F (gRelabel π ω)) = pushforward Δ F

A symmetric witness has the same pushforward along F and along F ∘ gRelabel π.

def TriangleInflation.Graph.gTwist {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) (ω : GAssign Γ t) : Fin t → Γ.V → Bool

The rows read by a table after relabelling the copy indices of each source: row r reads, at every vertex, the copy π_e r of each incident source e. For π = 1 these are the t diagonal rows.

Equations

• TriangleInflation.Graph.gTwist π ω r v = ω ⟨v, fun (e : ↥(Γ.inc v)) => (π ↑e) r⟩

theorem TriangleInflation.Graph.gTwist_eq_readDiag {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) (ω : GAssign Γ t) : gTwist π ω = readDiag (gRelabel π ω)

theorem TriangleInflation.Graph.gTwist_refl {Γ : PairGraph} {t : ℕ} (ω : GAssign Γ t) : gTwist (fun (x : Γ.Edge) => Equiv.refl (Fin t)) ω = readDiag ω

theorem TriangleInflation.Graph.gTwist_law {Γ : PairGraph} {t : ℕ} {Δ : GAssign Γ t → ℝ} {P : GTarget Γ} (hsym : GSymmetric t Δ) (hdiag : pushforward Δ readDiag = gTensorPow t P) (π : Γ.Edge → Equiv.Perm (Fin t)) : pushforward Δ (gTwist π) = gTensorPow t P

The twisted-row law. For a symmetric witness whose diagonal law is the t-fold tensor power of the target, the t rows read after any relabelling of the copy indices are again t independent copies of the target. This is the only property of the witness that the double-star reconstruction uses.

Reading an expectation off a pushforward

theorem TriangleInflation.Graph.sum_mul_pushforward {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (Δ : α → ℝ) (F : α → β) (g : β → ℝ) : ∑ a : α, g (F a) * Δ a = ∑ b : β, g b * pushforward Δ F b

Expectations only see the pushforward.

theorem TriangleInflation.Graph.sum_gTwist {Γ : PairGraph} {t : ℕ} {Δ : GAssign Γ t → ℝ} {P : GTarget Γ} (hsym : GSymmetric t Δ) (hdiag : pushforward Δ readDiag = gTensorPow t P) (π : Γ.Edge → Equiv.Perm (Fin t)) (g : (Fin t → Γ.V → Bool) → ℝ) : ∑ ω : GAssign Γ t, g (gTwist π ω) * Δ ω = ∑ u : Fin t → Γ.V → Bool, g u * gTensorPow t P u

The expectation of a function of the twisted rows.

theorem TriangleInflation.Graph.sum_fin_two_pi {α : Type u_1} {M : Type u_2} [Fintype α] [AddCommMonoid M] (F : (Fin 2 → α) → M) : ∑ u : Fin 2 → α, F u = ∑ a : α, ∑ b : α, F ![a, b]

Sums over Fin 2 → α as double sums.

theorem TriangleInflation.Graph.gTwist_apply_eq_readDiag {Γ : PairGraph} {t : ℕ} {π : Γ.Edge → Equiv.Perm (Fin t)} {ω : GAssign Γ t} {r s : Fin t} {v : Γ.V} (h : ∀ e ∈ Γ.inc v, (π e) r = s) : gTwist π ω r v = readDiag ω s v

A vertex whose incident sources are all relabelled so that row r becomes row s reads, in the twisted row r, exactly what it reads in the diagonal row s.

theorem TriangleInflation.Graph.twoRow_law {Γ : PairGraph} {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) (π : Γ.Edge → Equiv.Perm (Fin 2)) (g : (Γ.V → Bool) → (Γ.V → Bool) → ℝ) : ∑ ω : GAssign Γ 2, g (gTwist π ω 0) (gTwist π ω 1) * Δ ω = ∑ a : Γ.V → Bool, ∑ b : Γ.V → Bool, g a b * (P a * P b)

The two-row identity at order two. Twisting by π and reading the two rows gives a pair of independent draws from the target.

Marginals of the target on blocks of vertices

def TriangleInflation.Graph.blockMarg {Γ : PairGraph} (A : Finset Γ.V) (P : GTarget Γ) : GTarget Γ

The marginal of a target on a set of vertices, presented as a function of a full outcome vector; it depends on w only through the coordinates in A.

Equations

• TriangleInflation.Graph.blockMarg A P w = ∑ w' : Γ.V → Bool, if ∀ v ∈ A, w' v = w v then P w' else 0

theorem TriangleInflation.Graph.blockMarg_congr {Γ : PairGraph} (A : Finset Γ.V) (P : GTarget Γ) {w w' : Γ.V → Bool} (h : ∀ v ∈ A, w v = w' v) : blockMarg A P w = blockMarg A P w'

@[simp]

theorem TriangleInflation.Graph.blockMarg_univ {Γ : PairGraph} (P : GTarget Γ) : blockMarg Finset.univ P = P

theorem TriangleInflation.Graph.blockMarg_empty {Γ : PairGraph} {P : GTarget Γ} (hP : IsLaw P) (w : Γ.V → Bool) : blockMarg ∅ P w = 1

theorem TriangleInflation.Graph.blockMarg_union_of_sourceDisjoint {Γ : PairGraph} {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hP : IsLaw P) (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) (A B : Finset Γ.V) (hAB : Disjoint (A.biUnion Γ.inc) (B.biUnion Γ.inc)) (w : Γ.V → Bool) : blockMarg (A ∪ B) P w = blockMarg A P w * blockMarg B P w

Source-disjoint blocks of the target are independent. If no source touches both A and B then the joint marginal of the target on A ∪ B is the product of its marginals on A and on B. This is step (i) of the paper proof, and it needs only order two.

theorem TriangleInflation.Graph.blockMarg_biUnion_of_sourceDisjoint {Γ : PairGraph} {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hP : IsLaw P) (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) {ι : Type u_1} (A : ι → Finset Γ.V) (hA : ∀ (i j : ι), i ≠ j → Disjoint ((A i).biUnion Γ.inc) ((A j).biUnion Γ.inc)) (S : Finset ι) (w : Γ.V → Bool) : blockMarg (S.biUnion A) P w = ∏ i ∈ S, blockMarg (A i) P w

The iterated form of blockMarg_union_of_sourceDisjoint: pairwise source-disjoint blocks are mutually independent under the target.

The conditioning event and the conditional law of the centres

def TriangleInflation.Graph.swapTwist {Γ : PairGraph} (j : Γ.Edge → Fin 2) : Γ.Edge → Equiv.Perm (Fin 2)

The relabelling that moves the copy index j e of each source to the index 0 (and back).

Equations

• TriangleInflation.Graph.swapTwist j e = Equiv.swap 0 (j e)

def TriangleInflation.Graph.flipIdx : Fin 2 → Fin 2

The other of the two copy indices.

Equations

• TriangleInflation.Graph.flipIdx r = if r = 0 then 1 else 0

@[simp]

theorem TriangleInflation.Graph.swapTwist_zero {Γ : PairGraph} (j : Γ.Edge → Fin 2) (e : Γ.Edge) : (swapTwist j e) 0 = j e

@[simp]

theorem TriangleInflation.Graph.swapTwist_one {Γ : PairGraph} (j : Γ.Edge → Fin 2) (e : Γ.Edge) : (swapTwist j e) 1 = flipIdx (j e)

theorem TriangleInflation.Graph.forall_fin_two_of_flip (r : Fin 2) (p : Fin 2 → Prop) : (∀ (m : Fin 2), p m) ↔ p r ∧ p (flipIdx r)

theorem TriangleInflation.Graph.twoRow_blockMass {Γ : PairGraph} {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) (π : Γ.Edge → Equiv.Perm (Fin 2)) (A₀ A₁ : Finset Γ.V) (w₀ w₁ : Γ.V → Bool) : ∑ ω : GAssign Γ 2, ((if ∀ v ∈ A₀, gTwist π ω 0 v = w₀ v then 1 else 0) * if ∀ v ∈ A₁, gTwist π ω 1 v = w₁ v then 1 else 0) * Δ ω = blockMarg A₀ P w₀ * blockMarg A₁ P w₁

Two-row block masses. The probability that the first twisted row matches w₀ on A₀ and the second matches w₁ on A₁ is the product of the two target marginals: this is the one computation the reconstruction performs.

theorem TriangleInflation.Graph.ind_mul_ind (p q : Prop) [Decidable p] [Decidable q] : ((if p then 1 else 0) * if q then 1 else 0) = if p ∧ q then 1 else 0

theorem TriangleInflation.Graph.ind_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : (if p then 1 else 0) = if q then 1 else 0

theorem TriangleInflation.Graph.gTwist_leaf_zero {Γ : PairGraph} {j : Γ.Edge → Fin 2} {ω : GAssign Γ 2} {leafEdge : Γ.V → Γ.Edge} {ℓ : Γ.V} (h : Γ.inc ℓ = {leafEdge ℓ}) : gTwist (swapTwist j) ω 0 ℓ = readDiag ω (j (leafEdge ℓ)) ℓ

A leaf reads, in the twisted row 0, the copy j of its unique source.

theorem TriangleInflation.Graph.gTwist_leaf_one {Γ : PairGraph} {j : Γ.Edge → Fin 2} {ω : GAssign Γ 2} {leafEdge : Γ.V → Γ.Edge} {ℓ : Γ.V} (h : Γ.inc ℓ = {leafEdge ℓ}) : gTwist (swapTwist j) ω 1 ℓ = readDiag ω (flipIdx (j (leafEdge ℓ))) ℓ

A leaf reads, in the twisted row 1, the other copy of its unique source.

theorem TriangleInflation.Graph.centreLeaf_mass {Γ : PairGraph} {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) (Lf : Finset Γ.V) (leafEdge : Γ.V → Γ.Edge) (hinc : ∀ ℓ ∈ Lf, Γ.inc ℓ = {leafEdge ℓ}) (j : Γ.Edge → Fin 2) (C : Finset Γ.V) (hC : Disjoint C Lf) (x : Γ.V → Fin 2 → Bool) (w : Γ.V → Bool) : ∑ ω : GAssign Γ 2, ((if ∀ v ∈ C, gTwist (swapTwist j) ω 0 v = w v then 1 else 0) * if ∀ ℓ ∈ Lf, ∀ (m : Fin 2), readDiag ω m ℓ = x ℓ m then 1 else 0) * Δ ω = (blockMarg (C ∪ Lf) P fun (v : Γ.V) => if v ∈ Lf then x v (j (leafEdge v)) else w v) * blockMarg Lf P fun (v : Γ.V) => x v (flipIdx (j (leafEdge v)))

The conditional marginal of the centres (step (iii) of the paper proof).

Fix a copy index j e for every source. Condition a Navascués–Wolfe witness at order two on the event E that each leaf's two copies read a prescribed array x. Then the joint mass of E together with the event that the vertices of C — in practice the two centres — read, on the copy j of each of their leaf sources and the copy 0 of every other source, the values w, is the corresponding two-block marginal of the target. Dividing by the same identity with C = ∅ turns this into the conditional law of the centres given the leaf values, which is the only fact about the witness the reconstruction uses.

Models with deterministic local responses

The reconstruction builds a model whose sources are independent and whose responses are deterministic functions of the incident sources. It is convenient to package such a model as a single decoder dec from source values to outcomes, subject to the locality requirement that the outcome at v depend only on the sources incident to v.

theorem TriangleInflation.Graph.respMass_ite (d b : Bool) : respMass (if d = true then 0 else 1) b = if b = d then 1 else 0

respMass of a deterministic response is the indicator of the prescribed outcome.

theorem TriangleInflation.Graph.gCompatible_of_localDecoder {Γ : PairGraph} {A : Type} [Fintype A] [Inhabited A] (ν : Γ.Edge → A → ℝ) (hν : ∀ (e : Γ.Edge), IsLaw (ν e)) (dec : (Γ.Edge → A) → Γ.V → Bool) (hloc : ∀ (z z' : Γ.Edge → A) (v : Γ.V), (∀ e ∈ Γ.inc v, z e = z' e) → dec z v = dec z' v) (P : GTarget Γ) (hP : pushforward (fun (z : Γ.Edge → A) => ∏ e : Γ.Edge, ν e (z e)) dec = P) : GCompatible Γ P

A deterministic local decoder gives a model. If every source e carries an independent law ν e and the outcome at each vertex v is a function dec of the source values that depends only on the sources incident to v, then the pushforward of the product law along dec is compatible.

theorem TriangleInflation.Graph.sum_prod_pi {ι : Type u_1} {A : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype A] [CommRing R] (g : ι → A → R) : ∑ z : ι → A, ∏ i : ι, g i (z i) = ∏ i : ι, ∑ a : A, g i a

A sum over a function space of a product of per-coordinate weights is the product of the coordinate sums.

Reconstruction: the source-disjoint fibre case

A double-star forest whose components are single sources — a perfect matching — is already covered by the machinery above: the source of a component carries the outcomes of its two endpoints. This is the degenerate case p = q = 0 of the paper's Theorem, and it is recorded here because it exercises the whole pipeline (twisted rows, block independence, deterministic local decoder) end to end.

theorem TriangleInflation.Graph.gCompatible_of_fibre_sourceDisjoint {Γ : PairGraph} {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hP : IsLaw P) (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) (edgeAt : Γ.V → Γ.Edge) (hmem : ∀ (v : Γ.V), edgeAt v ∈ Γ.inc v) (hdisj : ∀ (e e' : Γ.Edge), e ≠ e' → Disjoint ({v : Γ.V | edgeAt v = e}.biUnion Γ.inc) ({v : Γ.V | edgeAt v = e'}.biUnion Γ.inc)) : GCompatible Γ P

Reconstruction when the vertex fibres of the sources are source-disjoint. Choose for each vertex v an incident source edgeAt v. If the vertex sets {v | edgeAt v = e} are pairwise source-disjoint, every target passing the order-two Navascués–Wolfe test is compatible: the source e carries the joint outcome of the vertices that read it, which by source-disjoint block independence is exactly the right marginal.

The combinatorics of a double-star forest

structure TriangleInflation.Graph.DSStruct (Γ : PairGraph) : Type

The combinatorial data of a double-star forest. Every vertex is a leaf or a centre; a leaf carries a single source joining it to its centre; a centre has a partner centre, and the two share the centre source of their component. root v names the centre source of the component of v, so the components are the fibres of root.

• leaf : Γ.V → Bool

  Is the vertex a leaf?

• edgeAt : Γ.V → Γ.Edge

  For a leaf, its unique source; for a centre, the centre source of its component.

• mate : Γ.V → Γ.V

  For a leaf, its centre; for a centre, its partner.

• root : Γ.V → Γ.Edge

  The centre source of the component of a vertex.

• vtx : Γ.Edge → Γ.V

  A vertex whose edgeAt is the given source.

• vtx_edgeAt (e : Γ.Edge) : self.edgeAt (self.vtx e) = e
• edgeAt_inc (v : Γ.V) : self.edgeAt v ∈ Γ.inc v
• edgeAt_inc_mate (v : Γ.V) : self.edgeAt v ∈ Γ.inc (self.mate v)
• edgeAt_mem (v u : Γ.V) : self.edgeAt v ∈ Γ.inc u → u = v ∨ u = self.mate v

  The source edgeAt v touches only v and mate v.

• mate_not_leaf (v : Γ.V) : self.leaf (self.mate v) = false
• mate_ne (v : Γ.V) : self.mate v ≠ v
• leaf_inc (v : Γ.V) : self.leaf v = true → Γ.inc v = {self.edgeAt v}
• fib_leaf (v : Γ.V) : self.leaf v = true → {u : Γ.V | self.edgeAt u = self.edgeAt v} = {v}
• fib_ctr (v : Γ.V) : self.leaf v = false → {u : Γ.V | self.edgeAt u = self.edgeAt v} = {v, self.mate v}
• root_leaf (v : Γ.V) : self.leaf v = true → self.root v = self.edgeAt (self.mate v)
• root_ctr (v : Γ.V) : self.leaf v = false → self.root v = self.edgeAt v
• comp_sourceDisjoint (y y' : Γ.Edge) : y ≠ y' → Disjoint ({v : Γ.V | self.root v = y}.biUnion Γ.inc) ({v : Γ.V | self.root v = y'}.biUnion Γ.inc)

@[reducible, inline]

abbrev TriangleInflation.Graph.DSLat (Γ : PairGraph) : Type

The latent alphabet used by the reconstruction: a response table together with a bit. The same type serves every source; the source law is what distinguishes leaf sources, which carry the bit, from centre sources, which carry the table.

Equations

• TriangleInflation.Graph.DSLat Γ = (((Γ.V → Bool) → Γ.V → Bool) × Bool)

def TriangleInflation.Graph.dfltTable (Γ : PairGraph) : (Γ.V → Bool) → Γ.V → Bool

The table that unsupported arguments are sent to.

Equations

• TriangleInflation.Graph.dfltTable Γ x✝¹ x✝ = false

def TriangleInflation.Graph.vMarg {Γ : PairGraph} (P : GTarget Γ) (v : Γ.V) (β : Bool) : ℝ

The one-vertex marginal of the target.

Equations

• TriangleInflation.Graph.vMarg P v β = TriangleInflation.Graph.blockMarg {v} P (Function.const Γ.V β)

noncomputable def TriangleInflation.Graph.xarr {Γ : PairGraph} (P : GTarget Γ) (ℓ : Γ.V) (m : Fin 2) : Bool

The array of two symbols listed at each leaf: both symbols when both are supported, and otherwise the supported symbol twice.

Equations

• TriangleInflation.Graph.xarr P ℓ m = if TriangleInflation.Graph.vMarg P ℓ false = 0 then true else if TriangleInflation.Graph.vMarg P ℓ true = 0 then false else decide (m = 1)

noncomputable def TriangleInflation.Graph.pick {Γ : PairGraph} (P : GTarget Γ) (ℓ : Γ.V) (β : Bool) : Fin 2

A copy index at which the leaf ℓ reads the symbol β.

Equations

• TriangleInflation.Graph.pick P ℓ β = if TriangleInflation.Graph.xarr P ℓ 0 = β then 0 else 1

def TriangleInflation.Graph.DSStruct.leaves {Γ : PairGraph} (D : DSStruct Γ) (y : Γ.Edge) : Finset Γ.V

The leaves of the component whose centre source is y.

Equations

• D.leaves y = {v : Γ.V | D.leaf v = true ∧ D.root v = y}

def TriangleInflation.Graph.DSStruct.allLeaves {Γ : PairGraph} (D : DSStruct Γ) : Finset Γ.V

All the leaves.

Equations

• D.allLeaves = {v : Γ.V | D.leaf v = true}

def TriangleInflation.Graph.DSStruct.comp {Γ : PairGraph} (D : DSStruct Γ) (y : Γ.Edge) : Finset Γ.V

The vertices of the component whose centre source is y.

Equations

• D.comp y = {v : Γ.V | D.root v = y}

def TriangleInflation.Graph.DSStruct.ctrs {Γ : PairGraph} (D : DSStruct Γ) (y : Γ.Edge) : Finset Γ.V

The two centres of the component whose centre source is y.

Equations

• D.ctrs y = {D.vtx y, D.mate (D.vtx y)}

def TriangleInflation.Graph.DSStruct.locVec {Γ : PairGraph} (D : DSStruct Γ) (z : Γ.Edge → DSLat Γ) (v : Γ.V) : Γ.V → Bool

The leaf values that a vertex sees among its sources.

Equations

• D.locVec z v u = if D.leaf u = true ∧ D.mate u = v then (z (D.edgeAt u)).2 else false

def TriangleInflation.Graph.DSStruct.locOut {Γ : PairGraph} (D : DSStruct Γ) (w : Γ.V → Bool) (v : Γ.V) : Γ.V → Bool

The same vector read off an outcome vector.

Equations

• D.locOut w v u = if D.leaf u = true ∧ D.mate u = v then w u else false

def TriangleInflation.Graph.DSStruct.dec {Γ : PairGraph} (D : DSStruct Γ) (z : Γ.Edge → DSLat Γ) : Γ.V → Bool

The decoder of the reconstructed model: a leaf copies its source, a centre evaluates its half of the centre table on the values of its leaf sources.

Equations

• D.dec z v = if D.leaf v = true then (z (D.edgeAt v)).2 else (z (D.edgeAt v)).1 (D.locVec z v) v

noncomputable def TriangleInflation.Graph.DSStruct.jOf {Γ : PairGraph} (D : DSStruct Γ) (P : GTarget Γ) (ξ : Γ.V → Bool) (e : Γ.Edge) : Fin 2

The relabelling index attached to each source by a vector of leaf values.

Equations

• D.jOf P ξ e = if D.leaf (D.vtx e) = true then TriangleInflation.Graph.pick P (D.vtx e) (ξ (D.vtx e)) else 0

noncomputable def TriangleInflation.Graph.DSStruct.tableOf {Γ : PairGraph} (D : DSStruct Γ) (P : GTarget Γ) (ω : GAssign Γ 2) : (Γ.V → Bool) → Γ.V → Bool

The response table read off a witness table: on the leaf values ξ it returns the observations that read, at each leaf source, the copy showing ξ.

Equations

• D.tableOf P ω ξ = TriangleInflation.Graph.gTwist (TriangleInflation.Graph.swapTwist (D.jOf P ξ)) ω 0

def TriangleInflation.Graph.DSStruct.evt {Γ : PairGraph} (D : DSStruct Γ) (P : GTarget Γ) (y : Γ.Edge) (ω : GAssign Γ 2) : Prop

The conditioning event of the component with centre source y: every leaf of that component has its two copies reading the prescribed array.

Equations

• D.evt P y ω = ∀ ℓ ∈ D.leaves y, ∀ (m : Fin 2), TriangleInflation.Graph.readDiag ω m ℓ = TriangleInflation.Graph.xarr P ℓ m

@[instance_reducible]

noncomputable instance TriangleInflation.Graph.DSStruct.instDecidableEvt {Γ : PairGraph} (D : DSStruct Γ) (P : GTarget Γ) (y : Γ.Edge) (ω : GAssign Γ 2) : Decidable (D.evt P y ω)

Equations

• D.instDecidableEvt P y ω = id inferInstance

noncomputable def TriangleInflation.Graph.DSStruct.evtMass {Γ : PairGraph} (D : DSStruct Γ) (P : GTarget Γ) (Δ : GAssign Γ 2 → ℝ) (y : Γ.Edge) : ℝ

The mass of the conditioning event.

Equations

• D.evtMass P Δ y = ∑ ω : TriangleInflation.Graph.GAssign Γ 2, (if D.evt P y ω then 1 else 0) * Δ ω

noncomputable def TriangleInflation.Graph.DSStruct.tabLaw {Γ : PairGraph} (D : DSStruct Γ) (P : GTarget Γ) (Δ : GAssign Γ 2 → ℝ) (y : Γ.Edge) (T : (Γ.V → Bool) → Γ.V → Bool) : ℝ

The law of the pair of response tables, read off the witness conditioned on evt.

Equations

• D.tabLaw P Δ y T = (∑ ω : TriangleInflation.Graph.GAssign Γ 2, ((if D.evt P y ω then 1 else 0) * if D.tableOf P ω = T then 1 else 0) * Δ ω) / D.evtMass P Δ y

noncomputable def TriangleInflation.Graph.DSStruct.lat {Γ : PairGraph} (D : DSStruct Γ) (P : GTarget Γ) (Δ : GAssign Γ 2 → ℝ) (e : Γ.Edge) : DSLat Γ → ℝ

The source law of the reconstructed model.

Equations

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

One-vertex marginals and the listed arrays

theorem TriangleInflation.Graph.vMarg_eq {Γ : PairGraph} (P : GTarget Γ) (v : Γ.V) (β : Bool) : vMarg P v β = ∑ u : Γ.V → Bool, if u v = β then P u else 0

theorem TriangleInflation.Graph.blockMarg_singleton {Γ : PairGraph} (P : GTarget Γ) (v : Γ.V) (w : Γ.V → Bool) : blockMarg {v} P w = vMarg P v (w v)

theorem TriangleInflation.Graph.vMarg_nonneg {Γ : PairGraph} {P : GTarget Γ} (hP : IsLaw P) (v : Γ.V) (β : Bool) : 0 ≤ vMarg P v β

theorem TriangleInflation.Graph.vMarg_sum {Γ : PairGraph} {P : GTarget Γ} (hP : IsLaw P) (v : Γ.V) : vMarg P v false + vMarg P v true = 1

theorem TriangleInflation.Graph.vMarg_xarr_pos {Γ : PairGraph} {P : GTarget Γ} (hP : IsLaw P) (ℓ : Γ.V) (m : Fin 2) : 0 < vMarg P ℓ (xarr P ℓ m)

theorem TriangleInflation.Graph.xarr_pick {Γ : PairGraph} {P : GTarget Γ} (ℓ : Γ.V) (β : Bool) (h : 0 < vMarg P ℓ β) : xarr P ℓ (pick P ℓ β) = β

theorem TriangleInflation.Graph.blockMarg_nonneg {Γ : PairGraph} {P : GTarget Γ} (hP : IsLaw P) (A : Finset Γ.V) (w : Γ.V → Bool) : 0 ≤ blockMarg A P w

theorem TriangleInflation.Graph.blockMarg_le {Γ : PairGraph} {P : GTarget Γ} (hP : IsLaw P) {A B : Finset Γ.V} (h : A ⊆ B) (w : Γ.V → Bool) : blockMarg B P w ≤ blockMarg A P w

theorem TriangleInflation.Graph.DSStruct.edgeAt_inj_leaves {Γ : PairGraph} (D : DSStruct Γ) {ℓ ℓ' : Γ.V} (h : D.leaf ℓ = true) (he : D.edgeAt ℓ' = D.edgeAt ℓ) : ℓ' = ℓ

theorem TriangleInflation.Graph.DSStruct.leaf_inc_disjoint {Γ : PairGraph} (D : DSStruct Γ) {ℓ ℓ' : Γ.V} (h : D.leaf ℓ = true) (h' : D.leaf ℓ' = true) (hne : ℓ ≠ ℓ') : Disjoint (Γ.inc ℓ) (Γ.inc ℓ')

theorem TriangleInflation.Graph.DSStruct.blockMarg_leaves {Γ : PairGraph} (D : DSStruct Γ) {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hP : IsLaw P) (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) (S : Finset Γ.V) (hS : ∀ v ∈ S, D.leaf v = true) (w : Γ.V → Bool) : blockMarg S P w = ∏ ℓ ∈ S, vMarg P ℓ (w ℓ)

Any set of leaves is a union of source-disjoint singletons, so its marginal is the product of the one-vertex marginals.

theorem TriangleInflation.Graph.DSStruct.vtx_of_leaf {Γ : PairGraph} (D : DSStruct Γ) {v : Γ.V} (h : D.leaf v = true) : D.vtx (D.edgeAt v) = v

@[simp]

theorem TriangleInflation.Graph.DSStruct.mem_leaves {Γ : PairGraph} (D : DSStruct Γ) {v : Γ.V} {y : Γ.Edge} : v ∈ D.leaves y ↔ D.leaf v = true ∧ D.root v = y

@[simp]

theorem TriangleInflation.Graph.DSStruct.mem_comp {Γ : PairGraph} (D : DSStruct Γ) {v : Γ.V} {y : Γ.Edge} : v ∈ D.comp y ↔ D.root v = y

theorem TriangleInflation.Graph.DSStruct.leaf_of_mem_leaves {Γ : PairGraph} (D : DSStruct Γ) {v : Γ.V} {y : Γ.Edge} (h : v ∈ D.leaves y) : D.leaf v = true

theorem TriangleInflation.Graph.DSStruct.ctrs_not_leaf {Γ : PairGraph} (D : DSStruct Γ) {y : Γ.Edge} (hy : D.leaf (D.vtx y) = false) (v : Γ.V) : v ∈ D.ctrs y → D.leaf v = false

theorem TriangleInflation.Graph.DSStruct.ctrs_disjoint_leaves {Γ : PairGraph} (D : DSStruct Γ) {y : Γ.Edge} (hy : D.leaf (D.vtx y) = false) : Disjoint (D.ctrs y) (D.leaves y)

theorem TriangleInflation.Graph.DSStruct.comp_eq {Γ : PairGraph} (D : DSStruct Γ) {y : Γ.Edge} (hy : D.leaf (D.vtx y) = false) : D.comp y = D.ctrs y ∪ D.leaves y

theorem TriangleInflation.Graph.DSStruct.jOf_edgeAt {Γ : PairGraph} (D : DSStruct Γ) {P : GTarget Γ} {ℓ : Γ.V} (h : D.leaf ℓ = true) (ξ : Γ.V → Bool) : D.jOf P ξ (D.edgeAt ℓ) = pick P ℓ (ξ ℓ)

theorem TriangleInflation.Graph.DSStruct.evtMass_eq {Γ : PairGraph} (D : DSStruct Γ) {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) (y : Γ.Edge) (j : Γ.Edge → Fin 2) (w : Γ.V → Bool) : D.evtMass P Δ y = (blockMarg (D.leaves y) P fun (v : Γ.V) => if v ∈ D.leaves y then xarr P v (j (D.edgeAt v)) else w v) * blockMarg (D.leaves y) P fun (v : Γ.V) => xarr P v (flipIdx (j (D.edgeAt v)))

The mass of the conditioning event, evaluated by the conditional-marginal identity.

theorem TriangleInflation.Graph.DSStruct.evtMass_pos {Γ : PairGraph} (D : DSStruct Γ) {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hP : IsLaw P) (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) (y : Γ.Edge) : 0 < D.evtMass P Δ y

theorem TriangleInflation.Graph.DSStruct.tabLaw_isLaw {Γ : PairGraph} (D : DSStruct Γ) {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hP : IsLaw P) (hΔ : IsLaw Δ) (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) (y : Γ.Edge) : IsLaw (D.tabLaw P Δ y)

theorem TriangleInflation.Graph.DSStruct.lat_isLaw {Γ : PairGraph} (D : DSStruct Γ) {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hP : IsLaw P) (hΔ : IsLaw Δ) (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) (e : Γ.Edge) : IsLaw (D.lat P Δ e)

theorem TriangleInflation.Graph.DSStruct.leaves_subset_comp {Γ : PairGraph} (D : DSStruct Γ) (y : Γ.Edge) : D.leaves y ⊆ D.comp y

noncomputable def TriangleInflation.Graph.DSStruct.ctrFactor {Γ : PairGraph} (D : DSStruct Γ) (P : GTarget Γ) (Δ : GAssign Γ 2 → ℝ) (y : Γ.Edge) (w : Γ.V → Bool) : ℝ

The conditional mass that the reconstructed centre source assigns to the outcomes w at the two centres of the component y.

Equations

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

theorem TriangleInflation.Graph.DSStruct.ctrFactor_mul {Γ : PairGraph} (D : DSStruct Γ) {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hP : IsLaw P) (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) {y : Γ.Edge} (hy : D.leaf (D.vtx y) = false) (w : Γ.V → Bool) : D.ctrFactor P Δ y w * blockMarg (D.leaves y) P w = blockMarg (D.comp y) P w

The component identity. The centre factor times the leaf marginals of a component is the marginal of the target on the whole component. This is step (iii)–(iv) of the paper proof in the form the reconstruction needs.

theorem TriangleInflation.Graph.gTwist_congr {Γ : PairGraph} {t : ℕ} {π π' : Γ.Edge → Equiv.Perm (Fin t)} {ω : GAssign Γ t} {r : Fin t} {v : Γ.V} (h : ∀ e ∈ Γ.inc v, π e = π' e) : gTwist π ω r v = gTwist π' ω r v

A vertex's twisted reading depends on the relabelling only through its incident sources.

def TriangleInflation.Graph.DSStruct.fib {Γ : PairGraph} (D : DSStruct Γ) (e : Γ.Edge) : Finset Γ.V

The vertices whose chosen source is e.

Equations

• D.fib e = {v : Γ.V | D.edgeAt v = e}

theorem TriangleInflation.Graph.DSStruct.fib_of_leaf {Γ : PairGraph} (D : DSStruct Γ) {e : Γ.Edge} (h : D.leaf (D.vtx e) = true) : D.fib e = {D.vtx e}

theorem TriangleInflation.Graph.DSStruct.fib_of_ctr {Γ : PairGraph} (D : DSStruct Γ) {e : Γ.Edge} (h : D.leaf (D.vtx e) = false) : D.fib e = D.ctrs e

theorem TriangleInflation.Graph.DSStruct.comp_of_leaf {Γ : PairGraph} (D : DSStruct Γ) {e : Γ.Edge} (h : D.leaf (D.vtx e) = true) : D.comp e = ∅

A leaf source is the centre source of no component.

theorem TriangleInflation.Graph.DSStruct.leaves_of_leafEdge {Γ : PairGraph} (D : DSStruct Γ) {e : Γ.Edge} (h : D.leaf (D.vtx e) = true) : D.leaves e = ∅

theorem TriangleInflation.Graph.DSStruct.dec_local {Γ : PairGraph} (D : DSStruct Γ) (z z' : Γ.Edge → DSLat Γ) (v : Γ.V) (h : ∀ e ∈ Γ.inc v, z e = z' e) : D.dec z v = D.dec z' v

The decoder is local: the outcome at v depends only on the sources incident to v.

theorem TriangleInflation.Graph.DSStruct.tableOf_ctr {Γ : PairGraph} (D : DSStruct Γ) (P : GTarget Γ) (ω : GAssign Γ 2) {v : Γ.V} (hv : D.leaf v = false) (w : Γ.V → Bool) : D.tableOf P ω (D.locOut w v) v = gTwist (swapTwist (D.jOf P w)) ω 0 v

At a centre, the reconstructed table evaluated on the local leaf values reads the twisted observation used by the conditional-marginal identity.

def TriangleInflation.Graph.DSStruct.condw {Γ : PairGraph} (D : DSStruct Γ) (w : Γ.V → Bool) (v : Γ.V) (a : DSLat Γ) : ℝ

The indicator that a source value gives the vertex v the outcome w v.

Equations

• D.condw w v a = if D.leaf v = true then if a.2 = w v then 1 else 0 else if a.1 (D.locOut w v) v = w v then 1 else 0

theorem TriangleInflation.Graph.DSStruct.condw_leaf {Γ : PairGraph} (D : DSStruct Γ) {w : Γ.V → Bool} {v : Γ.V} (h : D.leaf v = true) (a : DSLat Γ) : D.condw w v a = if a.2 = w v then 1 else 0

theorem TriangleInflation.Graph.DSStruct.condw_ctr {Γ : PairGraph} (D : DSStruct Γ) {w : Γ.V → Bool} {v : Γ.V} (h : D.leaf v = false) (a : DSLat Γ) : D.condw w v a = if a.1 (D.locOut w v) v = w v then 1 else 0

theorem TriangleInflation.Graph.DSStruct.lat_leaf {Γ : PairGraph} (D : DSStruct Γ) {P : GTarget Γ} {Δ : GAssign Γ 2 → ℝ} {e : Γ.Edge} (h : D.leaf (D.vtx e) = true) (a : DSLat Γ) : D.lat P Δ e a = if a.1 = dfltTable Γ then vMarg P (D.vtx e) a.2 else 0

theorem TriangleInflation.Graph.DSStruct.lat_ctr {Γ : PairGraph} (D : DSStruct Γ) {P : GTarget Γ} {Δ : GAssign Γ 2 → ℝ} {e : Γ.Edge} (h : D.leaf (D.vtx e) = false) (a : DSLat Γ) : D.lat P Δ e a = if a.2 = false then D.tabLaw P Δ e a.1 else 0

theorem TriangleInflation.Graph.DSStruct.factor_leaf {Γ : PairGraph} (D : DSStruct Γ) {P : GTarget Γ} {Δ : GAssign Γ 2 → ℝ} {e : Γ.Edge} (he : D.leaf (D.vtx e) = true) (w : Γ.V → Bool) : ∑ a : DSLat Γ, D.lat P Δ e a * ∏ v ∈ D.fib e, D.condw w v a = vMarg P (D.vtx e) (w (D.vtx e))

The per-source factor of the reconstructed model at a leaf source.

theorem TriangleInflation.Graph.DSStruct.factor_ctr {Γ : PairGraph} (D : DSStruct Γ) {P : GTarget Γ} {Δ : GAssign Γ 2 → ℝ} (hP : IsLaw P) (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) {e : Γ.Edge} (he : D.leaf (D.vtx e) = false) (w : Γ.V → Bool) : ∑ a : DSLat Γ, D.lat P Δ e a * ∏ v ∈ D.fib e, D.condw w v a = D.ctrFactor P Δ e w

The per-source factor of the reconstructed model at a centre source.

theorem TriangleInflation.Graph.DSStruct.dec_indicator {Γ : PairGraph} (D : DSStruct Γ) (P : GTarget Γ) (Δ : GAssign Γ 2 → ℝ) (w : Γ.V → Bool) (z : Γ.Edge → DSLat Γ) : (if D.dec z = w then ∏ e : Γ.Edge, D.lat P Δ e (z e) else 0) = ∏ e : Γ.Edge, D.lat P Δ e (z e) * ∏ v ∈ D.fib e, D.condw w v (z e)

The decoder indicator, written as a product over the sources.

theorem TriangleInflation.Graph.DSStruct.gCompatible_of_dsStruct {Γ : PairGraph} (D : DSStruct Γ) {Δ : GAssign Γ 2 → ℝ} {P : GTarget Γ} (hP : IsLaw P) (hΔ : IsLaw Δ) (hsym : GSymmetric 2 Δ) (hdiag : pushforward Δ readDiag = gTensorPow 2 P) : GCompatible Γ P

The double-star reconstruction. A target passing the order-two Navascués–Wolfe test on a pair graph carrying a double-star structure is compatible.