Transport and exhaustion (A6)

Statements split from the original Statements.lean skeleton (one file per proving task). The mathematics is AUDIT-NOTES A6, with the paper proofs in sections 12 (lem:transport) and 13 (lem:exhaustion).

Both statements are proved. induced_transport is split into its two halves, transport_ai_feasible (an H-witness extends to a G-witness) and transport_compatible_restrict (a G-model restricts to an H-model); the Transport namespace carries their machinery, and the Exhaustion namespace the graph theory behind exhaustion. Both namespaces are nested so that their generic names cannot collide with the rest of the library.

A6: transport along induced subgraphs, and exhaustion

Infrastructure for transport

The machinery of lem:transport, kept in the Transport namespace so that its generic names do not collide with the rest of the library: pushforward algebra and pi-type splitting, the edge map of an induced embedding, the extended witness (transportWitness) with its symmetry, diagonal law and ancestral prescriptions, and the restricted model (restrictModel) with its validity and observed law.

Generic lemmas

theorem TriangleInflation.Graph.Transport.sum_prod_pi {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (w : (i : ι) → α i → ℝ) : ∑ y : (i : ι) → α i, ∏ i : ι, w i (y i) = ∏ i : ι, ∑ a : α i, w i a

theorem TriangleInflation.Graph.Transport.sum_respMass (q : ℝ) : ∑ b : Bool, respMass q b = 1

theorem TriangleInflation.Graph.Transport.cast_pi_apply {ι : Type u_1} {α : ι → Type u_2} (x : (i : ι) → α i) {a b : ι} (p : a = b) : cast ⋯ (x a) = x b

theorem TriangleInflation.Graph.Transport.cast_inj_apply {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} (F : ι' → ι) (hF : Function.Injective F) (x : (f : ι') → α (F f)) {f' f : ι'} (p : F f' = F f) : cast ⋯ (x f') = x f

theorem TriangleInflation.Graph.Transport.respMass_affine {ι : Type u_1} [Fintype ι] (w q : ι → ℝ) (b : Bool) (hw : ∑ i : ι, w i = 1) : ∑ i : ι, w i * respMass (q i) b = respMass (∑ i : ι, w i * q i) b

respMass is affine in its first argument.

theorem TriangleInflation.Graph.Transport.prod_split {ι : Type u_1} [Fintype ι] (p : ι → Prop) [DecidablePred p] (F : ι → ℝ) : ∏ i : ι, F i = (∏ i : { x : ι // p x }, F ↑i) * ∏ i : { x : ι // ¬p x }, F ↑i

Splitting a product over a finite type along a predicate.

Splitting a sum over a dependent function type along a predicate

theorem TriangleInflation.Graph.Transport.sum_pi_two_block {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : ι → Prop) (w : (i : ι) → α i → ℝ) (hw : ∀ (i : ι), ∑ a : α i, w i a = 1) (A B : ((i : ι) → α i) → ℝ) (hA : ∀ (z z' : (i : ι) → α i), (∀ (i : ι), p i → z i = z' i) → A z = A z') (hB : ∀ (z z' : (i : ι) → α i), (∀ (i : ι), ¬p i → z i = z' i) → B z = B z') : ∑ z : (i : ι) → α i, (∏ i : ι, w i (z i)) * (A z * B z) = (∑ z : (i : ι) → α i, (∏ i : ι, w i (z i)) * A z) * ∑ z : (i : ι) → α i, (∏ i : ι, w i (z i)) * B z

Factor weighted expectations across complementary blocks of coordinates.

theorem TriangleInflation.Graph.Transport.sum_pi_prod_indep {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] {ν : Type u_3} (blk : ν → ι → Prop) (w : (i : ι) → α i → ℝ) (hw : ∀ (i : ι), ∑ a : α i, w i a = 1) (g : ν → ((i : ι) → α i) → ℝ) (hdisj : ∀ (u u' : ν), u ≠ u' → ∀ (i : ι), blk u i → ¬blk u' i) (hg : ∀ (u : ν) (z z' : (i : ι) → α i), (∀ (i : ι), blk u i → z i = z' i) → g u z = g u z') (s : Finset ν) : ∑ z : (i : ι) → α i, (∏ i : ι, w i (z i)) * ∏ u ∈ s, g u z = ∏ u ∈ s, ∑ z : (i : ι) → α i, (∏ i : ι, w i (z i)) * g u z

Independence: the expectation of a product of functions of disjoint blocks of coordinates factorizes.

The edge map of an induced embedding

def TriangleInflation.Graph.Transport.edgeMap (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) : H.Edge → G.Edge

The edge map induced by an induced embedding.

Equations

• TriangleInflation.Graph.Transport.edgeMap G H φ hind e = ⟨Sym2.map φ ↑e, ⋯⟩

@[simp]

theorem TriangleInflation.Graph.Transport.edgeMap_val (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (e : H.Edge) : ↑(edgeMap G H φ hind e) = Sym2.map φ ↑e

theorem TriangleInflation.Graph.Transport.edgeMap_injective (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) : Function.Injective (edgeMap G H φ hind)

theorem TriangleInflation.Graph.Transport.edgeMap_mem_inc_iff (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (u : H.V) (e : H.Edge) : edgeMap G H φ hind e ∈ G.inc (φ u) ↔ e ∈ H.inc u

Inducedness gives the exact incidence correspondence.

@[reducible, inline]

abbrev TriangleInflation.Graph.Transport.Rest (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) : Type

The G-edges outside the image of the edge map.

Equations

• TriangleInflation.Graph.Transport.Rest G H φ hind = { g : G.Edge // ¬∃ (f : H.Edge), TriangleInflation.Graph.Transport.edgeMap G H φ hind f = g }

theorem TriangleInflation.Graph.Transport.cross_unique (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (g : G.Edge) (hg : ¬∃ (f : H.Edge), edgeMap G H φ hind f = g) (u u' : H.V) (hu : g ∈ G.inc (φ u)) (hu' : g ∈ G.inc (φ u')) : u = u'

Key consequence of inducedness: an edge of G outside the image of the edge map meets the image of φ in at most one vertex.

The restricted model

noncomputable def TriangleInflation.Graph.Transport.mergeVals (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (M : GModel G) (u : H.V) (c : (f : ↥(H.inc u)) → M.L (edgeMap G H φ hind ↑f)) (z : (r : Rest G H φ hind) → M.L ↑r) (g : ↥(G.inc (φ u))) : M.L ↑g

Merge the H-edge values c at u with the values z of the remaining G-edges.

Equations

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

theorem TriangleInflation.Graph.Transport.mergeVals_eq (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (M : GModel G) (u : H.V) (X : (g : G.Edge) → M.L g) : (fun (g : ↥(G.inc (φ u))) => X ↑g) = mergeVals G H φ hφ hind M u (fun (f : ↥(H.inc u)) => X (edgeMap G H φ hind ↑f)) fun (r : Rest G H φ hind) => X ↑r

noncomputable def TriangleInflation.Graph.Transport.restrictModel (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (M : GModel G) : GModel H

The model of H obtained from a model of G by keeping the sources in the image of the edge map and averaging out the remaining ones.

Equations

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

theorem TriangleInflation.Graph.Transport.restrictModel_valid (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (M : GModel G) (hM : M.Valid) : (restrictModel G H φ hφ hind M).Valid

Range equivalences and counting

noncomputable def TriangleInflation.Graph.Transport.imgEquiv {A : Type u_1} {B : Type u_2} (F : A → B) (hF : Function.Injective F) : A ≃ { b : B // ∃ (a : A), F a = b }

An injection is an equivalence onto its image, described as a subtype.

Equations

• TriangleInflation.Graph.Transport.imgEquiv F hF = { toFun := fun (a : A) => ⟨F a, ⋯⟩, invFun := fun (b : { b : B // ∃ (a : A), F a = b }) => ⋯.choose, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TriangleInflation.Graph.Transport.imgEquiv_val {A : Type u_1} {B : Type u_2} (F : A → B) (hF : Function.Injective F) (a : A) : ↑((imgEquiv F hF) a) = F a

theorem TriangleInflation.Graph.Transport.card_img {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (F : A → B) (hF : Function.Injective F) : Fintype.card { b : B // ∃ (a : A), F a = b } = Fintype.card A

theorem TriangleInflation.Graph.Transport.card_compl_img {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (F : A → B) (hF : Function.Injective F) : Fintype.card { b : B // ¬∃ (a : A), F a = b } = Fintype.card B - Fintype.card A

The vertex-side splitting

noncomputable def TriangleInflation.Graph.Transport.vtxEquiv (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) : (H.V → Bool) × ({ v : G.V // ¬∃ (u : H.V), φ u = v } → Bool) ≃ (G.V → Bool)

Splitting an outcome vector of G into its restriction along φ and the rest.

Equations

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

theorem TriangleInflation.Graph.Transport.vtxEquiv_phi (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (a : H.V → Bool) (b : { v : G.V // ¬∃ (u : H.V), φ u = v } → Bool) (u : H.V) : (vtxEquiv G H φ hφ) (a, b) (φ u) = a u

theorem TriangleInflation.Graph.Transport.vtxEquiv_out (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (a : H.V → Bool) (b : { v : G.V // ¬∃ (u : H.V), φ u = v } → Bool) (v : { v : G.V // ¬∃ (u : H.V), φ u = v }) : (vtxEquiv G H φ hφ) (a, b) ↑v = b v

theorem TriangleInflation.Graph.Transport.vtx_marginal (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (q : G.V → ℝ) (wH : H.V → Bool) : ∑ b : { v : G.V // ¬∃ (u : H.V), φ u = v } → Bool, ∏ v : G.V, respMass (q v) ((vtxEquiv G H φ hφ) (wH, b) v) = ∏ u : H.V, respMass (q (φ u)) (wH u)

Marginalizing a product over the vertices of G down to the vertices of H.

The edge-side splitting

noncomputable def TriangleInflation.Graph.Transport.edgeValEquiv (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (M : GModel G) : ((f : H.Edge) → M.L (edgeMap G H φ hind f)) × ((r : Rest G H φ hind) → M.L ↑r) ≃ ((g : G.Edge) → M.L g)

Splitting a joint value of all G-sources into the values on the image of the edge map and the values on the rest.

Equations

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

theorem TriangleInflation.Graph.Transport.edgeValEquiv_left (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (M : GModel G) (x : (f : H.Edge) → M.L (edgeMap G H φ hind f)) (z : (r : Rest G H φ hind) → M.L ↑r) (f : H.Edge) : (edgeValEquiv G H φ hφ hind M) (x, z) (edgeMap G H φ hind f) = x f

theorem TriangleInflation.Graph.Transport.edgeValEquiv_right (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (M : GModel G) (x : (f : H.Edge) → M.L (edgeMap G H φ hind f)) (z : (r : Rest G H φ hind) → M.L ↑r) (r : Rest G H φ hind) : (edgeValEquiv G H φ hφ hind M) (x, z) ↑r = z r

theorem TriangleInflation.Graph.Transport.edgeValEquiv_prod (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (M : GModel G) (x : (f : H.Edge) → M.L (edgeMap G H φ hind f)) (z : (r : Rest G H φ hind) → M.L ↑r) : ∏ g : G.Edge, M.μ g ((edgeValEquiv G H φ hφ hind M) (x, z) g) = (∏ f : H.Edge, M.μ (edgeMap G H φ hind f) (x f)) * ∏ r : Rest G H φ hind, M.μ (↑r) (z r)

theorem TriangleInflation.Graph.Transport.mergeVals_edgeVal (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (M : GModel G) (u : H.V) (x : (f : H.Edge) → M.L (edgeMap G H φ hind f)) (z : (r : Rest G H φ hind) → M.L ↑r) : (fun (g : ↥(G.inc (φ u))) => (edgeValEquiv G H φ hφ hind M) (x, z) ↑g) = mergeVals G H φ hφ hind M u (fun (f : ↥(H.inc u)) => x ↑f) z

The observed law of the restricted model

theorem TriangleInflation.Graph.Transport.restrictModel_law (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (P : GTarget H) (M : GModel G) (hM : M.Valid) (hlaw : M.law = transportTarget G H φ P) : (restrictModel G H φ hφ hind M).law = P

Everything the transport proof needs beyond Defs lives in this namespace, so that the generic names do not collide with the rest of the library.

Generic pushforward infrastructure

theorem TriangleInflation.Graph.Transport.TransportFeasible.pushforward_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [DecidableEq β] [DecidableEq γ] (w : α → ℝ) (F : α → β) (K : β → γ) : pushforward (pushforward w F) K = pushforward w (K ∘ F)

Pushforwards compose.

theorem TriangleInflation.Graph.Transport.TransportFeasible.isLaw_pushforward {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] {w : α → ℝ} (h : IsLaw w) (F : α → β) : IsLaw (pushforward w F)

A pushforward of a law is a law.

theorem TriangleInflation.Graph.Transport.TransportFeasible.isLaw_prod {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {w₁ : A → ℝ} {w₂ : B → ℝ} (h₁ : IsLaw w₁) (h₂ : IsLaw w₂) : IsLaw fun (p : A × B) => w₁ p.1 * w₂ p.2

A product of laws is a law.

theorem TriangleInflation.Graph.Transport.TransportFeasible.pushforward_prod_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Fintype A] [Fintype B] [DecidableEq C] [DecidableEq D] (w₁ : A → ℝ) (w₂ : B → ℝ) (K₁ : A → C) (K₂ : B → D) (c : C) (d : D) : (∑ p : A × B, if K₁ p.1 = c ∧ K₂ p.2 = d then w₁ p.1 * w₂ p.2 else 0) = pushforward w₁ K₁ c * pushforward w₂ K₂ d

A pushforward of a product law along a product map, evaluated at a pair of targets.

The uniform law on a finite set of fair bits

noncomputable def TriangleInflation.Graph.Transport.TransportFeasible.unifLaw (A : Type u_1) [Fintype A] : (A → Bool) → ℝ

The law of independent fair bits indexed by A.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.unifLaw A x✝ = (1 / 2) ^ Fintype.card A

theorem TriangleInflation.Graph.Transport.TransportFeasible.unifLaw_isLaw (A : Type u_1) [Fintype A] [DecidableEq A] : IsLaw (unifLaw A)

theorem TriangleInflation.Graph.Transport.TransportFeasible.unifLaw_eq_prodLaw (C : Type u_1) [Fintype C] : unifLaw C = FiniteWeights.prodLaw fun (x : C) (x_1 : Bool) => 1 / 2

theorem TriangleInflation.Graph.Transport.TransportFeasible.unifLaw_restrict {A : Type u_1} {B : Type u_2} [Fintype A] [DecidableEq A] [Fintype B] (ρ : B → A) (hρ : Function.Injective ρ) : (pushforward (unifLaw A) fun (ξ : A → Bool) (b : B) => ξ (ρ b)) = unifLaw B

Restricting independent fair bits along an injection again gives independent fair bits.

The induced edge map

theorem TriangleInflation.Graph.Transport.TransportFeasible.edgeMap_mem_inc (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (u : H.V) (e : H.Edge) (he : e ∈ H.inc u) : edgeMap G H φ hind e ∈ G.inc (φ u)

theorem TriangleInflation.Graph.Transport.TransportFeasible.inc_nonempty (Γ : PairGraph) (v : Γ.V) : (Γ.inc v).Nonempty

Every vertex is incident to a source.

Observations outside the image

def TriangleInflation.Graph.Transport.TransportFeasible.InRange (G H : PairGraph) (φ : H.V → G.V) (v : G.V) : Prop

A vertex of G lies in the image of the embedding.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.InRange G H φ v = ∃ (u : H.V), φ u = v

@[instance_reducible]

instance TriangleInflation.Graph.Transport.TransportFeasible.instDecidableInRange (G H : PairGraph) (φ : H.V → G.V) (v : G.V) : Decidable (InRange G H φ v)

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.instDecidableInRange G H φ v = { decide := decide (∃ a ∈ Finset.univ, (fun (u : H.V) => φ u = v) a), reflects_decide := ⋯ }

@[reducible, inline]

abbrev TriangleInflation.Graph.Transport.TransportFeasible.OutObs (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) : Type

The copied observations of G at vertices outside the image of φ.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.OutObs G H φ t = { o : TriangleInflation.Graph.GObs G t // ¬TriangleInflation.Graph.Transport.TransportFeasible.InRange G H φ o.fst }

@[reducible, inline]

abbrev TriangleInflation.Graph.Transport.TransportFeasible.OutVert (G H : PairGraph) (φ : H.V → G.V) : Type

The vertices of G outside the image of φ.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.OutVert G H φ = { v : G.V // ¬TriangleInflation.Graph.Transport.TransportFeasible.InRange G H φ v }

def TriangleInflation.Graph.Transport.TransportFeasible.pullObs (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (o : GObs G t) (u : H.V) (h : φ u = o.fst) : GObs H t

The H-observation that a G-observation at an image vertex reads: it keeps only the copy indices of the sources coming from H.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.pullObs G H φ hind t o u h = ⟨u, fun (f : ↥(H.inc u)) => o.snd ⟨TriangleInflation.Graph.Transport.edgeMap G H φ hind ↑f, ⋯⟩⟩

theorem TriangleInflation.Graph.Transport.TransportFeasible.pullObs_congr (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (o : GObs G t) (u u' : H.V) (h : φ u = o.fst) (h' : φ u' = o.fst) (huu : u = u') : pullObs G H φ hind t o u h = pullObs G H φ hind t o u' h'

noncomputable def TriangleInflation.Graph.Transport.TransportFeasible.extAssign (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (p : GAssign H t × (OutObs G H φ t → Bool)) : GAssign G t

The extension of an H-witness assignment together with a family of outside fair bits to a G-witness assignment.

Equations

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

theorem TriangleInflation.Graph.Transport.TransportFeasible.extAssign_in (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (p : GAssign H t × (OutObs G H φ t → Bool)) (o : GObs G t) (u : H.V) (h : φ u = o.fst) : extAssign G H φ hind t p o = p.1 (pullObs G H φ hind t o u h)

theorem TriangleInflation.Graph.Transport.TransportFeasible.extAssign_out (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (p : GAssign H t × (OutObs G H φ t → Bool)) (o : GObs G t) (h : ¬InRange G H φ o.fst) : extAssign G H φ hind t p o = p.2 ⟨o, h⟩

The transported witness

noncomputable def TriangleInflation.Graph.Transport.TransportFeasible.transportSource (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) (ΔH : GAssign H t → ℝ) : GAssign H t × (OutObs G H φ t → Bool) → ℝ

The law on the source type of the extension: an H-witness, and one independent fair bit for every copied observation of G outside the image of φ.

Equations

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

noncomputable def TriangleInflation.Graph.Transport.TransportFeasible.transportWitness (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (ΔH : GAssign H t → ℝ) : GAssign G t → ℝ

The transported witness: the pushforward of transportSource along the extension map.

Equations

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

theorem TriangleInflation.Graph.Transport.TransportFeasible.transportSource_isLaw (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) {ΔH : GAssign H t → ℝ} (h : IsLaw ΔH) : IsLaw (transportSource G H φ t ΔH)

theorem TriangleInflation.Graph.Transport.TransportFeasible.transportWitness_isLaw (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) {ΔH : GAssign H t → ℝ} (h : IsLaw ΔH) : IsLaw (transportWitness G H φ hind t ΔH)

The diagonal law

def TriangleInflation.Graph.Transport.TransportFeasible.diagOutObs (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) (q : Fin t × OutVert G H φ) : OutObs G H φ t

The diagonal copied observation of an outside vertex in row r.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.diagOutObs G H φ t q = ⟨⟨↑q.2, fun (x : ↥(G.inc ↑q.2)) => q.1⟩, ⋯⟩

theorem TriangleInflation.Graph.Transport.TransportFeasible.diagOutObs_injective (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) : Function.Injective (diagOutObs G H φ t)

theorem TriangleInflation.Graph.Transport.TransportFeasible.extAssign_diag_in (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (p : GAssign H t × (OutObs G H φ t → Bool)) (r : Fin t) (u : H.V) : extAssign G H φ hind t p (copyObs (fun (x : G.Edge) => r) (φ u)) = readDiag p.1 r u

theorem TriangleInflation.Graph.Transport.TransportFeasible.extAssign_diag_out (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (p : GAssign H t × (OutObs G H φ t → Bool)) (r : Fin t) (w : OutVert G H φ) : extAssign G H φ hind t p (copyObs (fun (x : G.Edge) => r) ↑w) = p.2 (diagOutObs G H φ t (r, w))

theorem TriangleInflation.Graph.Transport.TransportFeasible.readDiag_extAssign_iff (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (p : GAssign H t × (OutObs G H φ t → Bool)) (v : Fin t → G.V → Bool) : readDiag (extAssign G H φ hind t p) = v ↔ (readDiag p.1 = fun (r : Fin t) (u : H.V) => v r (φ u)) ∧ (fun (q : Fin t × OutVert G H φ) => p.2 (diagOutObs G H φ t q)) = fun (q : Fin t × OutVert G H φ) => v q.1 ↑q.2

theorem TriangleInflation.Graph.Transport.TransportFeasible.card_outVert (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) : Fintype.card (OutVert G H φ) = Fintype.card G.V - Fintype.card H.V

theorem TriangleInflation.Graph.Transport.TransportFeasible.transport_diag (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (P : GTarget H) (ΔH : GAssign H t → ℝ) (hdiag : pushforward ΔH readDiag = gTensorPow t P) : pushforward (transportWitness G H φ hind t ΔH) readDiag = gTensorPow t (transportTarget G H φ P)

Symmetry

def TriangleInflation.Graph.Transport.TransportFeasible.gPermEquiv {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) : GObs Γ t ≃ GObs Γ t

The action of a per-source permutation of copy indices, as an equivalence.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.gPermEquiv π = Equiv.sigmaCongrRight fun (x : Γ.V) => Equiv.piCongrRight fun (e : ↥(Γ.inc x)) => π ↑e

theorem TriangleInflation.Graph.Transport.TransportFeasible.gPermEquiv_apply {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) (o : GObs Γ t) : (gPermEquiv π) o = gPerm π o

def TriangleInflation.Graph.Transport.TransportFeasible.precompEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ α) : (α → β) ≃ (α → β)

Precomposition with an equivalence of the index type.

Equations

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

theorem TriangleInflation.Graph.Transport.TransportFeasible.gRelabel_injective {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) : Function.Injective (gRelabel π)

def TriangleInflation.Graph.Transport.TransportFeasible.outPermEquiv (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) (π : G.Edge → Equiv.Perm (Fin t)) : OutObs G H φ t ≃ OutObs G H φ t

Copy-index permutations act on the outside observations.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.outPermEquiv G H φ t π = (TriangleInflation.Graph.Transport.TransportFeasible.gPermEquiv π).subtypeEquiv ⋯

def TriangleInflation.Graph.Transport.TransportFeasible.srcPermEquiv (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (π : G.Edge → Equiv.Perm (Fin t)) : GAssign H t × (OutObs G H φ t → Bool) ≃ GAssign H t × (OutObs G H φ t → Bool)

The action of a G-permutation on the source type of the extension.

Equations

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

theorem TriangleInflation.Graph.Transport.TransportFeasible.extAssign_relabel (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (π : G.Edge → Equiv.Perm (Fin t)) (p : GAssign H t × (OutObs G H φ t → Bool)) : extAssign G H φ hind t ((srcPermEquiv G H φ hind t π) p) = gRelabel π (extAssign G H φ hind t p)

theorem TriangleInflation.Graph.Transport.TransportFeasible.transport_symmetric (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (ΔH : GAssign H t → ℝ) (hsym : GSymmetric t ΔH) : GSymmetric t (transportWitness G H φ hind t ΔH)

Splitting an outcome of G into its H-part and its outside part

noncomputable def TriangleInflation.Graph.Transport.TransportFeasible.mergeVert (G H : PairGraph) (φ : H.V → G.V) (q : (H.V → Bool) × (OutVert G H φ → Bool)) : G.V → Bool

The outcome of G assembled from an H-outcome and an outside outcome.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.mergeVert G H φ q v = if h : TriangleInflation.Graph.Transport.TransportFeasible.InRange G H φ v then q.1 (Exists.choose h) else q.2 ⟨v, h⟩

theorem TriangleInflation.Graph.Transport.TransportFeasible.mergeVert_in (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (q : (H.V → Bool) × (OutVert G H φ → Bool)) (u : H.V) : mergeVert G H φ q (φ u) = q.1 u

theorem TriangleInflation.Graph.Transport.TransportFeasible.mergeVert_out (G H : PairGraph) (φ : H.V → G.V) (q : (H.V → Bool) × (OutVert G H φ → Bool)) (v : G.V) (h : ¬InRange G H φ v) : mergeVert G H φ q v = q.2 ⟨v, h⟩

noncomputable def TriangleInflation.Graph.Transport.TransportFeasible.vertEquiv (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) : (H.V → Bool) × (OutVert G H φ → Bool) ≃ (G.V → Bool)

Outcomes of G split as an H-outcome together with an outcome on the outside vertices.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.vertEquiv G H φ hφ = TriangleInflation.Graph.Transport.vtxEquiv G H φ hφ

The two parts of an injectable set

theorem TriangleInflation.Graph.Transport.TransportFeasible.copyObs_fst {Γ : PairGraph} {t : ℕ} (ι : Γ.Edge → Fin t) (v : Γ.V) : (copyObs ι v).fst = v

theorem TriangleInflation.Graph.Transport.TransportFeasible.mem_copySet_self {Γ : PairGraph} {t : ℕ} (ι : Γ.Edge → Fin t) (o : GObs Γ t) (h : o ∈ copySet ι) : o = copyObs ι o.fst

theorem TriangleInflation.Graph.Transport.TransportFeasible.extAssign_copy_in (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (ι : G.Edge → Fin t) (p : GAssign H t × (OutObs G H φ t → Bool)) (u : H.V) : extAssign G H φ hind t p (copyObs ι (φ u)) = p.1 (copyObs (fun (f : H.Edge) => ι (edgeMap G H φ hind f)) u)

def TriangleInflation.Graph.Transport.TransportFeasible.injPart (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (S : Finset (GObs G t)) (ι : G.Edge → Fin t) : Finset (GObs H t)

The H-part of an injectable set of copied observations of G.

Equations

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

def TriangleInflation.Graph.Transport.TransportFeasible.outPart (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) (S : Finset (GObs G t)) : Finset (OutObs G H φ t)

The outside part of a set of copied observations of G.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.outPart G H φ t S = {x : TriangleInflation.Graph.Transport.TransportFeasible.OutObs G H φ t | ↑x ∈ S}

def TriangleInflation.Graph.Transport.TransportFeasible.outVertPart (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) (S : Finset (GObs G t)) (ι : G.Edge → Fin t) : Finset (OutVert G H φ)

The outside vertices read by an injectable set of copied observations of G.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.outVertPart G H φ t S ι = {v : TriangleInflation.Graph.Transport.TransportFeasible.OutVert G H φ | TriangleInflation.Graph.copyObs ι ↑v ∈ S}

def TriangleInflation.Graph.Transport.TransportFeasible.readInjPart (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (S : Finset (GObs G t)) (ι : G.Edge → Fin t) (ψ : ↥S → Bool) : ↥(injPart G H φ hind t S ι) → Bool

The outcome pattern that the H-part inherits.

Equations

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

def TriangleInflation.Graph.Transport.TransportFeasible.readOutPart (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) (S : Finset (GObs G t)) (ψ : ↥S → Bool) : ↥(outPart G H φ t S) → Bool

The outcome pattern that the outside part inherits.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.readOutPart G H φ t S ψ x = if h : ↑↑x ∈ S then ψ ⟨↑↑x, h⟩ else false

def TriangleInflation.Graph.Transport.TransportFeasible.readOutVertPart (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) (S : Finset (GObs G t)) (ι : G.Edge → Fin t) (ψ : ↥S → Bool) : ↥(outVertPart G H φ t S ι) → Bool

The outcome pattern that the outside vertices inherit.

Equations

• TriangleInflation.Graph.Transport.TransportFeasible.readOutVertPart G H φ t S ι ψ x = if h : TriangleInflation.Graph.copyObs ι ↑↑x ∈ S then ψ ⟨TriangleInflation.Graph.copyObs ι ↑↑x, h⟩ else false

theorem TriangleInflation.Graph.Transport.TransportFeasible.readInjPart_apply (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (S : Finset (GObs G t)) (ι : G.Edge → Fin t) (ψ : ↥S → Bool) (u : H.V) (hu : copyObs ι (φ u) ∈ S) (hy : copyObs (fun (f : H.Edge) => ι (edgeMap G H φ hind f)) u ∈ injPart G H φ hind t S ι) : readInjPart G H φ hind t S ι ψ ⟨copyObs (fun (f : H.Edge) => ι (edgeMap G H φ hind f)) u, hy⟩ = ψ ⟨copyObs ι (φ u), hu⟩

theorem TriangleInflation.Graph.Transport.TransportFeasible.injPart_injectable (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (S : Finset (GObs G t)) (ι : G.Edge → Fin t) : GInjectable (injPart G H φ hind t S ι)

theorem TriangleInflation.Graph.Transport.TransportFeasible.card_outPart_eq (G H : PairGraph) (φ : H.V → G.V) (t : ℕ) (S : Finset (GObs G t)) (ι : G.Edge → Fin t) (hS : S ⊆ copySet ι) : (outPart G H φ t S).card = (outVertPart G H φ t S ι).card

theorem TriangleInflation.Graph.Transport.TransportFeasible.gRestrict_extAssign_iff (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (S : Finset (GObs G t)) (ι : G.Edge → Fin t) (hS : S ⊆ copySet ι) (ψ : ↥S → Bool) (p : GAssign H t × (OutObs G H φ t → Bool)) : gRestrict S (extAssign G H φ hind t p) = ψ ↔ gRestrict (injPart G H φ hind t S ι) p.1 = readInjPart G H φ hind t S ι ψ ∧ (fun (x : ↥(outPart G H φ t S)) => p.2 ↑x) = readOutPart G H φ t S ψ

theorem TriangleInflation.Graph.Transport.TransportFeasible.gPartyRead_mergeVert_iff (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (S : Finset (GObs G t)) (ι : G.Edge → Fin t) (hS : S ⊆ copySet ι) (ψ : ↥S → Bool) (q : (H.V → Bool) × (OutVert G H φ → Bool)) : gPartyRead S (mergeVert G H φ q) = ψ ↔ gPartyRead (injPart G H φ hind t S ι) q.1 = readInjPart G H φ hind t S ι ψ ∧ (fun (x : ↥(outVertPart G H φ t S ι)) => q.2 ↑x) = readOutVertPart G H φ t S ι ψ

theorem TriangleInflation.Graph.Transport.TransportFeasible.transportTarget_partyRead_split (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (P : GTarget H) (S : Finset (GObs G t)) (ι : G.Edge → Fin t) (hS : S ⊆ copySet ι) (ψ : ↥S → Bool) : pushforward (transportTarget G H φ P) (gPartyRead S) ψ = pushforward P (gPartyRead (injPart G H φ hind t S ι)) (readInjPart G H φ hind t S ι ψ) * (1 / 2) ^ (outVertPart G H φ t S ι).card

The marginal of the transported target on an injectable set factorizes into the marginal of P on the H-part and fair bits on the outside vertices it reads.

Ancestry

theorem TriangleInflation.Graph.Transport.TransportFeasible.mem_gAncestors_copyObs {Γ : PairGraph} {t : ℕ} (ι : Γ.Edge → Fin t) (v : Γ.V) (e : Γ.Edge) (he : e ∈ Γ.inc v) : (e, ι e) ∈ gAncestors (copyObs ι v)

theorem TriangleInflation.Graph.Transport.TransportFeasible.gAncestors_copyObs_mem {Γ : PairGraph} {t : ℕ} (ι : Γ.Edge → Fin t) (v : Γ.V) (z : GLatent Γ t) (hz : z ∈ gAncestors (copyObs ι v)) : z.1 ∈ Γ.inc v ∧ z.2 = ι z.1

theorem TriangleInflation.Graph.Transport.TransportFeasible.ai_disjoint {Γ : PairGraph} {t : ℕ} (S T : Finset (GObs Γ t)) (h : GAncestrallyIndependent S T) : Disjoint S T

Ancestrally independent sets are disjoint: no copied observation is parentless.

theorem TriangleInflation.Graph.Transport.TransportFeasible.injPart_ai (G H : PairGraph) (φ : H.V → G.V) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (S T : Finset (GObs G t)) (ιS ιT : G.Edge → Fin t) (h : GAncestrallyIndependent S T) : GAncestrallyIndependent (injPart G H φ hind t S ιS) (injPart G H φ hind t T ιT)

Ancestral independence in G is inherited by the H-parts.

theorem TriangleInflation.Graph.Transport.TransportFeasible.unifLaw_restrictPi {A : Type u_1} [Fintype A] [DecidableEq A] {n : ℕ} {β : Fin n → Type u_2} [(m : Fin n) → Fintype (β m)] (ρ : (m : Fin n) × β m → A) (hρ : Function.Injective ρ) (η : (m : Fin n) → β m → Bool) : pushforward (unifLaw A) (fun (ξ : A → Bool) (m : Fin n) (b : β m) => ξ (ρ ⟨m, b⟩)) η = (1 / 2) ^ ∑ m : Fin n, Fintype.card (β m)

Independent fair bits restricted along a family of injections indexed by a sigma type.

Injectable marginals and ancestral products

theorem TriangleInflation.Graph.Transport.TransportFeasible.transport_injectableMarginals (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (P : GTarget H) (ΔH : GAssign H t → ℝ) (hinj : GInjectableMarginals t ΔH P) : GInjectableMarginals t (transportWitness G H φ hind t ΔH) (transportTarget G H φ P)

Every G-injectable set carries the corresponding marginal of the transported target.

theorem TriangleInflation.Graph.Transport.TransportFeasible.transport_ancestralProducts (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (P : GTarget H) (ΔH : GAssign H t → ℝ) (hprod : GAncestralProducts t ΔH P) : GAncestralProducts t (transportWitness G H φ hind t ΔH) (transportTarget G H φ P)

Every finite family of pairwise ancestrally independent G-injectable sets carries the product of the corresponding marginals of the transported target.

theorem TriangleInflation.Graph.transport_ai_feasible (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (t : ℕ) (P : GTarget H) (hAI : GAIFeasible H t P) : GAIFeasible G t (transportTarget G H φ P)

Transport of a witness (AUDIT-NOTES A6, forward half; paper lem:transport(ii)). An H-witness extends to a G-witness: a copied observation at an H-vertex ignores the copy indices of the edges leaving H, and every copied observation at an outside vertex gets its own independent fair bit.

theorem TriangleInflation.Graph.transport_compatible_restrict (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (P : GTarget H) (hc : GCompatible G (transportTarget G H φ P)) : GCompatible H P

Restriction of a model (AUDIT-NOTES A6, backward half; paper lem:transport(i)). A G-model for P ⊗ fair restricts to an H-model for P: by inducedness a source of G outside the image of H is read by at most one H-vertex, so it can be averaged out locally as private randomness at that vertex, and the fair bits outside integrate to one.

theorem TriangleInflation.Graph.induced_transport (G H : PairGraph) (φ : H.V → G.V) (hφ : Function.Injective φ) (hind : ∀ (u v : H.V), H.G.Adj u v ↔ G.G.Adj (φ u) (φ v)) (hconn : H.G.Connected) (t : ℕ) (P : GTarget H) (hAI : GAIFeasible H t P) (hinc : ¬GCompatible H P) : GAIFeasible G t (transportTarget G H φ P) ∧ ¬GCompatible G (transportTarget G H φ P)

AUDIT-NOTES A6, induced-subgraph transport. If H embeds in G as an induced connected subgraph and P is an H-target that passes the order-t AI test but is incompatible, then P tensored with fair bits on the remaining vertices of G passes the order-t AI test for G and is incompatible for G. Forward: a G-model restricted to V(H) is an H-model, since a crossing source reaches only one H-vertex and can be absorbed as private randomness, and inducedness means there are no extra internal sources. Backward: extend the H-witness by ignoring crossing-edge indices at H-vertices and giving independent fair bits to the outside observations.

Exhaustion: the two induced subgraphs

The graph theory behind exhaustion. Everything in this section is about a bare SimpleGraph; PairGraph plays no role until the theorem itself.

theorem TriangleInflation.Graph.Exhaustion.induced_cycle_of_not_acyclic {V : Type} [Finite V] (G : SimpleGraph V) (hnac : ¬G.IsAcyclic) : ∃ (m : ℕ) (_ : 3 ≤ m) (ψ : Fin m → V), Function.Injective ψ ∧ ∀ (a b : Fin m), (cycleAdj m).Adj a b ↔ G.Adj (ψ a) (ψ b)

theorem TriangleInflation.Graph.Exhaustion.dist_getVert_of_shortest {V : Type} (G : SimpleGraph V) {u v : V} (p : G.Walk u v) (hp : p.length = G.dist u v) {i j : ℕ} (hij : i ≤ j) (hj : j ≤ p.length) : G.dist (p.getVert i) (p.getVert j) = j - i

Subwalks of a shortest walk are shortest: for a walk p from u to v whose length realizes G.dist u v, and i ≤ j ≤ p.length, the distance between the i-th and j-th vertices of p is exactly j - i.

theorem TriangleInflation.Graph.Exhaustion.dist_getVert_of_shortest' {V : Type} (G : SimpleGraph V) {u v : V} (p : G.Walk u v) (hp : p.length = G.dist u v) {i j : ℕ} (hi : i ≤ p.length) (hj : j ≤ p.length) : G.dist (p.getVert i) (p.getVert j) = max i j - min i j

Symmetric form of dist_getVert_of_shortest.

theorem TriangleInflation.Graph.Exhaustion.induced_path5_of_dist {V : Type} (G : SimpleGraph V) (u v : V) (hd : 4 ≤ G.dist u v) : ∃ (ψ : Fin 5 → V), Function.Injective ψ ∧ ∀ (a b : Fin 5), (pathAdj 5).Adj a b ↔ G.Adj (ψ a) (ψ b)

theorem TriangleInflation.Graph.exhaustion (Γ : PairGraph) (hconn : Γ.G.Connected) (hnot : ¬IsDoubleStarForest Γ.G) : (∃ (m : ℕ) (_ : 3 ≤ m) (φ : Fin m → Γ.V), Function.Injective φ ∧ ∀ (u v : Fin m), (cycleAdj m).Adj u v ↔ Γ.G.Adj (φ u) (φ v)) ∨ ∃ (φ : Fin 5 → Γ.V), Function.Injective φ ∧ ∀ (u v : Fin 5), (pathAdj 5).Adj u v ↔ Γ.G.Adj (φ u) (φ v)

AUDIT-NOTES A6, exhaustion. A connected pair graph that is not a double star contains an induced cycle (a shortest cycle) or an induced P₅ (five consecutive vertices of a geodesic in a tree of diameter at least four).