Lax Lean Archive

Explicit Zig-Zag Family and Path Replacement

Lax920634.ZigZagConstruction · concepts/Lax920634/ZigZagConstruction.lean · lax-920634

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Starting with the fixed powered seed of degree DD, square it. Repeatedly square the current graph and take its zig-zag product with the same seed. The level-kk graph has degree d=D2d=D^2 and (D4)k+1(D^4)^{k+1} vertices. Replace every vertex by a path of dd ports to obtain the subcubic graph HkH_k on Nk=d(D4)k+1N_k=d(D^4)^{k+1} vertices.

    The rotation query below gives the construction directly in integer arithmetic. Each recursive level makes two queries at the preceding level and two queries to the fixed seed. Thus the number of fixed-seed calls is 2k+2−22^{k+2}-2, bounded by a constant times NkN_k. Each integer manipulated has O(log⁡Nk)O(\log N_k) bits. Enumerating all edges is consequently polynomial in NkN_k. The fixed seed search has an enormous constant cost.

    Concept map
    4 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax920634.SeedRotation
    2import Lax920634.EdgeExpansion
    3
    4/-!
    5---
    6title: Explicit Zig-Zag Family and Path Replacement
    7type: definition
    8---
    9Starting with the fixed powered seed of degree DD, square it. Repeatedly
    10square the current graph and take its zig-zag product with the same seed.
    11The level-kk graph has degree d=D2d=D^2 and (D4)k+1(D^4)^{k+1} vertices.
    12Replace every vertex by a path of dd ports to obtain the subcubic graph
    13HkH_k on Nk=d(D4)k+1N_k=d(D^4)^{k+1} vertices.
    14
    15The rotation query below gives the construction directly in integer
    16arithmetic. Each recursive level makes two queries at the preceding level
    17and two queries to the fixed seed. Thus the number of fixed-seed calls is
    182k+2−22^{k+2}-2, bounded by a constant times NkN_k. Each integer manipulated has
    19O(log⁡Nk)O(\log N_k) bits. Enumerating all edges is consequently polynomial in
    20NkN_k. The fixed seed search has an enormous constant cost.
    21
    22# Formalization notes
    23
    24The construction uses numerical vertex labels and the concrete deterministic
    25seed scan. The graph is the simple undirected closure of the generated path
    26and matching edges. The proof connects this executable recurrence to the
    27numbered zig-zag tower and verifies every returned matching endpoint's bounds.
    28-/
    29
    30namespace Lax920634.ZigZagConstruction
    31
    32open SeedSearch
    33
    34/-- The fixed degree of each regular graph in the tower. -/
    35def degree : ℕ := seedDegree ^ 2
    36
    37/-- The number of vertices in the regular graph at a given level. -/
    38def baseOrder (k : ℕ) : ℕ := (seedDegree ^ 4) ^ (k + 1)
    39
    40/-- The number of vertices after path replacement at a given level. -/
    41def order (k : ℕ) : ℕ := baseOrder k * degree
    42
    43/-- A total numerical query to the fixed seed's edge rotation. -/
    44def seedValue (p : ℕ × ℕ) : ℕ × ℕ :=
    45 if h : p.1 < seedOrder ∧ p.2 < seedDegree then
    46 let r := SeedRotation.rotation (⟨p.1, h.1⟩, ⟨p.2, h.2⟩)
    47 (r.1.val, r.2.val)
    48 else (0, 0)
    49
    50/-- The regular tower's rotation, computed by squaring and zig-zag steps. -/
    51def rotation : ℕ → ℕ × ℕ → ℕ × ℕ
    52 | 0, (v, i) =>
    53 let p₀ := seedValue (v, i / seedDegree)
    54 let p₁ := seedValue (p₀.1, i % seedDegree)
    55 (p₁.1, p₀.2 + seedDegree * p₁.2)
    56 | k + 1, (v, i) =>
    57 let p := seedValue (v % seedDegree ^ 4, i / seedDegree)
    58 let q₀ := rotation k (v / seedDegree ^ 4, p.1 / degree)
    59 let q₁ := rotation k (q₀.1, p.1 % degree)
    60 let r := seedValue (q₀.2 + degree * q₁.2, i % seedDegree)
    61 (r.1 + seedDegree ^ 4 * q₁.1, p.2 + seedDegree * r.2)
    62
    63/-- The matching endpoint of a port, in the canonical vertex numbering. -/
    64def matchingNeighbor (k v : ℕ) : ℕ :=
    65 let r := rotation k (v / degree, v % degree)
    66 r.2 + degree * r.1
    67
    68/-- The subcubic graph defined by the explicit tower and path-edge formulas. -/
    69def graph (k : ℕ) : SimpleGraph (Fin (order k)) :=
    70 SimpleGraph.fromRel (fun u v =>
    71 (u.val / degree = v.val / degree ∧ u.val + 1 = v.val) ∨
    72 v.val = matchingNeighbor k u.val)
    73
    74/-- The candidate neighbors, omitting nonexistent endpoint edges of a path. -/
    75def neighbors (k v : ℕ) : List ℕ :=
    76 (if 0 < v % degree then [v - 1] else []) ++
    77 (if v % degree + 1 < degree then [v + 1] else []) ++
    78 [matchingNeighbor k v]
    79
    80end Lax920634.ZigZagConstruction
    81
    Formalization notes

    The construction uses numerical vertex labels and the concrete deterministic seed scan. The graph is the simple undirected closure of the generated path and matching edges. The proof connects this executable recurrence to the numbered zig-zag tower and verifies every returned matching endpoint's bounds.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…