The Finner inequality and the explicit violation

Statements for paper Section 5.2 (sec:incompat): Lemma 5.7 (lem:finner), Lemma 5.8 (lem:violation), and the incompatibility half of Proposition 5.12 (prop:Rp). Proofs are deferred.

This file also collects the basic normalization facts about the weight functions of Defs.lean, which the later files use.

Basic normalization facts

theorem TriangleInflation.bern_isLaw {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) : IsLaw (bern r)

Bern(r) is a law when r ∈ [0,1].

theorem TriangleInflation.prodLaw_isLaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] {w : ι → Bool → ℝ} (hw : ∀ (i : ι), IsLaw (w i)) : IsLaw (prodLaw w)

A product of per-coordinate laws is a law.

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

A pushforward of a law is a law.

theorem TriangleInflation.Q_isLaw {ε r : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : IsLaw (Q ε r)

Q(ε,r) is a law for ε, r ∈ [0,1] (paper equation (eq:Q)).

theorem TriangleInflation.Rlaw_isLaw {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) : IsLaw (Rlaw p)

R_p is a law for p ∈ [0,1] (paper Proposition 5.12).

theorem TriangleInflation.defectLaw_isLaw {t : ℕ} {ε s : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : IsLaw (defectLaw t ε s)

The defect-cube law is a law when ε, s ∈ [0,1] (paper Section 5.1).

The Finner inequality

theorem TriangleInflation.finner_of_compatible {P : ThreeBit → ℝ} (h : TriangleCompatible P) : atom000 P ^ 2 ≤ margA P * margB P * margC P

Paper Lemma 5.7 (lem:finner), the event form of Finner's inequality for the triangle: every triangle-compatible law satisfies P(000)² ≤ P_A(0) P_B(0) P_C(0).

Formalization boundary: TriangleCompatible uses finite latent alphabets (see the header of Defs.lean); the paper's proof uses neither finiteness of the latent alphabets nor determinism of the responses, so the statement here is the finite-latent instance of it.

The explicit violation

theorem TriangleInflation.witness_violation (t : ℕ) (ht : 1 ≤ t) {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1 / ↑t ^ 3) : margA (Q ε ((1 - ε) ^ (t - 1))) * margB (Q ε ((1 - ε) ^ (t - 1))) * margC (Q ε ((1 - ε) ^ (t - 1))) < atom000 (Q ε ((1 - ε) ^ (t - 1))) ^ 2

Paper Lemma 5.8 (lem:violation), first part: for t ≥ 1 and 0 < ε < t⁻³, the law Q(ε, (1-ε)^{t-1}) strictly violates the Finner inequality.

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

Paper Lemma 5.8 (lem:violation), conclusion: such a Q(ε,(1-ε)^{t-1}) is not triangle compatible.

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

Paper Lemma 5.8 (lem:violation), quantitative part: at ε = ε_t = 1/(2t³) the Finner margin of P_t = Q(ε_t, r_t) is at least ε_t²/2.

R_p

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

Paper Proposition 5.12 (prop:Rp), incompatibility half: R_p violates the Finner inequality, hence is not triangle compatible, for every 0 < p < 1.