The convex-order distance rate for the triangle

The binary-triangle instance of manuscript Corollary 6.1 (prop:promised, eq:nw-rate) at revision 2aa1f05ce932fdeef3896c83d287abd77cd8befb: feasibility at order n gives a compatible law at squared Euclidean distance at most (1 - ‖P‖₂²)/n. This improves the weaker collision-counting coefficient proved by rate_triangle.

The argument is the convex-order one. Let Γ be a Navascués–Wolfe witness at order n and let ω be a deterministic assignment. Shifting the three families of copy indices by a common triple a ∈ [n]³ is an element of the symmetry group S_n³, and the n diagonal triangles of the shifted assignment are the n copied triangles Δ_{a_X + ℓ, a_Z + ℓ, a_Y + ℓ}. Averaging the empirical law of those n triangles over the n³ shifts returns the empirical law q_ω of all n³ copied triangles, so q_ω is a mixture of n-point empirical laws. Cauchy–Schwarz (conditional Jensen for the convex functional ‖·‖₂²) therefore bounds ‖q_ω‖₂² by the mean over shifts of the squared norm of the n-point empirical law, and the symmetry of Γ together with the diagonal prescription P^{⊗n} evaluates that mean exactly: the n coinciding pairs contribute 1 each and the n² - n distinct pairs contribute ‖P‖₂² each.

The total-variation corollaries convert with Cauchy–Schwarz on the eight atoms: d_TV(P, q_ω) ≤ (√8/2)‖P - q_ω‖₂ ≤ (√8/2)√((1-‖P‖₂²)/n) ≤ √7/(2√n), the last step by ‖P‖₂² ≥ 1/8 for a law on eight atoms.

The theorem rate_triangle retains its separate collision-counting proof. The sharp estimate below matches the current manuscript corollary, including its coefficient 1/n.

noncomputable def TriangleInflation.tvDist (P Q : ThreeBit → ℝ) : ℝ

Total variation distance between two three-bit weight functions: half the ℓ¹ distance.

Equations

• TriangleInflation.tvDist P Q = 1 / 2 * ∑ x : TriangleInflation.ThreeBit, |P x - Q x|

Collisions among the diagonal triangles

The common shift of the three copy-index families

The sharp mean squared norm

The sharp distance rate

theorem TriangleInflation.rate_triangle_sharp (n : ℕ) (hn : 1 ≤ n) {P : ThreeBit → ℝ} (hP : IsLaw P) (h : NWFeasible n P) : ∃ (Qc : ThreeBit → ℝ), IsLaw Qc ∧ TriangleCompatible Qc ∧ (sqNorm fun (x : ThreeBit) => P x - Qc x) ≤ (1 - sqNorm P) / ↑n

Manuscript Corollary 6.1 (prop:promised, eq:nw-rate) for the binary triangle. If P is feasible at order n, some triangle-compatible law Qc satisfies ‖P - Qc‖₂² ≤ (1 - ‖P‖₂²)/n. The constant carries no factor counting the three independent source types, so it improves rate_triangle, whose constant 1 - (1 - 1/n)³ is asymptotically 3/n.

Total variation

theorem TriangleInflation.tv_le_of_nwFeasible (n : ℕ) (hn : 1 ≤ n) {P : ThreeBit → ℝ} (hP : IsLaw P) (h : NWFeasible n P) : ∃ (Qc : ThreeBit → ℝ), IsLaw Qc ∧ TriangleCompatible Qc ∧ tvDist P Qc ≤ √8 / 2 * √((1 - sqNorm P) / ↑n)

The total-variation form of rate_triangle_sharp: a law feasible at order n is within (√8/2)√((1 - ‖P‖₂²)/n) in total variation of a triangle-compatible law.

theorem TriangleInflation.tv_le_sqrt_seven (n : ℕ) (hn : 1 ≤ n) {P : ThreeBit → ℝ} (hP : IsLaw P) (h : NWFeasible n P) : ∃ (Qc : ThreeBit → ℝ), IsLaw Qc ∧ TriangleCompatible Qc ∧ tvDist P Qc ≤ √7 / (2 * √↑n)

The source-count-free rate in its cleanest form: a law feasible at order n is within √7/(2√n) in total variation of a triangle-compatible law, using ‖P‖₂² ≥ 1/8.