The “three-parameter recursive cutoff” construction (a radius-1 factor-of-i.i.d. triple rule).

This file defines the explicit rule (as a ClassicalAlgorithm) for a convenient rational choice of parameters (t, t1, t2). Later files will prove the quantitative bound ClassicalAlgorithm.p recursive3ParamAlg < 24118/100000.

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.t : Rand

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.t = ⟨5 / 8, Distributed2Coloring.UpperBound.Recursive3Param.t._proof_3⟩

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.t1 : Rand

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.t1 = ⟨3 / 8, Distributed2Coloring.UpperBound.Recursive3Param.t1._proof_2⟩

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.t2 : Rand

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.t2 = ⟨17 / 32, Distributed2Coloring.UpperBound.Recursive3Param.t2._proof_3⟩

theorem Distributed2Coloring.UpperBound.Recursive3Param.t1_lt_t2 : ↑t1 < ↑t2

theorem Distributed2Coloring.UpperBound.Recursive3Param.t2_lt_t : ↑t2 < ↑t

theorem Distributed2Coloring.UpperBound.Recursive3Param.t_lt_one : ↑t < 1

theorem Distributed2Coloring.UpperBound.Recursive3Param.zero_lt_t : 0 < ↑t

theorem Distributed2Coloring.UpperBound.Recursive3Param.t1_le_t2 : ↑t1 ≤ ↑t2

theorem Distributed2Coloring.UpperBound.Recursive3Param.t2_le_t : ↑t2 ≤ ↑t

Base surface z_base (one parameter)

This is the base cutoff surface z_base(x,y;t) described in the project write-up.

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.zBase (x y : Rand) : ℝ

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

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

Recursive surface at the chosen parameters

For these concrete dyadic-rational parameters, the rescaling maps phi and psi from the tex are both globally linear, which simplifies the “inside square” formula substantially.

We implement the recursive surface directly using the induced partition (this is definitionally a 3-parameter rule with parameters (t,t1,t2)).

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.z0 (x y : Rand) : ℝ

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

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

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.g (x y z : Rand) : Color

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.g x y z = if ↑z < Distributed2Coloring.UpperBound.Recursive3Param.z0 x y then 1 else 0

theorem Distributed2Coloring.UpperBound.Recursive3Param.measurable_zBase : Measurable fun (xy : Rand × Rand) => zBase xy.1 xy.2

theorem Distributed2Coloring.UpperBound.Recursive3Param.measurable_z0 : Measurable fun (xy : Rand × Rand) => z0 xy.1 xy.2

theorem Distributed2Coloring.UpperBound.Recursive3Param.measurable_g : Measurable fun (xyz : Rand × Rand × Rand) => g xyz.1 xyz.2.1 xyz.2.2

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.recursive3ParamAlg : ClassicalAlgorithm

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

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

Range lemmas

For probability computations, it is convenient to view z0 x y as an element of the unit interval.

theorem Distributed2Coloring.UpperBound.Recursive3Param.zBase_mem_Icc (x y : Rand) : zBase x y ∈ Set.Icc 0 1

theorem Distributed2Coloring.UpperBound.Recursive3Param.z0_mem_Icc (x y : Rand) : z0 x y ∈ Set.Icc 0 1

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.z0I (x y : Rand) : Rand

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.z0I x y = ⟨Distributed2Coloring.UpperBound.Recursive3Param.z0 x y, ⋯⟩

theorem Distributed2Coloring.UpperBound.Recursive3Param.g_eq_one_iff (x y z : Rand) : g x y z = 1 ↔ ↑z < z0 x y

theorem Distributed2Coloring.UpperBound.Recursive3Param.g_eq_zero_iff (x y z : Rand) : g x y z = 0 ↔ ¬↑z < z0 x y