Finite certificates for rotations of listed multigraphs

A certificate lists the successor of each of the 2m indexed darts. Dart 2i is the first end of listed edge i, and dart 2i+1 its second end. The checker uses bounded table lookup and at most 2m iterations for orbit membership, including singleton orbits. All labels and indices use binary encodings; no loop is funded by a vertex label or a supplied table entry.

The table must be a permutation, every endpoint must be declared, and the successor orbits must be exactly the endpoint fibers. Accepted certificates decode to the existing Graph.RotationSystem; conversely every rotation on a graph with declared endpoints has a certificate. Decoding is proof-only; the Boolean checker does not execute a choice operation.

verifyGenusZero additionally checks V+F=E+2 in each nonempty edge component, counting distinct endpoint vertices, indexed edges, and all face orbits. Isolated declared vertices use the separate point-component convention V=1,E=0,F=1; they contribute no dart orbit. No face is required to carry a constraint, and repeated vertices along face orbits are allowed.

This finite representation and its correctness proofs are original. They supply no geometric realization or planarity recognition theorem.

Main definitions

• Cslib.Complexity.Graph.RotationCertificate: binary successor table.
• Cslib.Complexity.Graph.RotationCertificate.verifyGenusZero: finite supplied-certificate check.
• Cslib.Complexity.Graph.RotationSystem.NumericalGenusZero: componentwise numerical predicate.

Main results

• Cslib.Complexity.Graph.RotationCertificate.decode_ofRotation: exact rotation recovery.
• Cslib.Complexity.Graph.RotationCertificate.verifyEuler_eq_true_iff: numerical correspondence.
• Cslib.Complexity.Graph.RotationCertificate.exists_bounded_certificate_iff: both directions with a quadratic certificate bit bound.

def Cslib.Complexity.Graph.Dart.index {G : Graph} (d : G.Dart) : ℕ

Binary index of a dart: edge position followed by its endpoint bit.

def Cslib.Complexity.Graph.Dart.indexEquiv (G : Graph) : G.Dart ≃ Fin (2 * G.edges.length)

Indexed darts are exactly the positions of the flattened endpoint list.

theorem Cslib.Complexity.Graph.Dart.vertex_index {G : Graph} (d : G.Dart) : G.incidenceVertices.getD d.index 0 = d.vertex

The code reads exactly the original dart endpoint.

structure Cslib.Complexity.Graph.RotationCertificate : Type

One binary successor index for each indexed edge end, in edge/end order.

• successor : List ℕ

  Successor table; its required length is twice the actual edge-list length.

@[instance_reducible]

instance Cslib.Complexity.Graph.instDecidableEqRotationCertificate : DecidableEq RotationCertificate

def Cslib.Complexity.Graph.instDecidableEqRotationCertificate.decEq (x✝ x✝¹ : RotationCertificate) : Decidable (x✝ = x✝¹)

def Cslib.Complexity.Graph.instReprRotationCertificate.repr : RotationCertificate → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.Graph.instReprRotationCertificate : Repr RotationCertificate

theorem Cslib.Complexity.Graph.encRotationCertificate_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : List ℕ) => { successor := p }) encRotationCertificateFields encRotationCertificate 1 1

theorem Cslib.Complexity.Graph.encRotationCertificate_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List ℕ} {T0 S0 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) T0 S0) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { successor := x0 x }) encIn encRotationCertificate (fun (x : γ) => T0 x) fun (x : γ) => S0 x

theorem Cslib.Complexity.Graph.encRotationCertificate_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → List ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { successor := x0 x }) encIn encRotationCertificate budget

theorem Cslib.Complexity.Graph.encRotationCertificate_successor_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → RotationCertificate} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encRotationCertificate → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).successor) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

theorem Cslib.Complexity.Graph.encRotationCertificate_successor_inO : Turing.MultiTapeTM.ComputableInO RotationCertificate.successor encRotationCertificate (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (fun (a : RotationCertificate) => (encRotationCertificate a).length) fun (a : RotationCertificate) => (encRotationCertificate a).length

def Cslib.Complexity.Graph.encRotationCertificate : RotationCertificate ↪ List Bool

A rotation certificate is its framed list of binary successor indices.

theorem Cslib.Complexity.Graph.encRotationCertificate_successor_deg : Turing.MultiTapeTM.ComputableInDegree RotationCertificate.successor encRotationCertificate (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) 1 1

@[reducible, inline]

abbrev Cslib.Complexity.Graph.encRotationCertificateFields : List ℕ ↪ List Bool

The tuple of the fields of encRotationCertificate.

theorem Cslib.Complexity.Graph.encRotationCertificate_successor_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → RotationCertificate} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encRotationCertificate S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).successor) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) S✝

theorem Cslib.Complexity.Graph.encRotationCertificate_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { successor := x0 x }) encIn encRotationCertificate

@[simp]

theorem Cslib.Complexity.Graph.encRotationCertificate_apply (a : RotationCertificate) : encRotationCertificate a = encRotationCertificateFields a.successor

theorem Cslib.Complexity.Graph.encRotationCertificate_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : RotationCertificate) => a.successor) encRotationCertificate encRotationCertificateFields 1 1

@[reducible, inline]

abbrev Cslib.Complexity.Graph.encGraphRotationCertificate : Graph × RotationCertificate ↪ List Bool

Graph, framed, followed by its successor certificate. Labels and indices are binary.

def Cslib.Complexity.Graph.RotationCertificate.walk (table : List ℕ) (steps start : ℕ) : ℕ

Total table iteration. Missing entries return zero, even for enormous binary indices.

def Cslib.Complexity.Graph.RotationCertificate.orbitBool (n : ℕ) (table : List ℕ) (i j : ℕ) : Bool

Orbit test with a clock funded by the actual number of darts.

def Cslib.Complexity.Graph.RotationCertificate.verifyRotation (G : Graph) (c : RotationCertificate) : Bool

All declared endpoints, exact table length, permutation, and exact endpoint fibers.

theorem Cslib.Complexity.Graph.RotationCertificate.length_of_verifyRotation {G : Graph} {c : RotationCertificate} (h : verifyRotation G c = true) : c.successor.length = 2 * G.edges.length

Every accepted raw rotation table has exactly one successor entry per indexed dart. Unlike length_ofRotation, this applies to supplied certificates without a generator premise.

theorem Cslib.Complexity.Graph.RotationCertificate.orbitBool_eq_true_iff {G : Graph} (f : Equiv.Perm G.Dart) (table : List ℕ) (ht : ∀ (d : G.Dart), table.getD d.index 0 = (f d).index) (d e : G.Dart) : orbitBool (2 * G.edges.length) table d.index e.index = true ↔ f.SameCycle d e

A bounded table orbit is the existing permutation's SameCycle, when its entries encode that permutation. The clock is the cardinality, rather than the permutation's order.

noncomputable def Cslib.Complexity.Graph.RotationCertificate.decode (G : Graph) (c : RotationCertificate) (h : verifyRotation G c = true) : G.RotationSystem

Decode an accepted finite table to the existing rotation-system structure. This operation is used in proofs; the native checker executes only finite list operations.

theorem Cslib.Complexity.Graph.RotationCertificate.index_decode_rotate {G : Graph} {c : RotationCertificate} (h : verifyRotation G c = true) (d : G.Dart) : ((decode G c h).rotate d).index = c.successor.getD d.index 0

The decoded successor is exactly the supplied table entry.

def Cslib.Complexity.Graph.RotationCertificate.ofRotation {G : Graph} (r : G.RotationSystem) : RotationCertificate

A table for an abstract rotation, in the canonical edge/end order.

@[simp]

theorem Cslib.Complexity.Graph.RotationCertificate.length_ofRotation {G : Graph} (r : G.RotationSystem) : (ofRotation r).successor.length = 2 * G.edges.length

The canonical table has exactly two entries per listed edge.

theorem Cslib.Complexity.Graph.RotationCertificate.getD_ofRotation {G : Graph} (r : G.RotationSystem) (d : G.Dart) : (ofRotation r).successor.getD d.index 0 = (r.rotate d).index

Reading the canonical table recovers the rotation.

theorem Cslib.Complexity.Graph.RotationCertificate.verifyRotation_ofRotation {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) : verifyRotation G (ofRotation r) = true

Every existing rotation has an accepted finite certificate when its endpoints are declared. No rotation is assumed to be geometrically planar.

theorem Cslib.Complexity.Graph.RotationCertificate.decode_ofRotation_rotate {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) : (decode G (ofRotation r) ⋯).rotate = r.rotate

Encoding and then decoding preserves the actual successor permutation.

theorem Cslib.Complexity.Graph.RotationCertificate.decode_ofRotation {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) : decode G (ofRotation r) ⋯ = r

Canonical table encoding and checked decoding recover the existing rotation structure.

theorem Cslib.Complexity.Graph.RotationCertificate.length_enc_ofRotation_le {G : Graph} (r : G.RotationSystem) : (encRotationCertificate (ofRotation r)).length ≤ 10 * ((encGraph G).length + 1) ^ 2

A coarse quadratic bit bound for the canonical certificate, including all framing. The bound depends on the encoded graph length, even for sparse, very large vertex labels.

def Cslib.Complexity.Graph.RotationCertificate.componentStep (G : Graph) (seen : List ℕ) : List ℕ

One breadth-first expansion, retaining the old list. Repetitions are harmless: the result is used only for membership, never as a vertex count.

def Cslib.Complexity.Graph.RotationCertificate.componentVertices (G : Graph) (root : ℕ) : List ℕ

Finite reachability from a declared root, with one iteration per declared vertex record.

def Cslib.Complexity.Graph.RotationCertificate.componentBool (G : Graph) (root v : ℕ) : Bool

Native component membership; no range up to a binary vertex label is constructed.

def Cslib.Complexity.Graph.RotationCertificate.SameComponent (G : Graph) (u v : ℕ) : Prop

Membership in the same connected component of the existing graph on declared vertices.

theorem Cslib.Complexity.Graph.RotationCertificate.SameComponent.refl {G : Graph} {v : ℕ} (hv : v ∈ G.vertices) : SameComponent G v v

A declared vertex is in its own component, including an isolated vertex.

theorem Cslib.Complexity.Graph.RotationCertificate.SameComponent.symm {G : Graph} {u v : ℕ} (h : SameComponent G u v) : SameComponent G v u

Component membership is symmetric.

theorem Cslib.Complexity.Graph.RotationCertificate.SameComponent.trans {G : Graph} {u v w : ℕ} (h : SameComponent G u v) (h' : SameComponent G v w) : SameComponent G u w

Component membership is transitive.

theorem Cslib.Complexity.Graph.RotationCertificate.componentBool_eq_true_iff {G : Graph} {root v : ℕ} (hr : root ∈ G.vertices) : componentBool G root v = true ↔ SameComponent G root v

The finite expansion agrees exactly with connectedness in the existing induced graph. The path bound is the number of declared vertices, including malformed duplicate records.

def Cslib.Complexity.Graph.RotationCertificate.reverseIndex (i : ℕ) : ℕ

Reverse a dart's endpoint bit without inspecting vertex labels.

theorem Cslib.Complexity.Graph.RotationCertificate.reverseIndex_index {G : Graph} (d : G.Dart) : reverseIndex d.index = d.reverse.index

Binary reversal agrees with reversal of the existing indexed dart.

def Cslib.Complexity.Graph.RotationCertificate.faceTable (G : Graph) (c : RotationCertificate) : List ℕ

The face successor table: reverse the edge, then look up the inverse rotation. idxOf returns the table length on failure, making this total on malformed certificates.

def Cslib.Complexity.Graph.RotationCertificate.faceRepBool (n : ℕ) (table : List ℕ) (i : ℕ) : Bool

Test that this dart is the least indexed member of its face orbit, including fixed points.

theorem Cslib.Complexity.Graph.RotationCertificate.index_decode_rotate_symm {G : Graph} {c : RotationCertificate} (h : verifyRotation G c = true) (d : G.Dart) : ((Equiv.symm (decode G c h).rotate) d).index = List.idxOf d.index c.successor

For any accepted raw table, its actual inverse rotation is exactly the bounded list search for the given dart index. Empty graphs have no dart premise to manufacture.

theorem Cslib.Complexity.Graph.RotationCertificate.getD_faceTable {G : Graph} {c : RotationCertificate} (h : verifyRotation G c = true) (d : G.Dart) : (faceTable G c).getD d.index 0 = ((decode G c h).faceNext d).index

The finite face table realizes exactly RotationSystem.faceNext.

def Cslib.Complexity.Graph.RotationCertificate.verifyEuler (G : Graph) (c : RotationCertificate) : Bool

Componentwise Euler test. Every declared root is checked separately. For a root with no incident dart, use the point-component convention V=1,E=0,F=1, not a dart orbit. For an edge component, count distinct vertices, listed edge positions, and every face orbit.

def Cslib.Complexity.Graph.RotationCertificate.verifyGenusZero (G : Graph) (c : RotationCertificate) : Bool

Full supplied-certificate checker: rotation validity and componentwise numerical Euler.

theorem Cslib.Complexity.Graph.RotationSystem.vertex_mem {G : Graph} (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : d.vertex ∈ G.vertices

Every dart endpoint is declared when all listed edge endpoints are declared.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_reverse {G : Graph} (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : RotationCertificate.SameComponent G d.vertex d.reverse.vertex

The two indexed ends of an edge belong to the same declared-vertex component, including when the edge is a loop. All listed endpoints must be declared.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_faceNext {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : RotationCertificate.SameComponent G d.vertex (r.faceNext d).vertex

A face successor stays in the same edge component.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_of_sameFace {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) {d e : G.Dart} (h : r.faceNext.SameCycle d e) : RotationCertificate.SameComponent G d.vertex e.vertex

All darts of each face orbit belong to one edge component. Thus componentwise face counts cannot split an orbit or transfer a face between disconnected edge components.

def Cslib.Complexity.Graph.RotationSystem.IsFaceRepresentative {G : Graph} (r : G.RotationSystem) (d : G.Dart) : Prop

The least indexed dart of a face. Fixed points qualify, so their faces are counted too.

noncomputable def Cslib.Complexity.Graph.RotationSystem.NumericalGenusZero {G : Graph} (r : G.RotationSystem) : Prop

Componentwise numerical genus zero. An edge component has V+F=E+2, with distinct endpoint vertices, indexed edge records and all face orbits. An isolated declared vertex is a point component with one conventional face and no dart. This is a numerical predicate on the existing rotations, not an equivalence to geometric planarity. In particular, geometric outer faces of disconnected drawings have not been identified with these componentwise faces.

theorem Cslib.Complexity.Graph.RotationSystem.existsUnique_faceRepresentative {G : Graph} (r : G.RotationSystem) (d : G.Dart) : ∃! e : G.Dart, r.faceNext.SameCycle d e ∧ r.IsFaceRepresentative e

Each face orbit has exactly one representative, including a one-dart fixed-point orbit.

theorem Cslib.Complexity.Graph.RotationCertificate.faceRepBool_eq_true_iff {G : Graph} {c : RotationCertificate} (h : verifyRotation G c = true) (d : G.Dart) : faceRepBool (2 * G.edges.length) (faceTable G c) d.index = true ↔ (decode G c h).IsFaceRepresentative d

The face representative test counts exactly the existing face orbits.

theorem Cslib.Complexity.Graph.RotationCertificate.verifyEuler_eq_true_iff {G : Graph} {c : RotationCertificate} (h : verifyRotation G c = true) : verifyEuler G c = true ↔ (decode G c h).NumericalGenusZero

The executable Euler check agrees with the explicit componentwise numerical predicate on the decoded existing rotation. No geometric correspondence is used.

theorem Cslib.Complexity.Graph.RotationCertificate.verifyGenusZero_eq_true_iff (G : Graph) (c : RotationCertificate) : verifyGenusZero G c = true ↔ ∃ (h : verifyRotation G c = true), (decode G c h).NumericalGenusZero

Exact soundness and completeness for a supplied certificate. Acceptance is equivalent to an actual rotation represented by the table and satisfying componentwise numerical Euler.

theorem Cslib.Complexity.Graph.RotationCertificate.exists_bounded_certificate_iff (G : Graph) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) : (∃ (r : G.RotationSystem), r.NumericalGenusZero) ↔ ∃ (c : RotationCertificate), (encRotationCertificate c).length ≤ 10 * ((encGraph G).length + 1) ^ 2 ∧ verifyGenusZero G c = true

Every numerical genus-zero rotation has a certificate within the explicit quadratic bit bound, and every accepted such certificate supplies an actual numerical genus-zero rotation.