Preprocessing, assembled

Dinur's powering step needs its input to be regular, to be an expander, and to carry a self-loop at every vertex. preprocess produces all three from an arbitrary constraint graph, by composing the three steps already built:

preprocess G E = ((G.reduce E).expanderize E).addLoops

Each step costs only a constant factor of the value and none of them can turn an unsatisfiable system satisfiable, so the composite is a gap-preserving reduction with a constant of its own, preprocessConst.

Degrees compose transparently: degree reduction gives 1 + E.degree, expanderizing adds E.degree, and the loops add one, for a final degree of 2 + 2 · E.degree — a constant, as the amplification bookkeeping requires. The size is a constant multiple of the original too: the vertex set is fixed by the last two steps, so it stays the 2 · numEdges half-edges of the first.

Main definitions

• ConstraintGraph.preprocess — the composite
• ConstraintGraph.preprocessLoops — its self-loops
• ConstraintGraph.preprocessConst — the constant factor it costs

Main results

• ConstraintGraph.deg_preprocess, order_preprocess
• ConstraintGraph.satisfiable_preprocess_of_satisfiable — completeness
• ConstraintGraph.le_unsatVal_preprocess — soundness, with a constant factor
• ConstraintGraph.spectralBound_preprocess — the result is an expander, with a bound strictly below one

@[reducible, inline]

abbrev Complexity.ConstraintGraph.PreDart (E : ExpanderFamily) : Type

The darts of a preprocessed system: the self-loop, the edge-link, the cloud's and the expander's. Naming the type outright — rather than leaving it as the composite the construction produces — keeps it independent of the graph.

Equations

• Complexity.ConstraintGraph.PreDart E = (Unit ⊕ Option (Fin E.degree) ⊕ Fin E.degree)

noncomputable def Complexity.ConstraintGraph.preprocess {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : RegCSP α

Degree reduction, then expanderizing, then adding self-loops, with the dart type named.

Equations

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

theorem Complexity.ConstraintGraph.preprocess_eq {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : G.preprocess E = ((G.reduce E).expanderize E).addLoops

It is the composite it is built from.

@[instance_reducible]

noncomputable instance Complexity.ConstraintGraph.instNumEncVGraphPreprocess {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : NumEnc (G.preprocess E).graph.V

The preprocessed system's vertices are the half-edges, which are numbered by their edge and their side.

Equations

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

@[instance_reducible]

noncomputable instance Complexity.ConstraintGraph.instNumEncDGraphPreprocess {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : NumEnc (G.preprocess E).graph.D

Its darts are the self-loop, the edge-link, the cloud-links and the expander's edges, in that order.

Equations

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

noncomputable def Complexity.ConstraintGraph.preprocessLoops {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : (G.preprocess E).graph.Loops

The self-loops of the preprocessed system.

Equations

• G.preprocessLoops E = ((G.reduce E).expanderize E).graph.addLoopsLoops

@[simp]

theorem Complexity.ConstraintGraph.order_preprocess {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : (G.preprocess E).graph.order = 2 * G.numEdges

@[simp]

theorem Complexity.ConstraintGraph.deg_preprocess {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : (G.preprocess E).graph.deg = 2 + 2 * E.degree

theorem Complexity.ConstraintGraph.satisfiable_preprocess_of_satisfiable {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (h : G.Satisfiable) : (G.preprocess E).Satisfiable

Completeness.

noncomputable def Complexity.ConstraintGraph.preprocessConst (E : ExpanderFamily) (α : Type) [Fintype α] : ℝ

The constant factor preprocessing costs.

Equations

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

theorem Complexity.ConstraintGraph.unsatVal_preprocess_eq {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) [Fintype α] [Nonempty α] : (G.preprocess E).unsatVal = (G.reduce E).unsatVal * ↑(1 + E.degree) / (↑(1 + E.degree) + ↑E.degree) * ↑(1 + 2 * E.degree) / (↑(1 + 2 * E.degree) + 1)

The value after the two trivial-constraint steps, as a multiple of the value after degree reduction.

theorem Complexity.ConstraintGraph.le_unsatVal_preprocess {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) [Fintype α] [Nonempty α] : preprocessConst E α * ↑G.unsatVal ≤ ↑(G.preprocess E).unsatVal

Soundness of preprocessing.

The spectral bound

noncomputable def Complexity.ConstraintGraph.preprocessLam (E : ExpanderFamily) : ℝ

The spectral bound preprocessing achieves.

Equations

• Complexity.ConstraintGraph.preprocessLam E = (1 + (1 + 2 * ↑E.degree) * ((1 + ↑E.degree + ↑E.degree * E.lam) / (1 + ↑E.degree + ↑E.degree))) / (1 + (1 + 2 * ↑E.degree))

theorem Complexity.ConstraintGraph.spectralBound_preprocess {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : (G.preprocess E).graph.SpectralBound (preprocessLam E)

The preprocessed system is an expander.

theorem Complexity.ConstraintGraph.preprocessLam_lt_one (E : ExpanderFamily) : preprocessLam E < 1