This file will host the Lean-level encoding of the exact rational certificate and the main theorem for n = 10^6.

Planned approach (to be implemented):

• encode the reduced SDP data over ℚ (constraints and seven small PSD blocks),
• import the exact rational dual certificate,
• prove dual feasibility and evaluate the dual objective exactly,
• translate the resulting edge-correlation bound into a monochromatic-edge bound.

def Distributed2Coloring.LowerBound.N1000000.coeffAt (a : Array ℤ) (i : ℕ) : ℤ

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

Equations

• Distributed2Coloring.LowerBound.N1000000.coeffAt a i = a.getD i 0

def Distributed2Coloring.LowerBound.N1000000.innerD2 (A B : Array (Array ℤ)) : ℤ

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

Equations

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

def Distributed2Coloring.LowerBound.N1000000.linNumD (i : ℕ) : ℤ

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

Equations

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

def Distributed2Coloring.LowerBound.N1000000.psdNumD2 (i : ℕ) : ℤ

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

Equations

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

def Distributed2Coloring.LowerBound.N1000000.c (i : ℕ) : ℤ

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

Equations

• Distributed2Coloring.LowerBound.N1000000.c i = if i = Distributed2Coloring.LowerBound.N1000000Data.edgeVar then 1 else 0

def Distributed2Coloring.LowerBound.N1000000.stationarityLHSD2 (i : ℕ) : ℤ

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

Equations

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

def Distributed2Coloring.LowerBound.N1000000.dualObjectiveComputedD2 : ℤ

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

Equations

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

theorem Distributed2Coloring.LowerBound.N1000000.dualObjective_ok : dualObjectiveComputedD2 = N1000000Data.dualObjectiveD2

def Distributed2Coloring.LowerBound.N1000000.stationarityOK : Bool

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

Equations

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

theorem Distributed2Coloring.LowerBound.N1000000.stationarityOK_true : stationarityOK = true