Local flips

Statements split from the original Statements.lean skeleton (one file per proving task). Every statement here is proved except flip_gExpFeasible; see AUDIT-NOTES for the mathematics.

The mathematics of this file is that flipKernel η is the product kernel of independent per-coordinate flips. Three structural facts carry every statement below.

• flipKernel_sum: each row of the kernel is a law, so flips preserve laws.
• flipLaw_pushforward: flips commute with marginalization to an injectively selected set of coordinates. Injectivity is what makes the selected flips independent; it fails for a selection that reads one coordinate twice, and each application below supplies its own injectivity (the diagonal rows are distinct because no vertex is isolated, an injectable set has one copied observation per vertex, ancestrally independent blocks are disjoint).
• flipLaw_sigma: the flip of a product law over disjoint blocks is the product of the flipped blocks.

Finite-sum helpers

theorem TriangleInflation.Graph.Flips.sum_prod_pi {α : Type u_1} [Fintype α] [DecidableEq α] {β : α → Type u_2} [(a : α) → Fintype (β a)] (g : (a : α) → β a → ℝ) : ∑ v : (a : α) → β a, ∏ a : α, g a (v a) = ∏ a : α, ∑ b : β a, g a b

Summing a product of per-coordinate weights over all dependent functions factorizes into the product of the per-coordinate sums.

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

Integrating a function against a pushforward is integrating its pullback.

theorem TriangleInflation.Graph.Flips.pushforward_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq β] [DecidableEq γ] (w : α → ℝ) (F : α → β) (e : β ≃ γ) (c : γ) : pushforward w (fun (a : α) => e (F a)) c = pushforward w F (e.symm c)

Postcomposing the read map with a bijection transports the pushforward.

theorem TriangleInflation.Graph.Flips.pushforward_equiv' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq β] [DecidableEq γ] (w : α → ℝ) (F : α → β) (e : β ≃ γ) (b : β) : pushforward w F b = pushforward w (fun (a : α) => e (F a)) (e b)

The same, read as a change of coordinates on the target of the read map.

The flip kernel

theorem TriangleInflation.Graph.Flips.flipKernel_nonneg {ι : Type} [Fintype ι] {η : ℝ} (h0 : 0 ≤ η) (h1 : η ≤ 1) (x y : ι → Bool) : 0 ≤ flipKernel η x y

Every transition probability of the flip kernel is nonnegative for η ∈ [0,1].

theorem TriangleInflation.Graph.Flips.flipKernel_pos {ι : Type} [Fintype ι] {η : ℝ} (h0 : 0 < η) (h1 : η < 1) (x y : ι → Bool) : 0 < flipKernel η x y

Every transition probability of the flip kernel is positive for η ∈ (0,1).

theorem TriangleInflation.Graph.Flips.flipKernel_sum {ι : Type} [Fintype ι] [DecidableEq ι] (η : ℝ) (x : ι → Bool) : ∑ y : ι → Bool, flipKernel η x y = 1

Each row of the flip kernel is a law: the per-coordinate weights 1 - η and η sum to one, for every η.

theorem TriangleInflation.Graph.Flips.flipKernel_comp {ι κ : Type} [Fintype ι] [Fintype κ] (η : ℝ) (e : κ ≃ ι) (x y : ι → Bool) : (flipKernel η (fun (j : κ) => x (e j)) fun (j : κ) => y (e j)) = flipKernel η x y

The flip kernel is exchangeable: relabelling the coordinates by a bijection leaves it unchanged.

theorem TriangleInflation.Graph.Flips.flipKernel_marginal {ι κ : Type} [Fintype ι] [DecidableEq ι] [Fintype κ] (η : ℝ) {f : κ → ι} (hf : Function.Injective f) (x : ι → Bool) (z : κ → Bool) : pushforward (flipKernel η x) (fun (ω : ι → Bool) (j : κ) => ω (f j)) z = flipKernel η (fun (j : κ) => x (f j)) z

Marginalizing the flip kernel to an injectively selected set of coordinates gives the flip kernel of the selected coordinates: the unselected coordinates sum out.

Flips against marginals and products

theorem TriangleInflation.Graph.Flips.flipLaw_pushforward {ι κ : Type} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (η : ℝ) {f : κ → ι} (hf : Function.Injective f) (P : (ι → Bool) → ℝ) : (pushforward (flipLaw η P) fun (ω : ι → Bool) (j : κ) => ω (f j)) = flipLaw η (pushforward P fun (ω : ι → Bool) (j : κ) => ω (f j))

Flips commute with marginalization to an injectively selected set of coordinates: the marginal of a flipped law is the flipped marginal.

theorem TriangleInflation.Graph.Flips.flipLaw_sigma {α : Type} [Fintype α] [DecidableEq α] {β : α → Type} [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] (η : ℝ) (Q : (a : α) → (β a → Bool) → ℝ) (U : (a : α) × β a → Bool) : flipLaw η (fun (u : (a : α) × β a → Bool) => ∏ a : α, Q a fun (b : β a) => u ⟨a, b⟩) U = ∏ a : α, flipLaw η (Q a) fun (b : β a) => U ⟨a, b⟩

Flips of a law that is a product over disjoint blocks are the product of the flipped blocks: independent flips factorize along the blocks.

Injectivity of the selections used below

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

No vertex is isolated, so every vertex carries at least one source.

theorem TriangleInflation.Graph.Flips.gAncestors_nonempty {Γ : PairGraph} {t : ℕ} (o : GObs Γ t) : (gAncestors o).Nonempty

Every copied observation has at least one copied latent ancestor.

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

Ancestrally independent sets of copied observations are disjoint: a shared member would contribute its (nonempty) set of ancestors to both.

theorem TriangleInflation.Graph.Flips.injectable_vertex_injective {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} (hS : GInjectable S) : Function.Injective fun (o : ↥S) => (↑o).fst

On an injectable set the vertex determines the copied observation, so the party read is an injective selection of coordinates.

def TriangleInflation.Graph.Flips.diagObs (Γ : PairGraph) (t : ℕ) (p : (_ : Fin t) × Γ.V) : GObs Γ t

The copied observation that diagonal row r reads at vertex v.

Equations

• TriangleInflation.Graph.Flips.diagObs Γ t p = ⟨p.snd, fun (x : ↥(Γ.inc p.snd)) => p.fst⟩

theorem TriangleInflation.Graph.Flips.readDiag_eq {Γ : PairGraph} {t : ℕ} (ω : GAssign Γ t) (r : Fin t) (v : Γ.V) : readDiag ω r v = ω (diagObs Γ t ⟨r, v⟩)

theorem TriangleInflation.Graph.Flips.readDiag_factor (Γ : PairGraph) (t : ℕ) : readDiag = fun (ω : GAssign Γ t) => (Equiv.piCurry fun (x : Fin t) (x_1 : Γ.V) => Bool) fun (p : (_ : Fin t) × Γ.V) => ω (diagObs Γ t p)

The diagonal read is the curried selection of the diagonal observations.

theorem TriangleInflation.Graph.Flips.diagObs_injective (Γ : PairGraph) (t : ℕ) : Function.Injective (diagObs Γ t)

The t · |V| diagonal observations are distinct: the vertex is the first component, and the row index is recovered from any incident source, of which there is at least one.

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

Relabelling copy indices is a bijection of copied observations.

Equations

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

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

Relabelling copy indices is a bijection of assignments.

Equations

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

Local flips

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

Independent flips of every coordinate with probability η ∈ [0,1] send laws to laws.

theorem TriangleInflation.Graph.flip_full_support {ι : Type} [Fintype ι] [DecidableEq ι] (η : ℝ) (h0 : 0 < η) (h1 : η < 1) (P : (ι → Bool) → ℝ) (hP : IsLaw P) (y : ι → Bool) : 0 < flipLaw η P y

Flips with 0 < η < 1 make every atom strictly positive (AUDIT-NOTES A7).

theorem TriangleInflation.Graph.flip_symmetric {Γ : PairGraph} {t : ℕ} (η : ℝ) (Δ : GAssign Γ t → ℝ) (h : GSymmetric t Δ) : GSymmetric t (flipLaw η Δ)

Flipping every copied observation independently preserves symmetry under the copy-index action, because the flip kernel is exchangeable.

theorem TriangleInflation.Graph.flip_diagonal {Γ : PairGraph} {t : ℕ} (η : ℝ) (Δ : GAssign Γ t → ℝ) (P : GTarget Γ) (h : pushforward Δ readDiag = gTensorPow t P) : pushforward (flipLaw η Δ) readDiag = gTensorPow t (flipLaw η P)

Flipping the witness flips the diagonal law: the t · |V| diagonal observations are distinct, so their flips are independent, and the diagonal law of the flipped witness is the tensor power of the flipped target.

theorem TriangleInflation.Graph.flip_injectableMarginals {Γ : PairGraph} {t : ℕ} (η : ℝ) (Δ : GAssign Γ t → ℝ) (P : GTarget Γ) (h : GInjectableMarginals t Δ P) : GInjectableMarginals t (flipLaw η Δ) (flipLaw η P)

Flips preserve the injectable-marginal prescriptions: an injectable set has one copied observation per vertex, so the flips on it are independent.

theorem TriangleInflation.Graph.flip_ancestralProducts {Γ : PairGraph} {t : ℕ} (η : ℝ) (Δ : GAssign Γ t → ℝ) (P : GTarget Γ) (h : GAncestralProducts t Δ P) : GAncestralProducts t (flipLaw η Δ) (flipLaw η P)

Flips preserve the ancestral-independence prescriptions: ancestrally independent blocks are disjoint sets of copied observations, so the flips across blocks are independent.

theorem TriangleInflation.Graph.flip_gAIFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) (h : GAIFeasible Γ t P) : GAIFeasible Γ t (flipLaw η P)

The packaged consequence: local flips of the target stay AI feasible at the same order.