Algebraic cancellation lemma used to keep integer cross-multiplication checks from ballooning: we replace a term (s : ℚ) / (D : ℚ) by the reduced fraction obtained by cancelling g = gcd(|s|, D).

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.Q : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000BCompressionCompute.Q = ℚ

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.Var : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000BCompressionCompute.Var = Distributed2Coloring.LowerBound.N1000000WeakDuality.Var

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.Block : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000BCompressionCompute.Block = Distributed2Coloring.LowerBound.N1000000WeakDuality.Block

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.DirIdx : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000BCompressionCompute.DirIdx = Distributed2Coloring.LowerBound.N1000000StructureConstants.DirIdx

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.qOfNat (m : ℕ) : Q

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

Equations

• Distributed2Coloring.LowerBound.N1000000BCompressionCompute.qOfNat m = ↑m

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.iOfNat (m : ℕ) : ℤ

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

Equations

• Distributed2Coloring.LowerBound.N1000000BCompressionCompute.iOfNat m = Int.ofNat m

def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.invDir (d : DirIdx) : DirIdx

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

Equations

• Distributed2Coloring.LowerBound.N1000000BCompressionCompute.invDir d = ⟨Distributed2Coloring.LowerBound.N1000000Witness.tTr[↑d]!, ⋯⟩

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000BCompressionCompute.basisDen (r : Block) : ℕ

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

Equations

• Distributed2Coloring.LowerBound.N1000000BCompressionCompute.basisDen r = Distributed2Coloring.LowerBound.N1000000WedderburnData.moduleBasisDen[↑r]!

def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.bValNum (r : Block) (j : Fin 3) (k : DirIdx) : ℤ

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.N1000000BCompressionCompute.bVal (r : Block) (j : Fin 3) (k : DirIdx) : Q

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.N1000000BCompressionCompute.compBasis (r : Block) (d : DirIdx) : Matrix (Fin 3) (Fin 3) Q

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.N1000000BCompressionCompute.div_by_D_eq_div_by_div_gcd (s : ℤ) : have g := s.natAbs.gcd N1000000Data.D; ↑s / ↑N1000000Data.D = ↑s / ↑↑g / ↑(N1000000Data.D / g)

def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.compBasisIntEntry (r : Block) (d : DirIdx) (p q : Fin 3) : ℤ

Integer numerator of a compressed basis entry, skipping zero basis coordinates.

Equations

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

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.compBasisIntEntry_eq_sum (r : Block) (d : DirIdx) (p q : Fin 3) : compBasisIntEntry r d p q = ∑ k : DirIdx, ∑ a : DirIdx, iOfNat (N1000000StructureConstants.baseTypeCount k) * iOfNat (N1000000StructureConstants.N k a d) * bValNum r p k * bValNum r q a

Skipping zero coordinates and factoring row coefficients preserves the defining double sum.

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.basisDenQ_ne_zero (r : Block) : ↑(basisDen r) ≠ 0

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.compBasis_entry_eq_div (r : Block) (d : DirIdx) (p q : Fin 3) : compBasis r d p q = ↑(compBasisIntEntry r d p q) / (↑(basisDen r) * ↑(basisDen r))

def Distributed2Coloring.LowerBound.N1000000BCompressionCompute.compBasisSymm (r : Block) (d : DirIdx) : Matrix (Fin 3) (Fin 3) Q

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.N1000000BCompressionCompute.idDirIdx : DirIdx

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.N1000000BCompressionCompute.varOrbit (i : Var) : DirIdx

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

Equations

• Distributed2Coloring.LowerBound.N1000000BCompressionCompute.varOrbit i = ⟨Distributed2Coloring.LowerBound.N1000000Witness.varToOrbitRep[↑i]!, ⋯⟩