A cloud, by counting

Degree reduction rotates inside a cloud through the cloud's enumeration: the half-edge it starts from is located by List.idxOf, and the one it lands on is read off by position. Neither operation is available to an algorithm, which can only count. This module replaces both by counts of half-edge numbers.

The cloud is enumerated in order of those numbers, so a half-edge's position is the number of smaller numbers in the cloud, and the half-edge at a position is the one whose number has that many smaller numbers below it.

Main definitions

• Complexity.ConstraintGraph.cloudCodes — the numbers of a cloud's half-edges

Main results

• Complexity.ConstraintGraph.idxOf_cloudList — the position is a count
• Complexity.ConstraintGraph.halfCode_getElem_cloudList — and the entry at a position is named by the count that reaches it

noncomputable def Complexity.ConstraintGraph.cloudCodes {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) : Finset ℕ

The numbers of the half-edges attached to a vertex.

Equations

• G.cloudCodes v = Finset.image G.halfCode (G.cloud v)

@[simp]

theorem Complexity.ConstraintGraph.mem_cloudCodes {α : Type} (G : ConstraintGraph α) {v : Fin G.numVerts} {c : ℕ} : c ∈ G.cloudCodes v ↔ ∃ (p : G.HalfEdge), G.owner p = v ∧ G.halfCode p = c

@[simp]

theorem Complexity.ConstraintGraph.card_cloudCodes {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) : (G.cloudCodes v).card = (G.cloud v).card

@[simp]

theorem Complexity.ConstraintGraph.length_cloudList {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) : (G.cloudList v).length = (G.cloud v).card

theorem Complexity.ConstraintGraph.countBelow_cloudCodes {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) (c : ℕ) : countBelow (G.cloudCodes v) c = {q ∈ G.cloud v | G.halfCode q < c}.card

Counting the smaller numbers of a cloud is counting its smaller half-edges.

theorem Complexity.ConstraintGraph.idxOf_cloudList {α : Type} (G : ConstraintGraph α) {v : Fin G.numVerts} {p : G.HalfEdge} (hp : G.owner p = v) : List.idxOf p (G.cloudList v) = countBelow (G.cloudCodes v) (G.halfCode p)

A half-edge's position in its cloud is a count.

theorem Complexity.ConstraintGraph.card_cloudCodes_eq_length {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) : (G.cloudCodes v).card = (G.cloudList v).length

theorem Complexity.ConstraintGraph.halfCode_getElem_cloudList {α : Type} (G : ConstraintGraph α) (v : Fin G.numVerts) (k : ℕ) (hk : k < (G.cloudList v).length) : ((G.cloudCodes v).orderEmbOfFin ⋯) ⟨k, hk⟩ = G.halfCode (G.cloudList v)[k]

The half-edge at a position is named by the count that reaches it.