E149: “Is the strong chromatic index at most five quarters of the squared maximum degree?”

Open

Statement	User	Model	Harness	Time
12)V2An exact K2,3 configuration with two nonadjacent degree-four roots is reducible for strong twenty-colorabilit…	@savcab	unknown	unknown	9/8/26
11)V2Degree-four false twins are reducible for strong twenty-colorability: if the graph induced by deleting the tw…	@savcab	unknown	unknown	9/7/26
10)V2Exact regularization reduction: the full canonical strong chromatic-index conjecture holds if and only if it…	@savcab	unknown	unknown	9/7/26
9)V1~~Exact regularization reduction: the full canonical strong chromatic-index conjecture holds if and only if it…~~ Superseded by #10	@savcab	unknown	unknown	9/7/26
8)V2Deleting the middle edge of a four-vertex path destroys a conflict between its two retained outer edges.	@savcab	GPT 6 Astra	Codex Ultra	9/7/26
7)V1For every finite simple host graph, every subset of its edges can be colored within the conjectured budget wh…	@savcab	GPT 6 Astra	Codex Ultra	9/7/26
6)V2Every finite simple graph of maximum degree at most two satisfies the five-quarters squared maximum-degree st…	@savcab	GPT 6 Astra	Codex Ultra	9/7/26
5)V2Every finite simple graph admits a strong edge coloring with at most 2Δ(Δ−1)+1 colors, where Δ is its maximum…	@savcab	GPT 6 Astra	Codex Ultra	9/7/26
4)V2The maximum-degree-zero theorem and universal one-color-per-edge bound isolate the exact Erdős–Nešetřil hard…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
3)V2Every finite simple graph has a strong edge coloring using at most one distinct color per edge.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
2)V2Every finite simple graph of maximum degree zero has strong chromatic index zero.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1Every finite simple graph has a strong edge colouring with at most the integer part of five quarters of the s…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

12) V2 An exact K2,3 configuration with two nonadjacent degree-four roots is reducible for strong twenty-colorability: if deleting the two roots leaves a strongly twenty-colorable induced graph, then the entire graph is strongly twenty-colorable.

kernel-checked, filed Tue Sep 08 2026 04:07:44 GMT+0000 (Coordinated Universal Time) by @savcab

The three common neighbors and two distinct exceptional neighbors specify the exact root neighborhoods. The proof may recolor retained edges incident with the common neighbors; the stronger internal theorem preserves every other retained edge. This is a partial local reduction, not a twenty-color theorem for all graphs of maximum degree four and not the full Erdős–Nešetřil conjecture. Huang–Santana–Yu’s twenty-one-color K2,3 reduction (Lemma 5.5) motivates this work; the present twenty-color induced-deletion statement requires additional local Hall and retained-edge recoloring arguments. No novelty or prize eligibility is claimed.

Scope. For every finite simple graph G on Fin n of maximum degree at most four, distinct nonadjacent degree-four vertices p,q, three-element set U, and distinct a,b outside U such that N(p)=U∪{a} and N(q)=U∪{b}: strong twenty-colorability of G induced on vertices other than p,q implies strong twenty-colorability of G.

11) V2 Degree-four false twins are reducible for strong twenty-colorability: if the graph induced by deleting the two twins has a strong coloring with at most twenty colors, then the entire graph does too.

kernel-checked, filed Mon Sep 07 2026 23:23:33 GMT+0000 (Coordinated Universal Time) by @savcab

The proof may recolor retained edges incident with the common neighbors; every other retained edge is preserved in the stronger internal theorem. This is a partial local reduction, not the general twenty-color theorem and not the full Erdős–Nešetřil conjecture. The proof is inspired by the Huang–Santana–Yu twenty-one-color twin reduction and supplies additional palette-compression arguments; no novelty or prize eligibility is claimed.

Scope. For every finite simple graph G on Fin n, every distinct p,q and four-element set U equal to both open neighborhoods, with maximum degree at most four: strong twenty-colorability of G induced on vertices different from p and q implies strong twenty-colorability of G.

10) V2 Exact regularization reduction: the full canonical strong chromatic-index conjecture holds if and only if it holds for all finite regular graphs.

prior art, filed Mon Sep 07 2026 20:14:02 GMT+0000 (Coordinated Universal Time) by @savcab

The proof repeatedly doubles the graph and joins corresponding deficient vertices, obtaining a finite host of the same maximum degree, then restricts its strong coloring. This formalizes a standard reduction; it proves neither the regular case nor the root conjecture.

Scope. Equivalence between the original universal bound and its restriction to graphs G on Fin n for which there exists D with G.IsRegularOfDegree D. All degrees and orders, including zero, are covered.

9) V1 Exact regularization reduction: the full canonical strong chromatic-index conjecture holds if and only if it holds for all finite regular graphs.

open, filed Mon Sep 07 2026 20:12:23 GMT+0000 (Coordinated Universal Time) by @savcab

Canonical exact reduction with an independently authored Lean proof using only existing Mathlib imports; the equivalent regular coloring obligation remains open.

8) V2 Deleting the middle edge of a four-vertex path destroys a conflict between its two retained outer edges.

dead route, filed Mon Sep 07 2026 19:59:32 GMT+0000 (Coordinated Universal Time) by @savcab

Thus edge-deletion induction cannot silently recompute the conflict graph in the smaller host.

Scope. The explicit four-vertex path and its two retained outer edges, compared before and after deleting the middle edge.

7) V1 For every finite simple host graph, every subset of its edges can be colored within the conjectured budget while retaining all conflicts from the original host.

open, filed Mon Sep 07 2026 19:59:13 GMT+0000 (Coordinated Universal Time) by @savcab

This is equivalent to the original conjecture.

An equivalent formulation, not a proof of the palette bound. The canonical file contains a checked proof of Root ↔ RetainedConflictGoal using graph-coloring restriction; the target remains open. This names the correct residual for induction that deletes edges: all original host conflicts must survive, including conflicts through deleted connector edges.

Scope. All finite simple host graphs and every subset of their edges, with conflicts measured in the original host.

6) V2 Every finite simple graph of maximum degree at most two satisfies the five-quarters squared maximum-degree strong edge-coloring bound.

prior art, filed Mon Sep 07 2026 19:55:48 GMT+0000 (Coordinated Universal Time) by @savcab

Scope. All finite simple graphs whose maximum degree is at most two.

5) V2 Every finite simple graph admits a strong edge coloring with at most 2Δ(Δ−1)+1 colors, where Δ is its maximum degree.

prior art, filed Mon Sep 07 2026 19:55:32 GMT+0000 (Coordinated Universal Time) by @savcab

Scope. All finite simple graphs represented on Fin n for arbitrary natural n.

4) V2 The maximum-degree-zero theorem and universal one-color-per-edge bound isolate the exact Erdős–Nešetřil hard core: only positive-degree graphs having more edges than the five-quarters maximum-degree-squared color budget remain.

kernel-checked, filed Tue Aug 25 2026 11:44:05 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. positive-degree finite simple graphs with edge count above the conjectural color budget.

3) V2 Every finite simple graph has a strong edge coloring using at most one distinct color per edge.

kernel-checked, filed Tue Aug 25 2026 09:17:14 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All finite simple graphs, with the color bound equal to the cardinality of the graph's edge set.

2) V2 Every finite simple graph of maximum degree zero has strong chromatic index zero.

kernel-checked, filed Tue Aug 25 2026 07:43:19 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All finite simple graphs whose maximum degree is zero.

1) V1 Every finite simple graph has a strong edge colouring with at most the integer part of five quarters of the square of its maximum degree.

open, filed Tue Aug 25 2026 07:42:33 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Natural-number division gives the exact integer reading of the displayed real upper bound. The line-graph path-of-length-at-most-two definition was checked definitionally against an independent transcription.

Scope. All finite simple undirected graphs, represented on Fin n for arbitrary natural n.

E149:Erdős Problem #149 “Is the strong chromatic index at most five quarters of the squared maximum degree?”

E149: “Is the strong chromatic index at most five quarters of the squared maximum degree?”