Two Colours on Original Multigraph Stars
Abstract
A finite loopless multigraph has two colours on every constrained star exactly when no all-constrained degree-two component has odd original edge count.
The finite types V and E index vertices and ORIGINAL edges. Two maps l,r : E -> V give the endpoints, with l(e) different from r(e) for every edge. The star of x is the finite set of edge IDs whose left or right endpoint is x. Distinct IDs with the same endpoint pair remain distinct; a parallel two-edge cycle has two edges. C is any finite set of constrained vertices, each of degree at least two. Mixed(l,r,c,x) means that two edges incident with x have different Bool colours. Reach is the equivalence closure generated by the original endpoint pairs. componentEdges(x) consists of the original IDs e with Reach(x,l(e)). OddComponent means that some component has all its vertices in C, all stars of cardinality two, and an odd number of original edges.
Theorem 1.1 (The Exact Existence and Obstruction Theorem).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/EdgeColouring/TwoColours.exists_iff_no_odd_component (✓ std3). ∎
Source. Repository-derived.
Commentary.
Minimize the number of monochromatic constrained stars over all edge colourings. Flipping an edge at a defect fixes that star. Minimality forces the other endpoint to become the unique replacement defect, preserving all other defects. A defect of degree at least three starts a finite path-extension contradiction: departed vertices retain opposite colours protected by used edges, while the initial vertex retains a third edge. Every extension reaches a fresh vertex, contradicting finiteness. Thus every possible surviving defect has degree two. Transport across the entire component shows that every vertex is constrained of degree two and the initial colouring has exactly one defect there. Counting incidences of each colour makes that component’s original edge count odd. Conversely, in an all-constrained degree-two component a successful colouring uses exactly one edge of each colour at every vertex. Double counting forces an even original edge count. These are unbounded proofs, with no supplied tour, colouring, path, or cut certificate.
The statement allows unconstrained vertices of any degree; it therefore includes the free-leaf convention and arbitrary isolated free vertices. It also includes empty edge sets, disconnected graphs and all parallel-edge multiplicities. No novelty in the graph theorem is claimed. The endpoint representation and defect-minimization derivation are repository mathematics; the motivating native incidence-two proof uses an elementary Euler-trail construction for the same lemma. A search of the pinned Mathlib Graph and Quiver interfaces found no supplier for this existence statement; SimpleGraph.Trails leaves its Euler-existence converse as a TODO.
In the incidence-two integer blocker argument, the dual graph has one edge for each used original coordinate and one star for each complete minimal Boolean row. With no adjacent original degree-two vertices, choose a triangle UVW and name its original edges e=UV, l=UW and r=VW, with U and V of degree at least three. the W-port split deletes only e, joins l and r to one new constrained degree-two vertex, and sends each other W-port to its own free leaf. The theorem then supplies both colours on every retained constrained star unless the exact exceptional odd component occurs. The new degree-two vertex forces l and r to have opposite colours; those same original IDs give both colours at W. The exceptional component instead yields the original alternating-star coefficient-one difference e_l-e_r. The port-split construction, its exceptional-component coefficient calculation, and the remaining complete Good/integral-blocker consumer are not formalized by this graph theorem. FullGroupGood, the unrestricted exact integral blocker and AM remain open.