Inflation for the classical triangle: definitions

Definitions for the manuscript Inflation for the Classical Triangle: Nontermination and Quantitative Complexity (papers/inflation-nontermination). This file carries definitions only; the statements live in Finner.lean, Defect.lean, Main.lean, Fan.lean, Exponent.lean and Rate.lean.

Representational decisions

• Laws are bare real weight functions. A law on a Fintype α is a function α → ℝ together with the predicate IsLaw (nonnegative, sums to 1). The unbundled form is used here because the paper's families Q(ε,r), P_ε, R_p are written for parameter ranges in which normalization is a hypothesis of the statement rather than part of the datum, and because the feasibility definitions quantify over witnesses on large index types where carrying proof fields through every statement is noise. No Mathlib Measure or PMF is used; all inequalities are real-valued.

• Latent alphabets are finite. TriangleCompatible quantifies over a TriangleModel, whose three latent spaces are arbitrary Fintypes. The paper (Section 2) allows arbitrary measurable latent spaces. Restricting to finite latent alphabets is a formalization boundary; it is justified by the theorem of Rosset, Gisin and Wolfe (2018) that latent alphabets of bounded finite size suffice for the triangle. That theorem is not formalized here. Consequently TriangleCompatible is a subset of the paper's C_tri, and a theorem ¬ TriangleCompatible P is the WEAKER statement: nonmembership in the finite-latent set does not by itself give nonmembership in the arbitrary-latent set. The arbitrary-latent statement needs either the Rosset–Gisin–Wolfe reduction (quoted, not formalized) or a direct measure-theoretic proof of Lemma 5.7; see FinnerMeasure.lean for the latter where it exists.

• The recursively expressible set is not formalized. Definition 2.3 of the paper (Definition 2.5, def:gexp, the I^exp_t hierarchy) needs d-separation in the inflated causal graph and the recursion of Wolfe–Spekkens–Fritz Definition 7. That machinery is deliberately out of scope here, so the membership Q(ε,r) ∈ I^exp_t of Theorem 5.1 (Lemma 5.10, lem:expressible) is an unformalized boundary. Only the two weaker hierarchies I^NW_t (NWFeasible) and I^AI_t (AIFeasible) are defined, and every statement that the paper phrases for all three hierarchies is formalized for those two. Since I^exp_t ⊆ I^AI_t ⊆ I^NW_t, the membership theorems formalized here are the weaker halves of the paper's claims and the rejection theorems are the stronger halves.

• Bit convention. Outcomes are Bool; false is the paper's 0 and true is its 1. So Bern(r) has Bern(r)(true) = r, matching Bern(r)(1) = r.

• Truncated subtraction. Exponents t - 1 are ℕ subtraction; every statement using them carries the hypothesis 1 ≤ t, where the two agree.

Laws as weight functions

def TriangleInflation.IsLaw {α : Type u_1} [Fintype α] (w : α → ℝ) : Prop

A probability weight function on a finite type: nonnegative and summing to one.

Equations

• TriangleInflation.IsLaw w = ((∀ (a : α), 0 ≤ w a) ∧ ∑ a : α, w a = 1)

def TriangleInflation.pushforward {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (w : α → ℝ) (F : α → β) : β → ℝ

Pushforward of a weight function along a map of finite types.

Equations

• TriangleInflation.pushforward w F b = ∑ a : α, if F a = b then w a else 0

def TriangleInflation.prodLaw {ι : Type u_1} [Fintype ι] (w : ι → Bool → ℝ) : (ι → Bool) → ℝ

The product of independent per-coordinate weight functions on ι → Bool.

Equations

• TriangleInflation.prodLaw w x = ∏ i : ι, w i (x i)

Three-bit laws

@[reducible, inline]

abbrev TriangleInflation.ThreeBit : Type

The outcome type of the triangle: the three observed bits (A, B, C). false is the paper's outcome 0.

Equations

• TriangleInflation.ThreeBit = (Bool × Bool × Bool)

inductive TriangleInflation.Party : Type

The three observed parties of the triangle.

• A : Party
• B : Party
• C : Party

@[instance_reducible]

instance TriangleInflation.instDecidableEqParty : DecidableEq Party

Equations

• TriangleInflation.instDecidableEqParty x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TriangleInflation.instReprParty.repr : Party → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance TriangleInflation.instReprParty : Repr Party

Equations

• TriangleInflation.instReprParty = { reprPrec := TriangleInflation.instReprParty.repr }

def TriangleInflation.partyBit : Party → ThreeBit → Bool

The bit that a party reads off a three-bit outcome.

Equations

• TriangleInflation.partyBit TriangleInflation.Party.A x✝ = x✝.1
• TriangleInflation.partyBit TriangleInflation.Party.B x✝ = x✝.2.1
• TriangleInflation.partyBit TriangleInflation.Party.C x✝ = x✝.2.2

def TriangleInflation.atom000 (P : ThreeBit → ℝ) : ℝ

P(000): the all-zero atom.

Equations

• TriangleInflation.atom000 P = P (false, false, false)

def TriangleInflation.margA (P : ThreeBit → ℝ) : ℝ

P_A(0): the zero marginal of the first bit.

Equations

• TriangleInflation.margA P = ∑ y : Bool, ∑ z : Bool, P (false, y, z)

def TriangleInflation.margB (P : ThreeBit → ℝ) : ℝ

P_B(0): the zero marginal of the second bit.

Equations

• TriangleInflation.margB P = ∑ x : Bool, ∑ z : Bool, P (x, false, z)

def TriangleInflation.margC (P : ThreeBit → ℝ) : ℝ

P_C(0): the zero marginal of the third bit.

Equations

• TriangleInflation.margC P = ∑ x : Bool, ∑ y : Bool, P (x, y, false)

def TriangleInflation.tensorPow (t : ℕ) (P : ThreeBit → ℝ) : (Fin t → ThreeBit) → ℝ

The t-fold tensor power P^{⊗t}, as a law on Fin t → ThreeBit.

Equations

• TriangleInflation.tensorPow t P v = ∏ l : Fin t, P (v l)

The copied observations of the order-t inflation

Paper Section 2.3. A^{ij} has X-index i and Z-index j; B^{ik} has X-index i and Y-index k; C^{jk} has Z-index j and Y-index k.

inductive TriangleInflation.Obs (t : ℕ) : Type

The 3t² copied observations of the order-t inflation.

• A {t : ℕ} (i j : Fin t) : Obs t
• B {t : ℕ} (i k : Fin t) : Obs t
• C {t : ℕ} (j k : Fin t) : Obs t

def TriangleInflation.instDecidableEqObs.decEq {t✝ : ℕ} (x✝ x✝¹ : Obs t✝) : Decidable (x✝ = x✝¹)

Equations

• TriangleInflation.instDecidableEqObs.decEq (TriangleInflation.Obs.A a a_1) (TriangleInflation.Obs.A b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• TriangleInflation.instDecidableEqObs.decEq (TriangleInflation.Obs.A i j) (TriangleInflation.Obs.B i_1 k) = isFalse ⋯
• TriangleInflation.instDecidableEqObs.decEq (TriangleInflation.Obs.A i j) (TriangleInflation.Obs.C j_1 k) = isFalse ⋯
• TriangleInflation.instDecidableEqObs.decEq (TriangleInflation.Obs.B i k) (TriangleInflation.Obs.A i_1 j) = isFalse ⋯
• TriangleInflation.instDecidableEqObs.decEq (TriangleInflation.Obs.B a a_1) (TriangleInflation.Obs.B b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• TriangleInflation.instDecidableEqObs.decEq (TriangleInflation.Obs.B i k) (TriangleInflation.Obs.C j k_1) = isFalse ⋯
• TriangleInflation.instDecidableEqObs.decEq (TriangleInflation.Obs.C j k) (TriangleInflation.Obs.A i j_1) = isFalse ⋯
• TriangleInflation.instDecidableEqObs.decEq (TriangleInflation.Obs.C j k) (TriangleInflation.Obs.B i k_1) = isFalse ⋯
• TriangleInflation.instDecidableEqObs.decEq (TriangleInflation.Obs.C a a_1) (TriangleInflation.Obs.C b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance TriangleInflation.instDecidableEqObs {t✝ : ℕ} : DecidableEq (Obs t✝)

Equations

• TriangleInflation.instDecidableEqObs = TriangleInflation.instDecidableEqObs.decEq

@[instance_reducible]

instance TriangleInflation.instFintypeObs {t✝ : ℕ} : Fintype (Obs t✝)

Equations

• TriangleInflation.instFintypeObs = Fintype.ofEquiv ((_ : Fin t✝) × Fin t✝ ⊕ (_ : Fin t✝) × Fin t✝ ⊕ (_ : Fin t✝) × Fin t✝) (TriangleInflation.Obs.proxyTypeEquiv t✝)

@[reducible, inline]

abbrev TriangleInflation.Assign (t : ℕ) : Type

A deterministic assignment of the copied observations, an element of {0,1}^{3t²}.

Equations

• TriangleInflation.Assign t = (TriangleInflation.Obs t → Bool)

def TriangleInflation.Obs.party {t : ℕ} : Obs t → Party

Which party a copied observation is a copy of.

Equations

• (TriangleInflation.Obs.A a a_1).party = TriangleInflation.Party.A
• (TriangleInflation.Obs.B a a_1).party = TriangleInflation.Party.B
• (TriangleInflation.Obs.C a a_1).party = TriangleInflation.Party.C

inductive TriangleInflation.Latent (t : ℕ) : Type

The copied latent variables of the order-t inflation: X_i, Z_j, Y_k.

• X {t : ℕ} (i : Fin t) : Latent t
• Z {t : ℕ} (j : Fin t) : Latent t
• Y {t : ℕ} (k : Fin t) : Latent t

@[instance_reducible]

instance TriangleInflation.instDecidableEqLatent {t✝ : ℕ} : DecidableEq (Latent t✝)

Equations

• TriangleInflation.instDecidableEqLatent = TriangleInflation.instDecidableEqLatent.decEq

def TriangleInflation.instDecidableEqLatent.decEq {t✝ : ℕ} (x✝ x✝¹ : Latent t✝) : Decidable (x✝ = x✝¹)

Equations

• TriangleInflation.instDecidableEqLatent.decEq (TriangleInflation.Latent.X a) (TriangleInflation.Latent.X b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TriangleInflation.instDecidableEqLatent.decEq (TriangleInflation.Latent.X i) (TriangleInflation.Latent.Z j) = isFalse ⋯
• TriangleInflation.instDecidableEqLatent.decEq (TriangleInflation.Latent.X i) (TriangleInflation.Latent.Y k) = isFalse ⋯
• TriangleInflation.instDecidableEqLatent.decEq (TriangleInflation.Latent.Z j) (TriangleInflation.Latent.X i) = isFalse ⋯
• TriangleInflation.instDecidableEqLatent.decEq (TriangleInflation.Latent.Z a) (TriangleInflation.Latent.Z b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TriangleInflation.instDecidableEqLatent.decEq (TriangleInflation.Latent.Z j) (TriangleInflation.Latent.Y k) = isFalse ⋯
• TriangleInflation.instDecidableEqLatent.decEq (TriangleInflation.Latent.Y k) (TriangleInflation.Latent.X i) = isFalse ⋯
• TriangleInflation.instDecidableEqLatent.decEq (TriangleInflation.Latent.Y k) (TriangleInflation.Latent.Z j) = isFalse ⋯
• TriangleInflation.instDecidableEqLatent.decEq (TriangleInflation.Latent.Y a) (TriangleInflation.Latent.Y b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TriangleInflation.instFintypeLatent {t✝ : ℕ} : Fintype (Latent t✝)

Equations

• TriangleInflation.instFintypeLatent = Fintype.ofEquiv (Fin t✝ ⊕ Fin t✝ ⊕ Fin t✝) (TriangleInflation.Latent.proxyTypeEquiv t✝)

def TriangleInflation.Obs.ancestors {t : ℕ} : Obs t → Finset (Latent t)

The copied latent ancestors of a copied observation: A^{ij} ↦ {X_i, Z_j}, B^{ik} ↦ {X_i, Y_k}, C^{jk} ↦ {Z_j, Y_k}.

Equations

• (TriangleInflation.Obs.A a a_1).ancestors = {TriangleInflation.Latent.X a, TriangleInflation.Latent.Z a_1}
• (TriangleInflation.Obs.B a a_1).ancestors = {TriangleInflation.Latent.X a, TriangleInflation.Latent.Y a_1}
• (TriangleInflation.Obs.C a a_1).ancestors = {TriangleInflation.Latent.Z a, TriangleInflation.Latent.Y a_1}

def TriangleInflation.ancestorsOf {t : ℕ} (S : Finset (Obs t)) : Finset (Latent t)

The copied latent ancestors of a set of copied observations.

Equations

• TriangleInflation.ancestorsOf S = S.biUnion TriangleInflation.Obs.ancestors

def TriangleInflation.AncestrallyIndependent {t : ℕ} (S T : Finset (Obs t)) : Prop

Paper Definition 2.4: two sets of copied observations are ancestrally independent when their copied latent ancestors are disjoint.

Equations

• TriangleInflation.AncestrallyIndependent S T = Disjoint (TriangleInflation.ancestorsOf S) (TriangleInflation.ancestorsOf T)

def TriangleInflation.copiedTriangle {t : ℕ} (i j k : Fin t) : Finset (Obs t)

The copied triangle Δ_{ijk} = {A^{ij}, B^{ik}, C^{jk}} (paper Section 2.3).

Equations

• TriangleInflation.copiedTriangle i j k = {TriangleInflation.Obs.A i j, TriangleInflation.Obs.B i k, TriangleInflation.Obs.C j k}

def TriangleInflation.diagonalTriangle {t : ℕ} (l : Fin t) : Finset (Obs t)

The diagonal triangle Δ_{lll} (paper Section 2.3).

Equations

• TriangleInflation.diagonalTriangle l = TriangleInflation.copiedTriangle l l l

def TriangleInflation.readTriangle {t : ℕ} (i j k : Fin t) (ω : Assign t) : ThreeBit

The three-bit outcome that an assignment gives to the copied triangle Δ_{ijk}.

Equations

• TriangleInflation.readTriangle i j k ω = (ω (TriangleInflation.Obs.A i j), ω (TriangleInflation.Obs.B i k), ω (TriangleInflation.Obs.C j k))

def TriangleInflation.readDiagonal {t : ℕ} (ω : Assign t) : Fin t → ThreeBit

The tuple of three-bit outcomes of the t diagonal triangles (Δ_{lll})_{l ∈ [t]}.

Equations

• TriangleInflation.readDiagonal ω l = TriangleInflation.readTriangle l l l ω

The symmetry group

def TriangleInflation.Obs.perm {t : ℕ} (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) : Obs t → Obs t

The action of (σ_X, σ_Z, σ_Y) ∈ S_t × S_t × S_t on copied observations. The first component permutes X-copy indices, the second Z-copy indices, the third Y-copy indices, exactly as in Definition 2.3(i).

Equations

• TriangleInflation.Obs.perm π (TriangleInflation.Obs.A a a_1) = TriangleInflation.Obs.A (π.1 a) (π.2.1 a_1)
• TriangleInflation.Obs.perm π (TriangleInflation.Obs.B a a_1) = TriangleInflation.Obs.B (π.1 a) (π.2.2 a_1)
• TriangleInflation.Obs.perm π (TriangleInflation.Obs.C a a_1) = TriangleInflation.Obs.C (π.2.1 a) (π.2.2 a_1)

def TriangleInflation.relabel {t : ℕ} (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) (ω : Assign t) : Assign t

Relabelling an assignment by an index permutation.

Equations

• TriangleInflation.relabel π ω v = ω (TriangleInflation.Obs.perm π v)

def TriangleInflation.SymmetricLaw (t : ℕ) (Γ : Assign t → ℝ) : Prop

Paper Definition 2.3(i): invariance under independent permutations of the three index families.

Equations

• TriangleInflation.SymmetricLaw t Γ = ∀ (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) (ω : TriangleInflation.Assign t), Γ (TriangleInflation.relabel π ω) = Γ ω

Injectable sets

Paper Definition 2.4 and Appendix A.

def TriangleInflation.SharedAgree {t : ℕ} : Obs t → Obs t → Prop

The primitive condition of Wolfe–Spekkens–Fritz Definition 4, specialized to the triangle: erasing copy indices is injective on the set, and any two members that are copies of variables sharing a source in the triangle agree in the copy index of that source.

Equations

• TriangleInflation.SharedAgree (TriangleInflation.Obs.A i j) (TriangleInflation.Obs.B i' k) = (i = i')
• TriangleInflation.SharedAgree (TriangleInflation.Obs.B i' k) (TriangleInflation.Obs.A i j) = (i = i')
• TriangleInflation.SharedAgree (TriangleInflation.Obs.A i j) (TriangleInflation.Obs.C j' k) = (j = j')
• TriangleInflation.SharedAgree (TriangleInflation.Obs.C j' k) (TriangleInflation.Obs.A i j) = (j = j')
• TriangleInflation.SharedAgree (TriangleInflation.Obs.B i k) (TriangleInflation.Obs.C j k') = (k = k')
• TriangleInflation.SharedAgree (TriangleInflation.Obs.C j k') (TriangleInflation.Obs.B i k) = (k = k')
• TriangleInflation.SharedAgree x✝¹ x✝ = True

def TriangleInflation.InjectableRaw {t : ℕ} (S : Finset (Obs t)) : Prop

The primitive definition of an injectable set (paper Appendix A.3).

Equations

• TriangleInflation.InjectableRaw S = ((∀ u ∈ S, ∀ v ∈ S, u.party = v.party → u = v) ∧ ∀ u ∈ S, ∀ v ∈ S, TriangleInflation.SharedAgree u v)

def TriangleInflation.Injectable {t : ℕ} (S : Finset (Obs t)) : Prop

Paper Definition 2.4 together with Appendix A: for the triangle the injectable sets are exactly the subsets of copied triangles. This characterization is the working definition here; Main.injectable_iff_injectableRaw records its equivalence with InjectableRaw.

Equations

• TriangleInflation.Injectable S = ∃ (i : Fin t) (j : Fin t) (k : Fin t), S ⊆ TriangleInflation.copiedTriangle i j k

def TriangleInflation.restrictAssign {t : ℕ} (S : Finset (Obs t)) (ω : Assign t) : ↥S → Bool

The restriction of an assignment to a set of copied observations.

Equations

• TriangleInflation.restrictAssign S ω v = ω ↑v

def TriangleInflation.partyRead {t : ℕ} (S : Finset (Obs t)) (w : ThreeBit) : ↥S → Bool

The outcome pattern that a three-bit law prescribes on an injectable set: each member reads the bit of the party it is a copy of.

Equations

• TriangleInflation.partyRead S w v = TriangleInflation.partyBit (↑v).party w

The defect cube (paper Section 5.1)

Cell t indexes the cube [t]³ of defect bits D_{ijk}; Obs t indexes the private bits N_v. The root bits are indexed by Root t = Cell t ⊕ Obs t.

@[reducible, inline]

abbrev TriangleInflation.Cell (t : ℕ) : Type

The cells (i,j,k) ∈ [t]³ of the defect cube.

Equations

• TriangleInflation.Cell t = (Fin t × Fin t × Fin t)

@[reducible, inline]

abbrev TriangleInflation.Root (t : ℕ) : Type

The root bits of the defect cube: defects on cells, private bits on observations.

Equations

• TriangleInflation.Root t = (TriangleInflation.Cell t ⊕ TriangleInflation.Obs t)

def TriangleInflation.onLine {t : ℕ} : Obs t → Cell t → Bool

onLine v c says the cell c lies on the line Λ(v) read by the observation v: Λ(A^{ij}) = {(i,j,k) : k ∈ [t]}, Λ(B^{ik}) = {(i,j,k) : j ∈ [t]}, Λ(C^{jk}) = {(i,j,k) : i ∈ [t]} (paper Section 5.1).

Equations

• TriangleInflation.onLine (TriangleInflation.Obs.A i j) x✝ = (x✝.1 == i && x✝.2.1 == j)
• TriangleInflation.onLine (TriangleInflation.Obs.B i k) x✝ = (x✝.1 == i && x✝.2.2 == k)
• TriangleInflation.onLine (TriangleInflation.Obs.C j k) x✝ = (x✝.2.1 == j && x✝.2.2 == k)

def TriangleInflation.outputs {t : ℕ} (d : Cell t → Bool) (N : Obs t → Bool) : Assign t

The output map of paper equation (eq:outputs): an observation outputs 1 exactly when its private bit and every defect on its line are 0.

Equations

• TriangleInflation.outputs d N v = decide (N v = false ∧ ∀ (c : TriangleInflation.Cell t), TriangleInflation.onLine v c = true → d c = false)

def TriangleInflation.outputsOf {t : ℕ} (x : Root t → Bool) : Assign t

The output map read off a joint root assignment.

Equations

• TriangleInflation.outputsOf x = TriangleInflation.outputs (fun (c : TriangleInflation.Cell t) => x (Sum.inl c)) fun (v : TriangleInflation.Obs t) => x (Sum.inr v)

def TriangleInflation.rootSupport {t : ℕ} (S : Finset (Obs t)) : Finset (Root t)

The root bits that a set of copied observations reads: the defect cells on their lines, together with their own private bits (paper Lemma 5.4, "disjoint inputs").

Equations

• TriangleInflation.rootSupport S = Finset.image Sum.inl {c : TriangleInflation.Cell t | ∃ v ∈ S, TriangleInflation.onLine v c = true} ∪ Finset.image Sum.inr S

def TriangleInflation.inDiagRegion {t : ℕ} (l : Fin t) (c : Cell t) : Bool

R_l, the union of the three lines of the diagonal triangle Δ_{lll}: the cells with at least two coordinates equal to l (paper equation (eq:Rl)).

Equations

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

The paper's explicit laws

def TriangleInflation.bern (r : ℝ) : Bool → ℝ

Bern(r), with Bern(r)(true) = r.

Equations

• TriangleInflation.bern r b = if b = true then r else 1 - r

def TriangleInflation.Q (ε r : ℝ) : ThreeBit → ℝ

Paper equation (eq:Q): Q(ε,r) = ε δ_{000} + (1-ε) Bern(r)^{⊗3}.

Equations

• TriangleInflation.Q ε r w = (ε * if w = (false, false, false) then 1 else 0) + (1 - ε) * (TriangleInflation.bern r w.1 * TriangleInflation.bern r w.2.1 * TriangleInflation.bern r w.2.2)

noncomputable def TriangleInflation.epsFam (t : ℕ) : ℝ

ε_t = 1/(2t³) (paper Theorem 5.2).

Equations

• TriangleInflation.epsFam t = 1 / (2 * ↑t ^ 3)

noncomputable def TriangleInflation.rFam (t : ℕ) : ℝ

r_t = (1 - ε_t)^{t-1} (paper Theorem 5.2).

Equations

• TriangleInflation.rFam t = (1 - TriangleInflation.epsFam t) ^ (t - 1)

noncomputable def TriangleInflation.Pfam (t : ℕ) : ThreeBit → ℝ

The nontermination family P_t = Q(ε_t, r_t) (paper Theorem 5.2).

Equations

• TriangleInflation.Pfam t = TriangleInflation.Q (TriangleInflation.epsFam t) (TriangleInflation.rFam t)

noncomputable def TriangleInflation.Peps (ε : ℝ) : ThreeBit → ℝ

The divergent-rejecting-order family P_ε = Q(ε, 1 - ε^{2/3}/2) (paper Proposition 5.13).

Equations

• TriangleInflation.Peps ε = TriangleInflation.Q ε (1 - ε ^ (2 / 3) / 2)

def TriangleInflation.Rlaw (p : ℝ) : ThreeBit → ℝ

R_p = (1-p) δ_{111} + p δ_{000} (paper Proposition 5.12).

Equations

• TriangleInflation.Rlaw p w = ((1 - p) * if w = (true, true, true) then 1 else 0) + p * if w = (false, false, false) then 1 else 0

noncomputable def TriangleInflation.sParam (t : ℕ) (ε r : ℝ) : ℝ

s = 1 - r/(1-ε)^{t-1}, the private-bit parameter of paper equation (eq:s).

Equations

• TriangleInflation.sParam t ε r = 1 - r / (1 - ε) ^ (t - 1)

Triangle compatibility

structure TriangleInflation.TriangleModel : Type 1

A triangle model with finite latent alphabets: three latent spaces with weight functions, and the three response probabilities f(x,z) = Pr(A = 0 | x,z), g(x,y) = Pr(B = 0 | x,y), h(z,y) = Pr(C = 0 | z,y).

• X : Type

  Latent alphabet shared by parties A and B.

• Y : Type

  Latent alphabet shared by parties B and C.

• Z : Type

  Latent alphabet shared by parties A and C.

• fintypeX : Fintype self.X
• fintypeY : Fintype self.Y
• fintypeZ : Fintype self.Z
• μX : self.X → ℝ

  Probability weight of the source shared by A and B.

• μY : self.Y → ℝ

  Probability weight of the source shared by B and C.

• μZ : self.Z → ℝ

  Probability weight of the source shared by A and C.

• f : self.X × self.Z → ℝ

  Conditional probability of outcome zero at A, given sources X and Z.

• g : self.X × self.Y → ℝ

  Conditional probability of outcome zero at B, given sources X and Y.

• h : self.Z × self.Y → ℝ

  Conditional probability of outcome zero at C, given sources Z and Y.

def TriangleInflation.respMass (q : ℝ) : Bool → ℝ

The response law of a party: probability q of the outcome 0 = false.

Equations

• TriangleInflation.respMass q b = if b = true then 1 - q else q

def TriangleInflation.TriangleModel.Valid (M : TriangleModel) : Prop

A triangle model is valid when the three source weights are laws and the three response probabilities take values in [0,1].

Equations

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

def TriangleInflation.TriangleModel.law (M : TriangleModel) : ThreeBit → ℝ

The observed law of a triangle model: the sources are independent and the responses are conditionally independent given the sources (paper Section 2.3).

Equations

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

def TriangleInflation.TriangleCompatible (P : ThreeBit → ℝ) : Prop

Paper Section 2.3: the triangle-compatible set C_tri, with the finite-latent-alphabet formalization boundary described in the file header.

Equations

• TriangleInflation.TriangleCompatible P = ∃ (M : TriangleInflation.TriangleModel), M.Valid ∧ M.law = P

The finite inflation tests

def TriangleInflation.NWFeasible (t : ℕ) (P : ThreeBit → ℝ) : Prop

Paper Definition 2.3: the Navascués–Wolfe feasible set I^NW_t. A law Γ_t on the copied observations, invariant under S_t³, whose diagonal law is the tensor power P^{⊗t}.

Equations

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

def TriangleInflation.InjectableMarginals (t : ℕ) (Γ : Assign t → ℝ) (P : ThreeBit → ℝ) : Prop

The injectable-marginal prescriptions of paper Definition 2.4: every injectable set has the corresponding marginal of P.

Equations

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

def TriangleInflation.AncestralProducts (t : ℕ) (Γ : Assign t → ℝ) (P : ThreeBit → ℝ) : Prop

The ancestral-independence prescriptions of paper Definition 2.4: every union of pairwise ancestrally independent injectable sets has the product of the corresponding marginals. The union is presented as a finite family, whose joint restriction law is required to factor.

Equations

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

def TriangleInflation.AIFeasible (t : ℕ) (P : ThreeBit → ℝ) : Prop

Paper Definition 2.4: the ancestral-independence feasible set I^AI_t.

Equations

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

The defect-cube witness

def TriangleInflation.rootWeight (t : ℕ) (ε s : ℝ) : Root t → Bool → ℝ

The per-root Bernoulli weights: defects are Bern(ε), private bits are Bern(s).

Equations

• TriangleInflation.rootWeight t ε s (Sum.inl val) = TriangleInflation.bern ε
• TriangleInflation.rootWeight t ε s (Sum.inr val) = TriangleInflation.bern s

def TriangleInflation.rootLaw (t : ℕ) (ε s : ℝ) : (Root t → Bool) → ℝ

The joint law of the independent root bits of the defect cube.

Equations

• TriangleInflation.rootLaw t ε s = TriangleInflation.prodLaw (TriangleInflation.rootWeight t ε s)

def TriangleInflation.defectLaw (t : ℕ) (ε s : ℝ) : Assign t → ℝ

Paper Section 5.1: the defect-cube law Γ_t, the pushforward of the independent defect and private bits under the output map (eq:outputs). Unfolding pushforward and prodLaw gives the explicit finite sum of product weights of paper equation (eq:table): Γ_t(w) = ∑_{x : outputsOf x = w} ∏_{roots} bern _ (x _).

Equations

• TriangleInflation.defectLaw t ε s = TriangleInflation.pushforward (TriangleInflation.rootLaw t ε s) TriangleInflation.outputsOf

First rejecting order

Paper Section 2.3: t_min^H(P) = min {t ≥ 1 : P ∉ I^H_t}. Formalized as Nat.sInf, which returns the junk value 0 when the set is empty. The set is nonempty exactly when some finite order rejects P; that this happens for every incompatible P is the asymptotic completeness of the hierarchy, which is quoted from Navascués–Wolfe in the paper and is not formalized here. Every statement about t_min below therefore either exhibits a rejecting order or assumes one.

noncomputable def TriangleInflation.tminNW (P : ThreeBit → ℝ) : ℕ

t_min^NW(P), the first order of the Navascués–Wolfe hierarchy that rejects P.

Equations

• TriangleInflation.tminNW P = sInf {t : ℕ | 1 ≤ t ∧ ¬TriangleInflation.NWFeasible t P}

noncomputable def TriangleInflation.tminAI (P : ThreeBit → ℝ) : ℕ

t_min^AI(P), the first order of the ancestral-independence hierarchy that rejects P.

Equations

• TriangleInflation.tminAI P = sInf {t : ℕ | 1 ≤ t ∧ ¬TriangleInflation.AIFeasible t P}