Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

The hub and tail construction for consecutive cycle sums

Abstract

A hub joined to a short initial block makes arbitrary core subsets and consecutive tail prefixes connected, with at most k minus one added edges.

Definition 1.1 (Vertices selected by their labels).

Lean statement: D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.vertices

Formalization. D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.vertices (✓ std3).

Source. Repository-derived.

Commentary.

For a natural number n and a finite set S of natural labels, vertices n S consists of those v in Fin n for which v.val + 1 belongs to S.

Theorem 1.2 (Membership under label selection).

Lean statement: D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.mem_vertices

Proof. Machine-checked in Lean as D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.mem_vertices (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n, finite label set S and vertex v in Fin n, v belongs to vertices n S if and only if v.val + 1 belongs to S.

Theorem 1.3 (Label selection preserves sums).

Lean statement: D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.sum_vertices

Proof. Machine-checked in Lean as D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.sum_vertices (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n and finite set S of natural labels, if every x in S satisfies 1 ≤ x ≤ n, the sum of v.val + 1 over vertices n S equals the sum of x over S. Each positive bounded label has the unique vertex with value x minus one.

Definition 1.4 (Cycle with a hub).

Lean statement: D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.completion

Formalization. D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.completion (✓ std3).

Source. Repository-derived.

Commentary.

For natural n and k with n positive, completion n k is the supremum of cycleGraph n and the simple graph generated by the unordered edges joining vertex zero to a vertex v with 2 ≤ v.val ≤ k. Its vertices retain their original consecutive labels.

Theorem 1.5 (The original cycle is retained).

Lean statement: D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.cycle_le_completion

Proof. Machine-checked in Lean as D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.cycle_le_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n and k with n positive, cycleGraph n is a subgraph of completion n k.

Theorem 1.6 (The number of newly added edges).

Lean statement: D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.added_edges_le

Proof. Machine-checked in Lean as D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.added_edges_le (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n and k with n positive, the natural cardinality of the edge set of completion n k minus the edge set of cycleGraph n is at most k minus one. The difference is contained in the star edges, indexed by vertex values from two through k.

Theorem 1.7 (Lower-labelled predecessors give connectedness).

Lean statement: D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.connected_of_predecessor

Proof. Machine-checked in Lean as D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.connected_of_predecessor (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n, simple graph G on Fin n, finite vertex set C, root r in Fin n and proof that r belongs to C, suppose every v in C distinct from r has a vertex u in C with u.val < v.val and G.Adj u v. Then the subgraph of G induced by C is connected. Strong induction on the vertex value constructs a path from r to every vertex of C. The hub-tail and interval constructions use this same supplier. Applied with C equal to the full vertex set, it also supplies connectedness of the domination construction’s base graph through the induced-universe isomorphism.

Theorem 1.8 (Core subsets with a tail prefix).

Lean statement: D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.hub_tail_connected

Proof. Machine-checked in Lean as D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.hub_tail_connected (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let n be positive and let k and j satisfy k < n and k ≤ j ≤ n. For every finite set S of natural labels, if every x in S lies between two and k, the subgraph of completion n k induced by vertices with labels in {1} ∪ S ∪ {k + 1, …, j} is connected. Core vertices and the first tail vertex are adjacent to the hub; every later tail vertex has its predecessor in the set.

Theorem 1.9 (Consecutive labels induce a connected graph).

Lean statement: D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.interval_connected

Proof. Machine-checked in Lean as D5/S3/Combinatorics/CycleSums/ConsecutiveCycleSumsGraph.interval_connected (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n, k, l and j with n positive and 1 ≤ l ≤ j ≤ n, the subgraph of completion n k induced by vertices with labels from l through j is connected. Successive labels are adjacent along the original cycle path.

References