The defect cube: laws of triangles, symmetry, and the diagonal

Proofs of paper Lemma 5.5 (lem:triangle-law), equation (eq:s), Lemma 5.6 (lem:symmetry) and Lemma 5.9 (lem:diag). The independence lemmas they build on are in Defect.lean.

The three substantive proofs share one mechanism. The output of a copied observation is the conjunction "my private bit is 0, and every defect on my line is 0", so it is the indicator allFalse S that a block S of root bits is all-zero. Under a product weight such an indicator has marginal Bern(∏_{u ∈ S} w_u(0)) (pushforward_allFalse), and indicators of disjoint blocks are independent (indep_of_disjoint_support). Lemma 5.5 splits the root bits read by Δ_{ijk} into four disjoint blocks — the shared cell (i,j,k), and for each of the three observations its private bit together with the t-1 remaining cells of its line — and assembles the four marginals into Q(ε,r).

Private helpers

Everything in DefectLawAux is auxiliary to the four statements below.

The four root blocks of a copied triangle

Weights and disjointness of the blocks

The induced permutation of root bits (Lemma 5.6)

Lemma 5.9

The law of a copied triangle (Lemma 5.5)

theorem TriangleInflation.defect_copiedTriangle_law {t : ℕ} {ε s : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (i j k : Fin t) : pushforward (defectLaw t ε s) (readTriangle i j k) = Q ε ((1 - s) * (1 - ε) ^ (t - 1))

Paper Lemma 5.5 (lem:triangle-law): under the defect law every copied triangle Δ_{ijk} has law Q(ε, r) with r = (1-s)(1-ε)^{t-1}.

theorem TriangleInflation.one_sub_sParam_mul (t : ℕ) {ε r : ℝ} (hε : ε < 1) : (1 - sParam t ε r) * (1 - ε) ^ (t - 1) = r

Paper equation (eq:s): with s = 1 - r/(1-ε)^{t-1} the copied-triangle parameter (1-s)(1-ε)^{t-1} is r.

theorem TriangleInflation.sParam_mem_Icc (t : ℕ) {ε r : ℝ} (hε1 : ε < 1) (hr0 : 0 ≤ r) (hr1 : r ≤ (1 - ε) ^ (t - 1)) : 0 ≤ sParam t ε r ∧ sParam t ε r ≤ 1

Paper equation (eq:s): s ∈ [0,1] exactly in the parameter range of Theorem 5.1.

Symmetry (Lemma 5.6)

theorem TriangleInflation.defect_symmetric {t : ℕ} (ε s : ℝ) : SymmetricLaw t (defectLaw t ε s)

Paper Lemma 5.6 (lem:symmetry): the defect law is invariant under independent permutations of the X-, Z- and Y-copy indices.

The diagonal (Lemma 5.9)

theorem TriangleInflation.diagRegion_disjoint {t : ℕ} {l m : Fin t} (h : l ≠ m) (c : Cell t) : ¬(inDiagRegion l c = true ∧ inDiagRegion m c = true)

Paper Lemma 5.9 (lem:diag), combinatorial half: the regions R_l of distinct diagonal triangles are disjoint, since a cell cannot have two coordinates equal to l and two equal to m ≠ l.

theorem TriangleInflation.inDiagRegion_iff {t : ℕ} (l : Fin t) (c : Cell t) : inDiagRegion l c = true ↔ ∃ v ∈ diagonalTriangle l, onLine v c = true

The region R_l of paper equation (eq:Rl) is the root support of the diagonal triangle Δ_{lll} on the defect cells.

theorem TriangleInflation.defect_diagonal_law {t : ℕ} {ε s : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : pushforward (defectLaw t ε s) readDiagonal = tensorPow t (Q ε ((1 - s) * (1 - ε) ^ (t - 1)))

Paper Lemma 5.9 (lem:diag): the t diagonal triangles are mutually independent under the defect law and their joint law is Q(ε,r)^{⊗t} with r = (1-s)(1-ε)^{t-1}. This is the tensor-power diagonal condition of Definition 2.3(ii).