The preprocessed graph, in numbers

Preprocessing superposes three edge sets on the half-edges of a graph: the edge-links pairing the two halves of an edge, the cloud-links joining the halves that share an endpoint, and the expander's own edges, with a self-loop added at every vertex. This module reads off what each of those does to a number.

The numbering is the one NumEnc gives: a half-edge is 2 e or 2 e + 1 according to which end it is — the same number DegreeReduction sorts clouds by — and a dart is 0 for the self-loop, 1 for the edge-link, 2 + j for the j-th cloud-link and 2 + degree + j for the j-th expander edge.

Main results

• Complexity.ConstraintGraph.enc_halfEdge — a half-edge's number is its code
• Complexity.ConstraintGraph.enc_preLoop, enc_preEdge, enc_preCloud, enc_preExp — the four kinds of dart, and preDart_cases: there are no others

theorem Complexity.ConstraintGraph.enc_halfEdge {α : Type} (G : ConstraintGraph α) (p : G.HalfEdge) : NumEnc.enc p = G.halfCode p

A half-edge's number is the code the clouds are sorted by.

def Complexity.ConstraintGraph.preLoop {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : (G.preprocess E).graph.D

The self-loop at a vertex.

Equations

• G.preLoop E = Sum.inl ()

def Complexity.ConstraintGraph.preEdge {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : (G.preprocess E).graph.D

The link to the other half of the same edge.

Equations

• G.preEdge E = Sum.inr (Sum.inl none)

def Complexity.ConstraintGraph.preCloud {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (j : Fin E.degree) : (G.preprocess E).graph.D

The j-th link inside the cloud.

Equations

• G.preCloud E j = Sum.inr (Sum.inl (some j))

def Complexity.ConstraintGraph.preExp {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (j : Fin E.degree) : (G.preprocess E).graph.D

The j-th edge of the superposed expander.

Equations

• G.preExp E j = Sum.inr (Sum.inr j)

theorem Complexity.ConstraintGraph.enc_preLoop {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : NumEnc.enc (G.preLoop E) = 0

The darts of the preprocessed graph: a self-loop, an edge-link, the cloud-links, and the expander's edges.

theorem Complexity.ConstraintGraph.enc_preEdge {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : NumEnc.enc (G.preEdge E) = 1

theorem Complexity.ConstraintGraph.enc_preCloud {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (j : Fin E.degree) : NumEnc.enc (G.preCloud E j) = 2 + ↑j

theorem Complexity.ConstraintGraph.enc_preExp {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (j : Fin E.degree) : NumEnc.enc (G.preExp E j) = 2 + E.degree + ↑j

theorem Complexity.ConstraintGraph.preDart_cases {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (d : (G.preprocess E).graph.D) : d = G.preLoop E ∨ d = G.preEdge E ∨ (∃ (j : Fin E.degree), d = G.preCloud E j) ∨ ∃ (j : Fin E.degree), d = G.preExp E j

Every dart is one of the four kinds.

What each kind of dart does

theorem Complexity.ConstraintGraph.rot_preLoop {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (v : (G.preprocess E).graph.V) : (G.preprocess E).graph.rot (v, G.preLoop E) = (v, G.preLoop E)

theorem Complexity.ConstraintGraph.rot_preEdge {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (v : G.HalfEdge) : (G.preprocess E).graph.rot (v, G.preEdge E) = (G.flipHalf v, G.preEdge E)

theorem Complexity.ConstraintGraph.rot_preCloud {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (v : G.HalfEdge) (j : Fin E.degree) : (G.preprocess E).graph.rot (v, G.preCloud E j) = ((G.cloudRot E v j).1, G.preCloud E (G.cloudRot E v j).2)

theorem Complexity.ConstraintGraph.rot_preExp {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (v : G.HalfEdge) (j : Fin E.degree) : (G.preprocess E).graph.rot (v, G.preExp E j) = ((E.vertexEquiv (G.reduce E).graph) (E.rot (G.reduce E).graph.order ((E.vertexEquiv (G.reduce E).graph).symm v, j)).1, G.preExp E (E.rot (G.reduce E).graph.order ((E.vertexEquiv (G.reduce E).graph).symm v, j)).2)

The three moves, in numbers

theorem Complexity.ConstraintGraph.enc_flipHalf {α : Type} (G : ConstraintGraph α) (p : G.HalfEdge) : NumEnc.enc (G.flipHalf p) = if NumEnc.enc p % 2 = 0 then NumEnc.enc p + 1 else NumEnc.enc p - 1

Crossing an edge flips the last bit of the number.

theorem Complexity.ConstraintGraph.enc_vertexEquiv {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (x : Fin (G.reduce E).graph.order) : NumEnc.enc ((E.vertexEquiv (G.reduce E).graph) x) = ↑x

The expander's vertices are numbered as the graph's are.

theorem Complexity.ConstraintGraph.val_vertexEquiv_symm {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (v : (G.reduce E).graph.V) : ↑((E.vertexEquiv (G.reduce E).graph).symm v) = NumEnc.enc v

The cloud step, in numbers

noncomputable def Complexity.ConstraintGraph.cloudStepNum {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) (v : Fin G.numVerts) (c : ℕ) (j : Fin E.degree) : ℕ × ℕ

The cloud step on numbers: count how many of the cloud's half-edges come before this one, let the expander family move that index, and read off the code the new index names.

Equations

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

theorem Complexity.ConstraintGraph.cloudStepNum_eq {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) (p : G.HalfEdge) (j : Fin E.degree) : G.cloudStepNum E (G.owner p) (NumEnc.enc p) j = (NumEnc.enc (G.cloudRot E p j).1, ↑(G.cloudRot E p j).2)

The numbers run the cloud step.

The whole rotation map, in numbers

noncomputable def Complexity.ConstraintGraph.ownerNum {α : Type} (G : ConstraintGraph α) (v : ℕ) : ℕ

The vertex a half-edge number is attached to.

Equations

• G.ownerNum v = if h : v / 2 < G.numEdges then if v % 2 = 0 then ↑(G.head ⟨v / 2, h⟩) else ↑(G.tail ⟨v / 2, h⟩) else 0

theorem Complexity.ConstraintGraph.ownerNum_enc {α : Type} (G : ConstraintGraph α) (p : G.HalfEdge) : G.ownerNum (NumEnc.enc p) = ↑(G.owner p)

noncomputable def Complexity.ConstraintGraph.cloudStepN {α : Type} (G : ConstraintGraph α) (E : ExpanderFamily) (u c j : ℕ) : ℕ × ℕ

The cloud step, on numbers throughout.

Equations

• G.cloudStepN E u c j = if hu : u < G.numVerts then if hj : j < E.degree then G.cloudStepNum E ⟨u, hu⟩ c ⟨j, hj⟩ else (c, j) else (c, j)

noncomputable def Complexity.ConstraintGraph.expStepN {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (v j : ℕ) : ℕ × ℕ

The expander step, on numbers.

Equations

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

noncomputable def Complexity.ConstraintGraph.preRotNum {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (v d : ℕ) : ℕ × ℕ

The preprocessed graph's rotation map, on numbers. Dart 0 is the self-loop, dart 1 crosses the edge, darts 2 to deg + 1 rotate inside the cloud, and the rest are the superposed expander's.

Equations

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

theorem Complexity.ConstraintGraph.preRotNum_eq {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (v : G.HalfEdge) (d : (G.preprocess E).graph.D) : G.preRotNum E (NumEnc.enc v) (NumEnc.enc d) = (NumEnc.enc ((G.preprocess E).graph.rot (v, d)).1, NumEnc.enc ((G.preprocess E).graph.rot (v, d)).2)

The numbers run the preprocessed graph's rotation map.