The triangle specialization

Statements split from the original Statements.lean skeleton (one file per proving task). See AUDIT-NOTES for the mathematics.

The triangle specialization

triangleGraph = cycle 3 is the scenario of TriangleInflation, with vertex 0 the party A, vertex 1 the party B and vertex 2 the party C.

The triangle bridge

The named sources of C₃, the induced bijections of copied observations, assignments, sets and copied latent sources, and the transport lemmas used by the four theorems below. The naming follows the file header of InflationGraph.Defs: the source {0,1} is the paper's X, the source {1,2} is Y and the source {0,2} is Z.

def TriangleInflation.Graph.triEdgeX : triangleGraph.Edge

The triangle source shared by parties A and B.

Equations

• TriangleInflation.Graph.triEdgeX = ⟨s(0, 1), TriangleInflation.Graph.triEdgeX._proof_1⟩

def TriangleInflation.Graph.triEdgeY : triangleGraph.Edge

The triangle source shared by parties B and C.

Equations

• TriangleInflation.Graph.triEdgeY = ⟨s(1, 2), TriangleInflation.Graph.triEdgeY._proof_1⟩

def TriangleInflation.Graph.triEdgeZ : triangleGraph.Edge

The triangle source shared by parties A and C.

Equations

• TriangleInflation.Graph.triEdgeZ = ⟨s(0, 2), TriangleInflation.Graph.triEdgeZ._proof_1⟩

def TriangleInflation.Graph.triInc0X : ↥(triangleGraph.inc 0)

Source X viewed as an edge incident to vertex 0.

Equations

• TriangleInflation.Graph.triInc0X = ⟨TriangleInflation.Graph.triEdgeX, TriangleInflation.Graph.triInc0X._proof_1⟩

def TriangleInflation.Graph.triInc0Z : ↥(triangleGraph.inc 0)

Source Z viewed as an edge incident to vertex 0.

Equations

• TriangleInflation.Graph.triInc0Z = ⟨TriangleInflation.Graph.triEdgeZ, TriangleInflation.Graph.triInc0Z._proof_1⟩

def TriangleInflation.Graph.triInc1X : ↥(triangleGraph.inc 1)

Source X viewed as an edge incident to vertex 1.

Equations

• TriangleInflation.Graph.triInc1X = ⟨TriangleInflation.Graph.triEdgeX, TriangleInflation.Graph.triInc1X._proof_1⟩

def TriangleInflation.Graph.triInc1Y : ↥(triangleGraph.inc 1)

Source Y viewed as an edge incident to vertex 1.

Equations

• TriangleInflation.Graph.triInc1Y = ⟨TriangleInflation.Graph.triEdgeY, TriangleInflation.Graph.triInc1Y._proof_1⟩

def TriangleInflation.Graph.triInc2Z : ↥(triangleGraph.inc 2)

Source Z viewed as an edge incident to vertex 2.

Equations

• TriangleInflation.Graph.triInc2Z = ⟨TriangleInflation.Graph.triEdgeZ, TriangleInflation.Graph.triInc2Z._proof_1⟩

def TriangleInflation.Graph.triInc2Y : ↥(triangleGraph.inc 2)

Source Y viewed as an edge incident to vertex 2.

Equations

• TriangleInflation.Graph.triInc2Y = ⟨TriangleInflation.Graph.triEdgeY, TriangleInflation.Graph.triInc2Y._proof_1⟩

theorem TriangleInflation.Graph.triInc0_cases (e : ↥(triangleGraph.inc 0)) : e = triInc0X ∨ e = triInc0Z

theorem TriangleInflation.Graph.triInc1_cases (e : ↥(triangleGraph.inc 1)) : e = triInc1X ∨ e = triInc1Y

theorem TriangleInflation.Graph.triInc2_cases (e : ↥(triangleGraph.inc 2)) : e = triInc2Z ∨ e = triInc2Y

def TriangleInflation.Graph.triObs {t : ℕ} (o : GObs triangleGraph t) : Obs t

Translate a graph observation into the named triangle observation.

Equations

• TriangleInflation.Graph.triObs ⟨⟨0, isLt⟩, f⟩ = TriangleInflation.Obs.A (f TriangleInflation.Graph.triInc0X) (f TriangleInflation.Graph.triInc0Z)
• TriangleInflation.Graph.triObs ⟨⟨1, isLt⟩, f⟩ = TriangleInflation.Obs.B (f TriangleInflation.Graph.triInc1X) (f TriangleInflation.Graph.triInc1Y)
• TriangleInflation.Graph.triObs ⟨⟨2, isLt⟩, f⟩ = TriangleInflation.Obs.C (f TriangleInflation.Graph.triInc2Z) (f TriangleInflation.Graph.triInc2Y)
• TriangleInflation.Graph.triObs ⟨⟨n.succ.succ.succ, h⟩, snd⟩ = absurd h ⋯

def TriangleInflation.Graph.triObsInv {t : ℕ} : Obs t → GObs triangleGraph t

Translate a named triangle observation into its graph representation.

Equations

• TriangleInflation.Graph.triObsInv (TriangleInflation.Obs.A i j) = ⟨0, fun (e : ↥(TriangleInflation.Graph.triangleGraph.inc 0)) => if e = TriangleInflation.Graph.triInc0X then i else j⟩
• TriangleInflation.Graph.triObsInv (TriangleInflation.Obs.B i k) = ⟨1, fun (e : ↥(TriangleInflation.Graph.triangleGraph.inc 1)) => if e = TriangleInflation.Graph.triInc1X then i else k⟩
• TriangleInflation.Graph.triObsInv (TriangleInflation.Obs.C j k) = ⟨2, fun (e : ↥(TriangleInflation.Graph.triangleGraph.inc 2)) => if e = TriangleInflation.Graph.triInc2Z then j else k⟩

def TriangleInflation.Graph.triEquiv (t : ℕ) : GObs triangleGraph t ≃ Obs t

Identify graph observations with the named triangle observations.

Equations

• TriangleInflation.Graph.triEquiv t = { toFun := TriangleInflation.Graph.triObs, invFun := TriangleInflation.Graph.triObsInv, left_inv := ⋯, right_inv := ⋯ }

The permutation correspondence

theorem TriangleInflation.Graph.triEdge_cases (e : triangleGraph.Edge) : e = triEdgeX ∨ e = triEdgeZ ∨ e = triEdgeY

theorem TriangleInflation.Graph.triEdge_eq_Y (e : triangleGraph.Edge) : ¬e = triEdgeX → ¬e = triEdgeZ → e = triEdgeY

def TriangleInflation.Graph.triPiEdgeEquiv (L : triangleGraph.Edge → Type u) : ((e : triangleGraph.Edge) → L e) ≃ L triEdgeX × L triEdgeZ × L triEdgeY

Identify an edge-indexed latent assignment with its X, Z, Y coordinates.

Equations

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

def TriangleInflation.Graph.triPermEquiv (t : ℕ) : (triangleGraph.Edge → Equiv.Perm (Fin t)) ≃ Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)

The three copy-index permutation families of the triangle.

Equations

• TriangleInflation.Graph.triPermEquiv t = TriangleInflation.Graph.triPiEdgeEquiv fun (x : TriangleInflation.Graph.triangleGraph.Edge) => Equiv.Perm (Fin t)

theorem TriangleInflation.Graph.triObs_gPerm {t : ℕ} (π : triangleGraph.Edge → Equiv.Perm (Fin t)) (o : GObs triangleGraph t) : triObs (gPerm π o) = Obs.perm ((triPermEquiv t) π) (triObs o)

theorem TriangleInflation.Graph.tri_partyBit {t : ℕ} (o : GObs triangleGraph t) (w : ThreeBit) : partyBit (triObs o).party w = threeBitEquiv.symm w o.fst

Transport of witnesses

def TriangleInflation.Graph.triAssignEquiv (t : ℕ) : GAssign triangleGraph t ≃ Assign t

The induced bijection of assignments.

Equations

• TriangleInflation.Graph.triAssignEquiv t = (TriangleInflation.Graph.triEquiv t).arrowCongr (Equiv.refl Bool)

theorem TriangleInflation.Graph.tri_assign_symm_apply {t : ℕ} (ω : Assign t) (o : GObs triangleGraph t) : (triAssignEquiv t).symm ω o = ω (triObs o)

theorem TriangleInflation.Graph.tri_assign_apply {t : ℕ} (ω : GAssign triangleGraph t) (v : Obs t) : (triAssignEquiv t) ω v = ω ((triEquiv t).symm v)

theorem TriangleInflation.Graph.tri_pushforward_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Fintype α] [Fintype β] [DecidableEq γ] [DecidableEq δ] (eab : α ≃ β) (ecd : γ ≃ δ) (w : α → ℝ) (F : α → γ) (F' : β → δ) (h : ∀ (a : α), F' (eab a) = ecd (F a)) : pushforward (fun (b : β) => w (eab.symm b)) F' = fun (d : δ) => pushforward w F (ecd.symm d)

theorem TriangleInflation.Graph.tri_sum_transport {t : ℕ} (Δ : GAssign triangleGraph t → ℝ) : ∑ ω : Assign t, Δ ((triAssignEquiv t).symm ω) = ∑ ω : GAssign triangleGraph t, Δ ω

theorem TriangleInflation.Graph.tri_isLaw_transport {t : ℕ} (Δ : GAssign triangleGraph t → ℝ) : (IsLaw fun (ω : Assign t) => Δ ((triAssignEquiv t).symm ω)) ↔ IsLaw Δ

theorem TriangleInflation.Graph.tri_assign_symm_relabel {t : ℕ} (π : triangleGraph.Edge → Equiv.Perm (Fin t)) (ω : Assign t) : (triAssignEquiv t).symm (relabel ((triPermEquiv t) π) ω) = gRelabel π ((triAssignEquiv t).symm ω)

theorem TriangleInflation.Graph.tri_sym_transport {t : ℕ} (Δ : GAssign triangleGraph t → ℝ) : (SymmetricLaw t fun (ω : Assign t) => Δ ((triAssignEquiv t).symm ω)) ↔ GSymmetric t Δ

def TriangleInflation.Graph.triDiagEquiv (t : ℕ) : (Fin t → triangleGraph.V → Bool) ≃ (Fin t → ThreeBit)

The bijection of diagonal reads.

Equations

• TriangleInflation.Graph.triDiagEquiv t = (Equiv.refl (Fin t)).arrowCongr TriangleInflation.Graph.threeBitEquiv

theorem TriangleInflation.Graph.tri_symm_diag_A {t : ℕ} (r : Fin t) : (triEquiv t).symm (Obs.A r r) = copyObs (fun (x : triangleGraph.Edge) => r) 0

theorem TriangleInflation.Graph.tri_symm_diag_B {t : ℕ} (r : Fin t) : (triEquiv t).symm (Obs.B r r) = copyObs (fun (x : triangleGraph.Edge) => r) 1

theorem TriangleInflation.Graph.tri_symm_diag_C {t : ℕ} (r : Fin t) : (triEquiv t).symm (Obs.C r r) = copyObs (fun (x : triangleGraph.Edge) => r) 2

theorem TriangleInflation.Graph.tri_readDiagonal_map {t : ℕ} (ω : GAssign triangleGraph t) : readDiagonal ((triAssignEquiv t) ω) = (triDiagEquiv t) (readDiag ω)

theorem TriangleInflation.Graph.tri_diag_transport {t : ℕ} (Δ : GAssign triangleGraph t → ℝ) (P : ThreeBit → ℝ) : pushforward (fun (ω : Assign t) => Δ ((triAssignEquiv t).symm ω)) readDiagonal = tensorPow t P ↔ pushforward Δ readDiag = gTensorPow t fun (w : triangleGraph.V → Bool) => P (threeBitEquiv w)

Sets of copied observations

def TriangleInflation.Graph.triFinsetEquiv (t : ℕ) : Finset (GObs triangleGraph t) ≃ Finset (Obs t)

Transport finite observation sets to the named triangle representation.

Equations

• TriangleInflation.Graph.triFinsetEquiv t = (TriangleInflation.Graph.triEquiv t).finsetCongr

def TriangleInflation.Graph.triSubEquiv {t : ℕ} (S : Finset (GObs triangleGraph t)) : ↥S ≃ ↥((triFinsetEquiv t) S)

Identify observations in a finite graph set with their triangle counterparts.

Equations

• TriangleInflation.Graph.triSubEquiv S = (TriangleInflation.Graph.triEquiv t).subtypeEquiv ⋯

def TriangleInflation.Graph.triBoolEquiv {t : ℕ} (S : Finset (GObs triangleGraph t)) : (↥S → Bool) ≃ (↥((triFinsetEquiv t) S) → Bool)

Transport Boolean assignments on a finite observation set.

Equations

• TriangleInflation.Graph.triBoolEquiv S = (TriangleInflation.Graph.triSubEquiv S).arrowCongr (Equiv.refl Bool)

theorem TriangleInflation.Graph.tri_restrictAssign_map {t : ℕ} (S : Finset (GObs triangleGraph t)) (ω : GAssign triangleGraph t) : restrictAssign ((triFinsetEquiv t) S) ((triAssignEquiv t) ω) = (triBoolEquiv S) (gRestrict S ω)

theorem TriangleInflation.Graph.tri_partyRead_map {t : ℕ} (S : Finset (GObs triangleGraph t)) (w : Fin 3 → Bool) : partyRead ((triFinsetEquiv t) S) (threeBitEquiv w) = (triBoolEquiv S) (gPartyRead S w)

theorem TriangleInflation.Graph.tri_copySet_map {t : ℕ} (ι : triangleGraph.Edge → Fin t) : (triFinsetEquiv t) (copySet ι) = copiedTriangle (ι triEdgeX) (ι triEdgeZ) (ι triEdgeY)

theorem TriangleInflation.Graph.tri_gInjectable_map {t : ℕ} (S : Finset (GObs triangleGraph t)) : Injectable ((triFinsetEquiv t) S) ↔ GInjectable S

Copied latent sources

def TriangleInflation.Graph.triLatentEquiv (t : ℕ) : GLatent triangleGraph t ≃ Latent t

Identify copied graph sources with named triangle latent sources.

Equations

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

theorem TriangleInflation.Graph.tri_gAncestors_map {t : ℕ} (o : GObs triangleGraph t) : Finset.map (triLatentEquiv t).toEmbedding (gAncestors o) = (triObs o).ancestors

theorem TriangleInflation.Graph.tri_mem_ancestorsOf_map {t : ℕ} (S : Finset (GObs triangleGraph t)) (a : Latent t) : a ∈ ancestorsOf ((triFinsetEquiv t) S) ↔ (triLatentEquiv t).symm a ∈ gAncestorsOf S

theorem TriangleInflation.Graph.tri_gAI_map {t : ℕ} (S T : Finset (GObs triangleGraph t)) : AncestrallyIndependent ((triFinsetEquiv t) S) ((triFinsetEquiv t) T) ↔ GAncestrallyIndependent S T

Transport of the injectable and ancestral prescriptions

theorem TriangleInflation.Graph.tri_restrict_pushforward {t : ℕ} (S : Finset (GObs triangleGraph t)) (Δ : GAssign triangleGraph t → ℝ) : pushforward (fun (ω : Assign t) => Δ ((triAssignEquiv t).symm ω)) (restrictAssign ((triFinsetEquiv t) S)) = fun (d : ↥((triFinsetEquiv t) S) → Bool) => pushforward Δ (gRestrict S) ((triBoolEquiv S).symm d)

theorem TriangleInflation.Graph.tri_partyRead_pushforward {t : ℕ} (S : Finset (GObs triangleGraph t)) (P : ThreeBit → ℝ) : pushforward P (partyRead ((triFinsetEquiv t) S)) = fun (d : ↥((triFinsetEquiv t) S) → Bool) => pushforward (fun (w : Fin 3 → Bool) => P (threeBitEquiv w)) (gPartyRead S) ((triBoolEquiv S).symm d)

theorem TriangleInflation.Graph.tri_injMarg_transport {t : ℕ} (Δ : GAssign triangleGraph t → ℝ) (P : ThreeBit → ℝ) : InjectableMarginals t (fun (ω : Assign t) => Δ ((triAssignEquiv t).symm ω)) P ↔ GInjectableMarginals t Δ fun (w : triangleGraph.V → Bool) => P (threeBitEquiv w)

def TriangleInflation.Graph.triPiEquiv {t n : ℕ} (S : Fin n → Finset (GObs triangleGraph t)) : ((m : Fin n) → ↥(S m) → Bool) ≃ ((m : Fin n) → ↥((triFinsetEquiv t) (S m)) → Bool)

Transport families of Boolean assignments on finite observation sets.

Equations

• TriangleInflation.Graph.triPiEquiv S = Equiv.piCongrRight fun (m : Fin n) => TriangleInflation.Graph.triBoolEquiv (S m)

theorem TriangleInflation.Graph.tri_ancProd_transport {t : ℕ} (Δ : GAssign triangleGraph t → ℝ) (P : ThreeBit → ℝ) : AncestralProducts t (fun (ω : Assign t) => Δ ((triAssignEquiv t).symm ω)) P ↔ GAncestralProducts t Δ fun (w : triangleGraph.V → Bool) => P (threeBitEquiv w)

theorem TriangleInflation.Graph.triInc0_ne (e : ↥(triangleGraph.inc 0)) : ¬e = triInc0X → e = triInc0Z

theorem TriangleInflation.Graph.triInc1_ne (e : ↥(triangleGraph.inc 1)) : ¬e = triInc1X → e = triInc1Y

theorem TriangleInflation.Graph.triInc2_ne (e : ↥(triangleGraph.inc 2)) : ¬e = triInc2Z → e = triInc2Y

def TriangleInflation.Graph.triInc0Equiv (L : triangleGraph.Edge → Type u) : ((e : ↥(triangleGraph.inc 0)) → L ↑e) ≃ L triEdgeX × L triEdgeZ

Identify the latent inputs at vertex 0 with its two named sources.

Equations

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

def TriangleInflation.Graph.triInc1Equiv (L : triangleGraph.Edge → Type u) : ((e : ↥(triangleGraph.inc 1)) → L ↑e) ≃ L triEdgeX × L triEdgeY

Identify the latent inputs at vertex 1 with its two named sources.

Equations

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

def TriangleInflation.Graph.triInc2Equiv (L : triangleGraph.Edge → Type u) : ((e : ↥(triangleGraph.inc 2)) → L ↑e) ≃ L triEdgeZ × L triEdgeY

Identify the latent inputs at vertex 2 with its two named sources.

Equations

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

theorem TriangleInflation.Graph.tri_prod_edge {M : Type u_1} [CommMonoid M] (F : triangleGraph.Edge → M) : ∏ e : triangleGraph.Edge, F e = F triEdgeX * F triEdgeZ * F triEdgeY

theorem TriangleInflation.Graph.tri_sum_edgePi {M : Type u_1} [AddCommMonoid M] (L : triangleGraph.Edge → Type) [(e : triangleGraph.Edge) → Fintype (L e)] (F : ((e : triangleGraph.Edge) → L e) → M) : ∑ x : (e : triangleGraph.Edge) → L e, F x = ∑ a : L triEdgeX, ∑ b : L triEdgeZ, ∑ c : L triEdgeY, F ((triPiEdgeEquiv L).symm (a, b, c))

@[simp]

theorem TriangleInflation.Graph.triPiEdge_symm_X (L : triangleGraph.Edge → Type u) (p : L triEdgeX × L triEdgeZ × L triEdgeY) : (triPiEdgeEquiv L).symm p triEdgeX = p.1

@[simp]

theorem TriangleInflation.Graph.triPiEdge_symm_Z (L : triangleGraph.Edge → Type u) (p : L triEdgeX × L triEdgeZ × L triEdgeY) : (triPiEdgeEquiv L).symm p triEdgeZ = p.2.1

@[simp]

theorem TriangleInflation.Graph.triPiEdge_symm_Y (L : triangleGraph.Edge → Type u) (p : L triEdgeX × L triEdgeZ × L triEdgeY) : (triPiEdgeEquiv L).symm p triEdgeY = p.2.2

@[simp]

theorem TriangleInflation.Graph.triInc0_symm_X (L : triangleGraph.Edge → Type u) (p : L triEdgeX × L triEdgeZ) : (triInc0Equiv L).symm p triInc0X = p.1

@[simp]

theorem TriangleInflation.Graph.triInc0_symm_Z (L : triangleGraph.Edge → Type u) (p : L triEdgeX × L triEdgeZ) : (triInc0Equiv L).symm p triInc0Z = p.2

@[simp]

theorem TriangleInflation.Graph.triInc1_symm_X (L : triangleGraph.Edge → Type u) (p : L triEdgeX × L triEdgeY) : (triInc1Equiv L).symm p triInc1X = p.1

@[simp]

theorem TriangleInflation.Graph.triInc1_symm_Y (L : triangleGraph.Edge → Type u) (p : L triEdgeX × L triEdgeY) : (triInc1Equiv L).symm p triInc1Y = p.2

@[simp]

theorem TriangleInflation.Graph.triInc2_symm_Z (L : triangleGraph.Edge → Type u) (p : L triEdgeZ × L triEdgeY) : (triInc2Equiv L).symm p triInc2Z = p.1

@[simp]

theorem TriangleInflation.Graph.triInc2_symm_Y (L : triangleGraph.Edge → Type u) (p : L triEdgeZ × L triEdgeY) : (triInc2Equiv L).symm p triInc2Y = p.2

theorem TriangleInflation.Graph.tri_tb0 (w : Fin 3 → Bool) : (threeBitEquiv w).1 = w 0

theorem TriangleInflation.Graph.tri_tb1 (w : Fin 3 → Bool) : (threeBitEquiv w).2.1 = w 1

theorem TriangleInflation.Graph.tri_tb2 (w : Fin 3 → Bool) : (threeBitEquiv w).2.2 = w 2

theorem TriangleInflation.Graph.tri_restrict_inc0 (L : triangleGraph.Edge → Type u) (x : (e : triangleGraph.Edge) → L e) : (fun (e : ↥(triangleGraph.inc 0)) => x ↑e) = (triInc0Equiv L).symm (x triEdgeX, x triEdgeZ)

theorem TriangleInflation.Graph.tri_restrict_inc1 (L : triangleGraph.Edge → Type u) (x : (e : triangleGraph.Edge) → L e) : (fun (e : ↥(triangleGraph.inc 1)) => x ↑e) = (triInc1Equiv L).symm (x triEdgeX, x triEdgeY)

theorem TriangleInflation.Graph.tri_restrict_inc2 (L : triangleGraph.Edge → Type u) (x : (e : triangleGraph.Edge) → L e) : (fun (e : ↥(triangleGraph.inc 2)) => x ↑e) = (triInc2Equiv L).symm (x triEdgeZ, x triEdgeY)

theorem TriangleInflation.Graph.tri_prod_vertex {M : Type u_1} [CommMonoid M] (F : triangleGraph.V → M) : ∏ v : triangleGraph.V, F v = F 0 * F 1 * F 2

theorem TriangleInflation.Graph.tri_gmodel_law_eq (M : GModel triangleGraph) (w : Fin 3 → Bool) : M.law w = ∑ a : M.L triEdgeX, ∑ b : M.L triEdgeZ, ∑ c : M.L triEdgeY, M.μ triEdgeX a * M.μ triEdgeZ b * M.μ triEdgeY c * respMass (M.resp 0 ((triInc0Equiv M.L).symm (a, b))) (w 0) * respMass (M.resp 1 ((triInc1Equiv M.L).symm (a, c))) (w 1) * respMass (M.resp 2 ((triInc2Equiv M.L).symm (b, c))) (w 2)

The observed law of a triangle GModel, as a triple sum.

theorem TriangleInflation.Graph.tri_tbs0 (w : ThreeBit) : threeBitEquiv.symm w 0 = w.1

theorem TriangleInflation.Graph.tri_tbs1 (w : ThreeBit) : threeBitEquiv.symm w 1 = w.2.1

theorem TriangleInflation.Graph.tri_tbs2 (w : ThreeBit) : threeBitEquiv.symm w 2 = w.2.2

def TriangleInflation.Graph.triToModel (M : GModel triangleGraph) : TriangleModel

The triangle model of a triangle GModel.

Equations

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

def TriangleInflation.Graph.triL (A B C : Type) : triangleGraph.Edge → Type

The latent alphabets of the triangle GModel of a triangle model.

Equations

• TriangleInflation.Graph.triL A B C e = if e = TriangleInflation.Graph.triEdgeX then A else if e = TriangleInflation.Graph.triEdgeZ then B else C

def TriangleInflation.Graph.triOfModel (N : TriangleModel) : GModel triangleGraph

The triangle GModel of a triangle model.

Equations

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

theorem TriangleInflation.Graph.triToModel_law (M : GModel triangleGraph) (w : ThreeBit) : (triToModel M).law w = M.law (threeBitEquiv.symm w)

theorem TriangleInflation.Graph.triOfModel_law (N : TriangleModel) (w : Fin 3 → Bool) : (triOfModel N).law w = N.law (threeBitEquiv w)

theorem TriangleInflation.Graph.exists_triObsEquiv (t : ℕ) : ∃ (e : GObs triangleGraph t ≃ Obs t) (σ : (triangleGraph.Edge → Equiv.Perm (Fin t)) ≃ Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)), (∀ (o : GObs triangleGraph t) (w : ThreeBit), partyBit (e o).party w = threeBitEquiv.symm w o.fst) ∧ ∀ (π : triangleGraph.Edge → Equiv.Perm (Fin t)) (o : GObs triangleGraph t), e (gPerm π o) = Obs.perm (σ π) (e o)

AUDIT-NOTES A1/A2. The copied observations of the order-t inflation of C₃ are in bijection with TriangleInflation.Obs t, by a bijection that intertwines the per-source copy-index actions and matches the vertex of a copied observation with the party of its image.

theorem TriangleInflation.Graph.gNWFeasible_triangle_iff (t : ℕ) (P : ThreeBit → ℝ) : (GNWFeasible triangleGraph t fun (w : triangleGraph.V → Bool) => P (threeBitEquiv w)) ↔ NWFeasible t P

The pair-source Navascués–Wolfe test on C₃ is the triangle test of TriangleInflation, under the re-encoding threeBitEquiv of three-bit outcomes as functions on Fin 3.

theorem TriangleInflation.Graph.gAIFeasible_triangle_iff (t : ℕ) (P : ThreeBit → ℝ) : (GAIFeasible triangleGraph t fun (w : triangleGraph.V → Bool) => P (threeBitEquiv w)) ↔ AIFeasible t P

The pair-source AI test on C₃ is the triangle AI test.

theorem TriangleInflation.Graph.gCompatible_triangle_iff (P : ThreeBit → ℝ) : (GCompatible triangleGraph fun (w : triangleGraph.V → Bool) => P (threeBitEquiv w)) ↔ TriangleCompatible P

The pair-source compatible set of C₃ is TriangleInflation.TriangleCompatible, both with finite latent alphabets (AUDIT-NOTES D1).