Finner's inequality for arbitrary latent alphabets

This file removes the finite-latent-alphabet boundary from the incompatibility half of the manuscript Inflation for the Classical Triangle (papers/inflation-nontermination).

Defs.lean defines TriangleCompatible through TriangleModel, whose three latent spaces are Fintypes. That is a proper formalization boundary: a finite-latent model is in particular an arbitrary-latent model, so the finite-latent compatible set is a subset of the paper's C_△, and a theorem ¬ TriangleCompatible P is therefore the weaker of the two nonmembership statements. Closing the gap needs either the cardinality reduction of Rosset, Gisin and Wolfe (2018) — quoted in the paper, not formalized — or a proof of Finner's inequality (paper Lemma 5.7) for arbitrary latent probability spaces. This file gives the second.

TriangleModelM is a triangle model whose latent alphabets are arbitrary measurable spaces carrying probability measures, with measurable response probabilities f, g, h valued in [0,1]; its observed law is the Bochner integral of the product of the three response masses against the product measure μX ⊗ μY ⊗ μZ. No finiteness, no countability, no determinism, no regularity beyond measurability is assumed.

• finner_of_compatibleM is Lemma 5.7 in that generality: P(000)² ≤ P_A(0) P_B(0) P_C(0). The proof is the paper's: Cauchy–Schwarz in y for fixed (x,z), Cauchy–Schwarz in the independent pair (x,z) against the constant function, then f ≤ 1, g² ≤ g, h² ≤ h because the responses are probabilities, and Fubini to factor the (x,z) integral of a product of a function of x and a function of z. Cauchy–Schwarz is proved here from nonnegativity of ∫ (u - λv)², so the only measure theory used is Fubini–Tonelli and linearity.
• triangleCompatibleM_of_triangleCompatible says the new compatible set contains the old one: a finite latent alphabet carries the counting measure weighted by its source law, with every set measurable, and the Bochner integral against the product of those measures is the finite sum of TriangleModel.law. The converse inclusion is exactly the Rosset–Gisin–Wolfe reduction and is not proved here; it is not needed, because every statement below is a nonmembership statement and so uses the inclusion in the direction proved.
• The theorems named with the suffix M — witness_not_compatibleM, Rlaw_not_compatibleM, Peps_not_compatibleM, main_violationM, no_finite_characterizing_orderM — are the arbitrary-latent forms of the incompatibility statements of Finner.lean, Main.lean and Exponent.lean. They are each the same finite computation about the three-bit law (which mentions no model at all) combined with finner_of_compatibleM in place of finner_of_compatible. For these five statements the finite-latent boundary recorded in the header of Defs.lean is gone: nothing about the latent alphabets is assumed, so ¬ TriangleCompatibleM P is nonmembership in the paper's C_△ itself.

The membership half of the paper (the inflation witnesses) is untouched: it is a statement about finite inflation hierarchies and carries no latent-alphabet hypothesis.

Triangle models with arbitrary latent probability spaces

structure TriangleInflation.TriangleModelM : Type 1

A triangle model with arbitrary latent alphabets: three measurable spaces carrying probability measures, 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). This is TriangleModel of Defs.lean with Fintype weight functions replaced by MeasureTheory.Measures.

• X : Type

  The latent alphabet shared by A and B.

• Y : Type

  The latent alphabet shared by B and C.

• Z : Type

  The latent alphabet shared by A and C.

• measX : MeasurableSpace self.X
• measY : MeasurableSpace self.Y
• measZ : MeasurableSpace self.Z
• μX : MeasureTheory.Measure self.X

  The law of the source X.

• μY : MeasureTheory.Measure self.Y

  The law of the source Y.

• μZ : MeasureTheory.Measure self.Z

  The law of the source Z.

• probX : MeasureTheory.IsProbabilityMeasure self.μX
• probY : MeasureTheory.IsProbabilityMeasure self.μY
• probZ : MeasureTheory.IsProbabilityMeasure self.μZ
• f : self.X × self.Z → ℝ

  f(x,z) = Pr(A = 0 | x,z).

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

  g(x,y) = Pr(B = 0 | x,y).

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

  h(z,y) = Pr(C = 0 | z,y).

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

A measure-theoretic triangle model is valid when the three response probabilities are measurable and take values in [0,1]. The source laws are probability measures by construction, which is the measure-theoretic form of the three IsLaw conditions of TriangleModel.Valid.

Equations

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

noncomputable def TriangleInflation.TriangleModelM.law (M : TriangleModelM) : ThreeBit → ℝ

The observed law of a measure-theoretic triangle model: the integral of the product of the three response masses against the product measure μX ⊗ μY ⊗ μZ, the sources being independent and the responses conditionally independent given the sources.

Equations

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

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

Paper Section 2.3: the triangle-compatible set C_△, with no restriction on the latent alphabets. triangleCompatibleM_of_triangleCompatible shows it contains the finite-latent set TriangleCompatible of Defs.lean.

Equations

• TriangleInflation.TriangleCompatibleM P = ∃ (M : TriangleInflation.TriangleModelM), M.Valid ∧ M.law = P

Analytic tools

The measure-theoretic Finner inequality

Reduction of the observed law to the integrals of the core lemma

The Finner inequality for arbitrary latent alphabets

theorem TriangleInflation.finner_of_compatibleM {P : ThreeBit → ℝ} (hc : TriangleCompatibleM P) : atom000 P ^ 2 ≤ margA P * margB P * margC P

Paper Lemma 5.7 (lem:finner) with arbitrary probability spaces as latent alphabets: every law that comes from a measure-theoretic triangle model satisfies P(000)² ≤ P_A(0) P_B(0) P_C(0).

Finite models are measure-theoretic models

theorem TriangleInflation.triangleCompatibleM_of_triangleCompatible {P : ThreeBit → ℝ} (hP : TriangleCompatible P) : TriangleCompatibleM P

A finite-latent triangle model is a measure-theoretic triangle model: put the counting measure weighted by the source law on each latent alphabet, with all sets measurable.

The incompatibility theorems without the finite-latent boundary

Each statement below is the arbitrary-latent form of the finite-latent statement of the same name in Finner.lean, Main.lean and Exponent.lean. The finite computations are reused verbatim: they are statements about the three-bit law alone and mention no model.

theorem TriangleInflation.witness_not_compatibleM (t : ℕ) (ht : 1 ≤ t) {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1 / ↑t ^ 3) : ¬TriangleCompatibleM (Q ε ((1 - ε) ^ (t - 1)))

Paper Lemma 5.8 (lem:violation), arbitrary latent alphabets.

theorem TriangleInflation.Rlaw_not_compatibleM {p : ℝ} (h0 : 0 < p) (h1 : p < 1) : ¬TriangleCompatibleM (Rlaw p)

Paper Proposition 5.12 (prop:Rp), incompatibility half, arbitrary latent alphabets.

theorem TriangleInflation.Peps_not_compatibleM {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1 / 8) : ¬TriangleCompatibleM (Peps ε)

Paper Proposition 5.13 (prop:family), part (c), arbitrary latent alphabets.

theorem TriangleInflation.main_violationM (t : ℕ) (ht : 1 ≤ t) : epsFam t ^ 2 / 2 ≤ atom000 (Pfam t) ^ 2 - margA (Pfam t) * margB (Pfam t) * margC (Pfam t) ∧ ¬TriangleCompatibleM (Pfam t)

Paper Theorem 5.2 (thm:main), violation half, arbitrary latent alphabets.

theorem TriangleInflation.no_finite_characterizing_orderM (t : ℕ) (ht : 1 ≤ t) : ∃ (P : ThreeBit → ℝ), IsLaw P ∧ AIFeasible t P ∧ NWFeasible t P ∧ ¬TriangleCompatibleM P

Paper Theorem 5.2 (thm:main), the nontermination corollary with arbitrary latent alphabets: for every finite order t there is a three-bit law that passes the order-t test and is not triangle compatible for any latent probability spaces.