Reading a half-edge's endpoint

A half-edge is numbered 2 e or 2 e + 1 according to which end of edge e it is, so the vertex it hangs from is one of that edge's two endpoints — and both are written down in the encoded graph. Halving the number picks the edge, its parity picks the end.

Main definitions

• Complexity.ownerFn — the vertex a half-edge number hangs from
• Complexity.cloudSizeFn — how many half-edges hang from a vertex
• Complexity.cloudIdxFn — how many of them come first

Main results

• Complexity.ownerFn_mem_FP, Complexity.ownerFn_eq
• Complexity.cloudSizeFn_mem_FP, Complexity.length_cloudSizeFn — the count is the number of half-edges the rule accepts
• Complexity.ConstraintGraph.count_owner_eq_card_cloud — and counting numbers is counting half-edges
• Complexity.cloudStepFn, Complexity.expStepFn — the two moves that need the expander
• Complexity.preRotFn — the preprocessed graph's rotation map, as one function

Main results

• Complexity.expStepFn_eq — the expander move computes what it should

noncomputable def Complexity.ownerFn (z : List Bool) : List Bool

The vertex a half-edge hangs from, on pair (encoded graph) (unary p).

Equations

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

theorem Complexity.ownerFn_mem_FP : ownerFn ∈ FP

Counting a cloud

noncomputable def Complexity.cloudMark (w : List Bool) : List Bool

One mark when the half-edge j hangs from the vertex asked for. The argument is pair (pair (encoded graph) (unary u)) (unary j).

Equations

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

theorem Complexity.cloudMark_mem_FP : cloudMark ∈ FP

theorem Complexity.length_cloudMark (Gz u j : List Bool) : (cloudMark (pair (pair Gz u) j)).length = if (ownerFn (pair Gz j)).length = u.length then 1 else 0

noncomputable def Complexity.cloudSizeFn (z : List Bool) : List Bool

How many half-edges hang from the vertex asked for, on pair (encoded graph) (unary u).

Equations

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

theorem Complexity.cloudSizeFn_mem_FP : cloudSizeFn ∈ FP

theorem Complexity.length_cloudSizeFn (Gz u : List Bool) (m : ℕ) (hm : (mulC 2 (posCount (pairSnd Gz))).length = m) : (cloudSizeFn (pair Gz u)).length = ∑ j ∈ Finset.range m, if (ownerFn (pair Gz (List.replicate j true))).length = u.length then 1 else 0

The count is the number of half-edges the rule accepts.

noncomputable def Complexity.cloudIdxFn (z : List Bool) : List Bool

How many half-edges before this one hang from the same vertex, on pair (encoded graph) (unary p).

Equations

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

theorem Complexity.cloudIdxFn_mem_FP : cloudIdxFn ∈ FP

theorem Complexity.length_cloudIdxFn (Gz : List Bool) (p : ℕ) : (cloudIdxFn (pair Gz (List.replicate p true))).length = ∑ j ∈ Finset.range p, if (ownerFn (pair Gz (List.replicate j true))).length = (ownerFn (pair Gz (List.replicate p true))).length then 1 else 0

The index is the number of earlier half-edges in the same cloud.

Finding a cloud's members

noncomputable def Complexity.eltMark (w : List Bool) : List Bool

One mark when the half-edge c is the k-th of the cloud of u. The argument is pair (pair (encoded graph) (pair (unary u) (unary k))) (unary c).

Equations

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

theorem Complexity.eltMark_mem_FP : eltMark ∈ FP

theorem Complexity.length_eltMark (Gz u k c : List Bool) : (eltMark (pair (pair Gz (pair u k)) c)).length = if (ownerFn (pair Gz c)).length = u.length then if (cloudIdxFn (pair Gz c)).length = k.length then 1 else 0 else 0

noncomputable def Complexity.cloudEltFn (z : List Bool) : List Bool

The k-th half-edge of the cloud of u, on pair (encoded graph) (pair (unary u) (unary k)).

Equations

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

theorem Complexity.cloudEltFn_eq_replicate (z : List Bool) : cloudEltFn z = List.replicate (cloudEltFn z).length true

theorem Complexity.cloudEltFn_mem_FP : cloudEltFn ∈ FP

theorem Complexity.ownerFn_eq {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (p : ℕ) (hp : p / 2 < G.numEdges) : ownerFn (pair (encGraph G) (List.replicate p true)) = List.replicate (G.ownerNum p) true

The reading is the owner.

theorem Complexity.ConstraintGraph.count_owner_eq_card_cloud {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) : {j ∈ Finset.range (2 * G.numEdges) | G.ownerNum j = ↑v}.card = (G.cloud v).card

Counting numbers is counting half-edges.

theorem Complexity.ConstraintGraph.count_owner_lt_eq_countBelow {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) (m : ℕ) (hm : m ≤ 2 * G.numEdges) : {j ∈ Finset.range m | G.ownerNum j = ↑v}.card = countBelow (G.cloudCodes v) m

Counting numbers below a bound is counting codes below it.

What the counts compute

theorem Complexity.length_count_encGraph {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) : (mulC 2 (posCount (pairSnd (encGraph G)))).length = 2 * G.numEdges

theorem Complexity.length_cloudSizeFn_eq {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (v : Fin G.numVerts) : (cloudSizeFn (pair (encGraph G) (List.replicate (↑v) true))).length = (G.cloud v).card

The size the algorithm counts is the size of the cloud.

theorem Complexity.length_cloudIdxFn_eq {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (m : ℕ) (hm : m < 2 * G.numEdges) : (cloudIdxFn (pair (encGraph G) (List.replicate m true))).length = countBelow (G.cloudCodes ⟨G.ownerNum m, ⋯⟩) m

The index the algorithm counts is the position in the cloud.

theorem Complexity.halfCode_lt {α : Type} (G : ConstraintGraph α) (p : G.HalfEdge) : G.halfCode p < 2 * G.numEdges

The code of a half-edge is below twice the edge count.

theorem Complexity.length_cloudEltFn_eq {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (v : Fin G.numVerts) (k : ℕ) (hk : k < (G.cloudList v).length) : (cloudEltFn (pair (encGraph G) (pair (List.replicate (↑v) true) (List.replicate k true)))).length = G.halfCode (G.cloudList v)[k]

The search finds the k-th half-edge of the cloud.

The two moves that need the expander

noncomputable def Complexity.cloudStepFn (F : FinBase) (pol : Polynomial ℕ) (z : List Bool) : List Bool

The cloud move, on pair (pair (graph) (unary owner)) (pair (unary code) (unary dart)): rotate the half-edge's index inside its cloud, then read off the half-edge the new index names.

Equations

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

theorem Complexity.cloudStepFn_mem_FP (F : FinBase) (pol : Polynomial ℕ) : cloudStepFn F pol ∈ FP

noncomputable def Complexity.expStepFn (F : FinBase) (pol : Polynomial ℕ) (z : List Bool) : List Bool

The expander move, on pair (graph) (pair (unary vertex) (unary dart)).

Equations

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

theorem Complexity.expStepFn_mem_FP (F : FinBase) (pol : Polynomial ℕ) : expStepFn F pol ∈ FP

theorem Complexity.cloudStepFn_eq {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (F : FinBase) (pol : Polynomial ℕ) (hd : 1 < F.deg) (v : Fin G.numVerts) (c j : ℕ) (hc : c < 2 * G.numEdges) (hown : G.ownerNum c = ↑v) (hj : j < (F.toFamily hd).degree) (hp : F.fitLevel hd (G.cloudList v).length ≤ Polynomial.eval (G.cloudList v).length pol) : cloudStepFn F pol (pair (pair (encGraph G) (List.replicate (↑v) true)) (pair (List.replicate c true) (List.replicate j true))) = pair (List.replicate (G.cloudStepNum (F.toFamily hd) v c ⟨j, hj⟩).1 true) (List.replicate (G.cloudStepNum (F.toFamily hd) v c ⟨j, hj⟩).2 true)

The cloud move computes what it should.

theorem Complexity.expStepFn_eq {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (F : FinBase) (pol : Polynomial ℕ) (hd : 1 < F.deg) (v j : ℕ) (hn : 0 < 2 * G.numEdges) (hp : F.fitLevel hd (2 * G.numEdges) ≤ Polynomial.eval (2 * G.numEdges) pol) : expStepFn F pol (pair (encGraph G) (pair (List.replicate v true) (List.replicate j true))) = pair (List.replicate (F.famRotVal hd (2 * G.numEdges) (v, j)).1 true) (List.replicate (F.famRotVal hd (2 * G.numEdges) (v, j)).2 true)

The expander move computes what it should.

The whole rotation map

noncomputable def Complexity.flipFn (v : List Bool) : List Bool

Crossing an edge: flip the last bit of the vertex number.

Equations

• Complexity.flipFn v = Complexity.ifEqLen (Complexity.modC 2 v) [] (v ++ [true]) (Complexity.dropOne v)

theorem Complexity.flipFn_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (z : List Bool) => flipFn (f z)) ∈ FP

theorem Complexity.flipFn_eq (v : ℕ) : flipFn (List.replicate v true) = List.replicate (if v % 2 = 0 then v + 1 else v - 1) true

noncomputable def Complexity.preRotFn (F : FinBase) (pol : Polynomial ℕ) (deg : ℕ) (z : List Bool) : List Bool

The preprocessed graph's rotation map, on pair (graph) (pair (unary vertex) (unary dart)). Dart 0 is the self-loop, dart 1 crosses the edge, the next deg are the cloud's, and the rest are the superposed expander's.

Equations

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

theorem Complexity.preRotFn_mem_FP (F : FinBase) (pol : Polynomial ℕ) (deg : ℕ) : preRotFn F pol deg ∈ FP

theorem Complexity.preRotFn_eq {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (F : FinBase) (pol : Polynomial ℕ) (hd : 1 < F.deg) (v d : ℕ) (hv : v < 2 * G.numEdges) (hdlt : d < 2 + 2 * (F.toFamily hd).degree) (hpc : ∀ (u : Fin G.numVerts), F.fitLevel hd (G.cloudList u).length ≤ Polynomial.eval (G.cloudList u).length pol) (hpe : F.fitLevel hd (2 * G.numEdges) ≤ Polynomial.eval (2 * G.numEdges) pol) : preRotFn F pol (F.toFamily hd).degree (pair (encGraph G) (pair (List.replicate v true) (List.replicate d true))) = pair (List.replicate (G.preRotNum (F.toFamily hd) v d).1 true) (List.replicate (G.preRotNum (F.toFamily hd) v d).2 true)

The whole rotation map computes what it should.