Commit Graph

243 Commits

Author SHA1 Message Date
didericis 1556109dda coloring_nested_tire_graphs: introduce boundary cut tire T_∂
NEW NOTE: boundary_cut_tire.tex (3 pages)
NEW SCRIPT: experiments/boundary_cut_tire.py

CONCEPT: T_∂^(i) per side i = the unique low-side face of H_1
(= face containing all pendants) treated as a virtual root tire.
  - Cycle = boundary walk of f_∂ (depth-1 edges)
  - OUT pendants = depth-0 cut edges in f_∂'s interior
  - IN pendants = depth-2 edges at boundary vertices going into
    adjacent high-side faces

T_∂ adjoins the high-side forest as a boundary node: not parent
or child geometrically, but shares edges with adjacent high-side
tires (depth-1 boundary edges, depth-2 in-pendants).

The extended chain DP includes T_∂ and uses edge-sharing
compatibility with adjacent high-side tires.

EMPIRICAL RESULTS (vs. ground truth from brute-force enumeration):

Dodecahedron:
  - cut #0 side 0 (|S|=4, H_1 = tree): MATCH 9=9 ✓
    [previously high-side DP gave 0, framework failed]
  - cut #3 side 1 (|S|=4): MATCH 9=9 ✓
  - cut #4 side 0 (|S|=4): MATCH 9=9 ✓
  - HM_0 cut #0 side 0 (|S|=4): MATCH 9=9 ✓

  Thicker sides: |R_dp| < |R_ground| (DP over-restricts).
  This is a separate issue (probably heuristic parent-finding
  or shared-edge logic when multiple high-side tires interact),
  not the coverage gap.

  Some cuts have side too large for brute-force enumeration in
  T_∂ (n_edges > 18 limit), marked 'bdy too big'.

KEY WIN: the coverage gap is closed for the thin-side case where
H_d is a tree. The boundary cut tire converts these from
"framework gives R=0" to "framework gives R = ground truth."

NOT YET CLOSED:
  - Thicker sides where DP under-counts vs ground truth
    (different sets, similar cardinality sometimes)
  - Branched per-tire half (T_∂'s cycle can traverse edges twice)
  - Strong per-tire extendibility conjecture

But the framework now has principled coverage on ALL sides,
not just those with cycles in H_1.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 23:17:28 -04:00
didericis 00358d00ed coloring_nested_tire_graphs: rebuild cut_depth_label PDF artifacts
Stale build artifacts from latexmk rebuild — no source changes.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 23:00:59 -04:00
didericis 84600dadd3 coloring_nested_tire_graphs: joint-projection chain DP + tree-H_d coverage gap
NEW: chain_dp_joint.py — chain DP tracking full per-tire colorings,
edge-tuple-based parent/child sharing, and ground-truth comparison
against brute-force G' edge-coloring enumeration.

KEY EMPIRICAL FINDING (4th issue in chain_half_analysis):
When H_d is a tree (no internal cycles), the high-side cut tire
forest is EMPTY.  The single H_d face is forced (by the level-set
lemma) to be entirely low-side or high-side; for a tree containing
the pendants, it's low-side.  Hence high-side forest has 0 tires.

This happens at dodecahedron cut #0 side 0 (|S_0|=4):
  - depths {0: 2, 1: 3}, |H|=6, |E(H)|=5
  - H_1 is a tree, 1 face of length 6 (= low-side)
  - No high-side cut tires
  - DP gives R_dp=0, but ground truth R=36

DP correctly produces non-empty output on side 1 (where H_1 has
2 faces, one high-side), but the high-side framework's coverage
is incomplete for thin (small |S_i|) cuts.

This is a STRUCTURAL gap, not a code bug.  The path forward
suggested in chain_half_analysis.tex: introduce a "boundary cut
tire" T_0 representing the low-side face + its pendants, so the
chain DP runs from leaves through T_0 to the cut.

Compounding with prior gaps:
  (1) cut tires aren't always spoke-only (branched H_d faces)
  (2) OUT-only projection loses S_3 orbit
  (3) heuristic parent-finding (vertex overlap)
  (4) tree H_d → empty high-side forest (this commit)

Net: the loose conjecture's chain half is genuinely open and
requires framework extension before the DP can be tested cleanly.
S_3 equivariance and high-side forest structure are the proven
pieces.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 22:58:21 -04:00
didericis 203b005336 coloring_nested_tire_graphs: chain half analysis + tree DP empirical test
NEW NOTE: chain_half_analysis.tex (4 pages).

Formulates the chain half of the loose conjecture as a tree DP
over the cut tire forest, identifies what's proven vs. open:

PROVEN
- Tree structure (high-side forest): from
  cut_tire_tree_structure.tex
- S_3-equivariance of the DP: trivial Lemma in this note
- Per-tire half for spoke-only cut tires (n ≥ 3): Prop 1.13

OPEN / GAPS DISCOVERED
1. Cut tires are NOT in general spoke-only. H_d can have degree-3
   vertices (= branch points), making face boundaries non-simple
   cycles.  Dodecahedron 6-edge cut yields H_1 with one face of
   length 20 over only 11 distinct vertices.  Prop 1.13's count
   2^n + 2(-1)^n applies only to spoke-only tires.

2. OUT-only projection loses S_3 orbit info.  The per-tire half
   guarantees a full S_3 orbit on the JOINT (in + out) projection,
   but restricting to OUT spokes can collapse to |A|=3 (constant
   tuples). Empirically observed ~20% of the time on test cases.
   Correct DP must track joint projection (analog of
   tire_fiber_step2.tex's joint-support tracking).

3. Non-emptiness preservation through the DP is the genuine open
   piece (Conj. in this note + Strong per-tire extendibility).

EMPIRICAL TESTS
- chain_dp_test.py: simple cycle DP (assumes spoke-only).
- chain_dp_general.py: handles branched faces via brute-force
  3-edge-coloring enumeration (cut off at 12 edges/tire for
  tractability).
- chain_dp_debug.py: diagnostic for inspecting H_d face structure.

The general test reveals all three gaps above when run on
Dodecahedron + HM #0.  Cross-cut R_0 ∩ R_1 should be non-empty
for both (they are 3-edge-colorable), but the heuristic
parent-finding plus OUT-only projection produce false negatives.

Status table at end of note summarizes what's needed to close.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 22:49:20 -04:00
didericis 415c33cfc3 coloring_nested_tire_graphs: rigorous proof of cut tire forest proposition (high-side refinement)
Replaces the informal Stage 2 argument with a rigorous one,
achieved by refining the proposition to high-side faces only.

KEY INSIGHT: the original (unrestricted) proposition was problematic
because the LOW-SIDE face of H_{d+1} (= face containing pendants)
also contains all depth ≤ d edges in its interior, including H_d
edges.  Hence low-side H_{d+1} faces span multiple H_d faces.

The fix: restrict to HIGH-SIDE faces only.

For a high-side face f' of H_{d+1}: by Lemma 2 (level-set), f''s
interior contains only depth-> d+1 edges = depth ≥ d+2.  Since
depth-d edges are NOT in this range, no H_d edge sits inside f'.
Therefore f' is contained in a unique H_d face (by partition).
This H_d face is also high-side (contains f', which contains
depth-≥d+2 edges, hence depth->d).

Result: high-side cut tires form a forest, rigorously.  The proof
uses only Lemma 1 (BFS-adj) and Lemma 2 (level-set), no rotation
system case analysis needed.

Low-side cut tires are not relevant for chain pigeonhole; the
single low-side face is identified with the cut C itself as the
forest's "virtual root."

Note grows to 5 pages.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 22:32:29 -04:00
didericis 0cb0137a75 coloring_nested_tire_graphs: fix \newtheorem{lem} preamble for the proof lemmas
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 22:24:54 -04:00
didericis 410c2a1b35 coloring_nested_tire_graphs: detailed proof of the cut tire forest proposition
Replaces the earlier sketch with a more detailed two-stage proof:

Stage 1: BFS level-set lemma.
  Lemma (BFS-adj): adjacent edges in line graph differ in depth by
    at most 1.  Proof: BFS-distance property.
  Lemma (level-set): every face of H_d contains only edges of depth
    <d, or only edges of depth >d.  Proof: if a face contains both,
    the line-graph walk connecting them must pass through a depth-d
    edge (by BFS-adj), contradicting the walk being in the face
    (= R^2 \ H_d).

Stage 2: faces of H_{d+1} embed in faces of H_d.
  Key claim: no H_d edge sits strictly inside any face of H_{d+1}.
  Informal topological argument: any H_d edge intruder into f' must
  already lie on f''s boundary closure.

Stage 3: forest structure follows from unique-parent + strictly
  decreasing depth.

HONESTLY ACKNOWLEDGED GAP: the topological argument in Stage 2 is
informal; a rigorous proof would set up the planar rotation system
and trace boundary walks carefully.  Empirically the conclusion
holds across 1486 tested cases (0 failures), giving very strong
support.

Note grows to 5 pages.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 22:24:29 -04:00
didericis 57eccad49c coloring_nested_tire_graphs: tree structure sweep on minimum-counterexample-eligible graphs
Strictly tests the cut-tire forest property on cubic plane graphs
whose primal triangulation is internally 6-connected (= eligible
to be a minimum counterexample to the 4CT, per Birkhoff 1913).

Verified internal 6-connectivity of two primal triangulations
(exhaustive check over all 5-vertex subsets):

  - Icosahedron (12v, 5-regular): YES, internally 6-connected.
    Dual = Dodecahedron.
  - Pentakis dodecahedron (32v, min deg 5, max deg 6):
    YES, internally 6-connected.  Dual = BuckyBall.

Tree structure sweep on the corresponding duals:
  - Dodecahedron: 45 cuts, 45/45 produce trees on both sides.
  - BuckyBall (60v cubic plane): 60 cuts, 60/60 produce trees.
  - TruncatedTet (12v): 2 cuts, 2/2 produce trees.

105/105 cuts on minimum-counterexample-eligible duals produced
trees on both sides. 0 failures.

(Tutte graph: ran out of timeout enumerating its 6-edge cuts;
skipped from final tally.)

This is the most direct evidence for Proposition (cut tires form a
forest): the tree structure holds on the actual Birkhoff-eligible
graphs.

Files:
  experiments/eligible_sweep.py
  experiments/eligible_sweep_data.txt
  notes/cut_tire_tree_structure.tex (updated)

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 22:15:10 -04:00
didericis c98a01b7f9 coloring_nested_tire_graphs: broader tree-structure sweep on cut tires (0 failures across 1486 tests)
Adds tree_structure_sweep.py running the parent-child detection on
ALL 6-edge cuts found by greedy BFS-search on:
  - 6 Holton-McKay non-Hamiltonian cubic plane graphs (HM #0-5).
  - Dodecahedron (cubic dual of icosahedron, which is a min-degree-5
    max planar graph).

Total 743 distinct 6-edge cuts × 2 sides each = 1486 tests.
Total cut tires examined: 11,477.
Tree-structure failures (cycles in parent relation): 0.

Per-graph cut counts:
  HM #0: 128 cuts (all trees both sides)
  HM #1: 127, HM #2: 122, HM #3: 123, HM #4: 101, HM #5: 97
  Dodecahedron: 45 cuts (all trees both sides)

NOTE on the user's request: strictly "min-deg-5 with vertex-conn-6"
maximal planar graphs are incompatible (max planar avg deg < 6 ⇒
some vertex has degree ≤ 5 ⇒ vertex conn ≤ 5).  Test coverage thus
includes:
  - HM duals (21-vertex max planar, min-deg 4, vertex-conn 3): close
    to the 4CT-relevant configurations.
  - Icosahedron (12-vertex 5-regular, vertex-conn 5): min-deg 5
    case.

Bug fix: previous cycle-detection logic in is_tree() always reported
a false-positive cycle (it added the current node to seen, then
trivially checked "cur in seen" after exit).  Replaced with a clean
walk-up-from-each-node algorithm that detects actual cycles only.

Adds:
  experiments/tree_structure_sweep.py
  experiments/tree_structure_sweep_data.txt

Updates notes/cut_tire_tree_structure.tex with broader sweep table
and totals.  Note grows to 4 pages.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 22:01:24 -04:00
didericis 8f0245aa3d coloring_nested_tire_graphs: cut tires form a tree (forest) under depth nesting
User observation: the cut tires can at most have a tree structure.
This is correct: each face of H_{d+1} lies inside exactly one face
of H_d in the planar embedding, giving a parent-child relation that
is a forest (rooted at depth-1 cut tires).

PROPOSITION: parent(T_{d+1}^{(f')}) = T_d^{(f)} where f is the
unique face of H_d containing f' in its interior.  Well-defined and
unique because H_d's faces partition the plane minus H_d's edges.

CONSEQUENCE FOR CHAIN HALF: chain pigeonhole reduces to a tree-DP
problem.  Process tires bottom-up from leaves; at each node, combine
with children via the in-spoke ↔ face-boundary-edge bijection;
at the root, R_i is the projection.  Tree DP is well-understood;
counterexamples (if any) must come from tree-DP failures, which is
much narrower than general-graph compatibility.

EMPIRICAL CHECK on G'_1 of HM#0:
  Root (1, 0): |f|=12, no children (outer shell).
  Root (1, 1): |f|=4, deep substructure all the way to depth 7
    with single chain of children.
EMPIRICAL CHECK on G'_0:
  Root (1, 0): |f|=9, one depth-2 child.
  Root (1, 1): |f|=9, no children.

In both cases the structure is a tree (= 2-root forest).

CAVEATS:
- The empirical parent test used a vertex-sharing heuristic that
  gives ambiguous candidates in some cases (8 ambiguous in G'_1).
  A rigorous test would use point-in-region containment via the
  planar embedding's face structure.
- The proposition itself is uncontested; the ambiguity is just an
  artifact of the empirical detection.

NEXT STEPS:
1. Prove the proposition rigorously via point-in-region.
2. Implement tree DP on the cut tire forest.
3. Bound |R_i| as a function of tree size.

Note: cut_tire_tree_structure.tex (4 pages).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 18:17:25 -04:00
didericis 9e1ce4e51c coloring_nested_tire_graphs: refresh cut_tire_chain_pigeonhole.log
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 16:52:50 -04:00
didericis 902db37b50 coloring_nested_tire_graphs: broader empirical sweep of loose conjecture (k>=2 form)
Adopts the k>=2 refinement of the loose chain pigeonhole conjecture
(per loose_conjecture_counterexamples.tex) and runs a broader sweep:

  - All 6 Holton-McKay non-Hamiltonian 38-vertex cubic plane graphs.
  - 3 candidate matching 6-edge cuts per graph (greedy search,
    preferring matching cuts then balance).
  - Both sides of each cut.
  - All depths d >= 1.
  - Brute-force enumerate proper edge 3-colorings (skipping cut
    tires with > 14 edges due to runtime).

Results:
  - 287 total cut tires examined.
  - 154 with k >= 2 in/out spokes.
  - 107 verifiable (≤ 14 edges).
  - ALL 107 passed: |π(T)| >= 6 with at least one full S_3-orbit.
  - 0 counterexamples found.

This is strong empirical support for the k>=2 form of the loose
conjecture's per-tire half.

The cut_depth_label note (now 7 pages) is updated with:
  - k >= 2 restriction in the conjecture statement.
  - Restriction rationale (k=1 trivially excluded).
  - Status: empirical sweep + provable spoke-only case.

Files:
  experiments/loose_conjecture_sweep.py
  experiments/loose_conjecture_sweep_data.txt
  notes/cut_depth_label.tex (updated)

Next step: the per-tire half is essentially provable for spoke-only
cut tires via Prop 1.13. The chain half remains the genuinely open
piece.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 16:48:54 -04:00
didericis 6093b8cce3 coloring_nested_tire_graphs: counterexamples to the loose conjecture as stated
Before attempting to prove the loose chain pigeonhole conjecture
("|π(T)| ≥ 6" for every non-trivial cut tire), looked for
counterexamples and found TWO in the existing empirical data:

  (d, face) = (1, 1): 1 out spoke, |π(T)| = 3, orbit size [3].
  (d, face) = (4, 0): 1 out spoke, |π(T)| = 3, orbit size [3].

Reason: a cut tire with exactly k = 1 in/out spoke has σ ∈ {1,2,3}.
S_3 acts with stabilizer of size 2 on any single-color σ, so the
orbit has size 6/2 = 3, never 6. The "|π(T)| ≥ 6" claim is
automatically false for k = 1 tires.

For k ≥ 2: σ can use 1 color (size-3 orbit) or ≥ 2 colors
(size-6 orbit). |π(T)| ≥ 6 requires at least one multi-color σ to
extend, which is not automatic but typically holds.

Three refined conjectures proposed:

  1. Restrict to k ≥ 2 spokes (avoids the trivial counterexample).
  2. Weaken to "non-empty and S_3-closed" (very weak; needs the
     chain composition to preserve non-emptiness).
  3. Just describe orbit sizes 3 or 6 (no useful claim).

The two found counterexamples are at "side" faces in the chain;
they don't break the bottom-line chain pigeonhole because the main
chain runs through larger faces.

To find harder counterexamples: look for k ≥ 2 cut tires whose face
boundary forces all spoke colors equal (= |π(T)| = 3 with k ≥ 2).
Such examples might exist but weren't found in the current data.

Recommended next step: restrict the conjecture to k ≥ 2 and re-run
the empirical sweep.

Note: loose_conjecture_counterexamples.tex (3 pages).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 16:24:19 -04:00
didericis e173b1d2d4 coloring_nested_tire_graphs: add looser chain-pigeonhole conjecture to cut_depth_label
Adds a "Looser chain pigeonhole hypothesis" section to
cut_depth_label.tex, between Cut tires and the
"Connection to chain pigeonhole" section.

The conjecture says: for every non-trivial cut tire T, the joint
projection π(T) is non-empty, S_3-closed, and contains at least
one full S_3-orbit (so |π(T)| ≥ 6).  Chain composition through
T_1 → T_2 → ... preserves S_3-symmetry, so R_i contains a full
S_3-orbit, and R_0 ∩ R_1 contains a common orbit, contradicting G'
being a counterexample.

Status:
  - Per-tire half: provable via Prop 1.13 of paper.tex (2^n + 2(-1)^n
    colorings) + S_3-equivariance.
  - Chain half: open. Requires showing per-tire S_3-orbit structure
    composes coherently through the depth chain.

Weaker than the rainbow / König-lift conjectures (no requirement on
specific face boundary structure), with stronger empirical support
across all cut tires tested.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 16:15:56 -04:00
didericis 702cbcecf7 coloring_nested_tire_graphs: empirical test of rainbow + König-lift on cut tires
For each cut tire on G'_1 of Holton-McKay #0 (HM cut: |S|=10,
matching 6-cut), brute-force enumerate proper edge 3-colorings,
compute the joint (σ_out, σ_in) projection, and check S_3-closure
and orbit decomposition.

Results (8 cut tires analyzed, 2 too big or trivial):

  d  face  |f|  out  in  |E|  #col  |π|  S3-cl  orbit sizes
  1   0    12    5   0   17   96   93   yes    [3, 6^15]
  1   1     4    1   0    5    6    3   yes    [3]
  2   0     7    4   3   14  126  126   yes    [6^21]
  2   1     7    4   3   14  126  126   yes    [6^21]
  3   0-2   2    0   0    2    3    1   yes    [1]
  4   0     4    1   0    5    6    3   yes    [3]
  4   1     8    2   1   11   24   21   yes    [3, 6^3]
  5   1     2    0   0    2    3    1   yes    [1]
  6   0    12    3   2   17   96   93   yes    [3, 6^15]
  7   0     2    0   0    2    3    1   yes    [1]

Findings:

  1. S_3-closure is universal (structural, expected).
  2. Orbit sizes are always 3 (constant) or 6 (generic).
  3. Non-trivial cut tires have rich projections (e.g. d=2 has
     21 size-6 orbits = 126 elements; d=6 has 16 orbits).

Neither conjecture is DIRECTLY testable on this example:

  - Rainbow conjecture requires antipodal-chord SP face boundary
    structure. Our cut tires' face boundaries don't naturally have
    this shape.

  - König-lift conjecture requires both sides give γ-face partitions
    on a shared γ. Cut tires at consecutive depths share data via
    in-spoke ↔ face-boundary-edge bijection, not via γ-face
    partitions.

What CAN be observed: cut tire projections are LARGE and S_3-
symmetric (substantially looser than the rainbow case's 36-element
prediction). A "loose conjecture" would say π(T) ≥ c · 6 with c
depending only on |E(T)|, derivable from Prop 1.13 in paper.tex.

Files:
  experiments/cut_tire_test.py
  notes/cut_tire_conjecture_tests.tex (3 pages)

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 16:09:05 -04:00
didericis 52a1608580 coloring_nested_tire_graphs: fix unicode arrows in cut_tire_chain_pigeonhole
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 16:00:30 -04:00
didericis 7cd1f0d08d coloring_nested_tire_graphs: chain pigeonhole on pendant-redefined cut tires
New note cut_tire_chain_pigeonhole.tex (4 pages) examining what
chain pigeonhole looks like under the redefined cut tire (face
boundary + labelled pendants).

KEY CHANGE: each cut tire is now structurally isomorphic to a partial
tire dual D(T), so all results from paper.tex / rainbow_proof.tex /
worst_case_proof_sketch.tex / k9_surviving_partitions.tex transfer
directly without re-derivation.

ARGUMENT SHAPE:
  Setup: min counterexample G', 6-edge cut, depth labelling, cut
  tires at each depth.

  Reduction: minimality ⇒ G'_i 3-edge-colorable ⇒ boundary
  configurations σ_0, σ_1.

  Layered: σ_i = π_out({T_1^{(i, f)}}). Chain compatibility:
  out spoke of T_d ↔ face boundary edge of T_{d-1} via the
  parent-graph correspondence.

  Pigeonhole: if at each layer the projection support contains
  S_3-symmetric structure, the chain propagates and forces
  R_0 ∩ R_1 ≠ ∅.

WHAT'S NEW UNDER THE REDEFINITION:
  1. Direct result transfer: cut tires LITERALLY are partial tire
     duals; no translation overhead.
  2. Cubicity restored: face-boundary vertices have degree 3 in the
     cut tire (degree 2 in H_d + 1 pendant).
  3. Combinatorial rigidity: cut tire data = face + degree-2 boundary
     vertices + in/out classification.

WHAT STAYS OPEN:
  (a) Chain pigeonhole at each layer: same conjectures (rainbow,
      König-lift) gate the argument.
  (b) Chain well-definedness: trivial H_d faces (length 2),
      degree-> 2 boundary vertices not getting pendants.
  (c) Depth-by-depth variability: no uniform bound on |π_out|
      across depths.

ASSESSMENT: strict improvement over the previous cut tire definition
(no transfer overhead, cubicity restored), but the hard step
remains the same as in the partial-tire-dual framework.

Concrete next step: cut-tire analogue of tire_fiber_step2 — for
each Holton-McKay graph, build cut tire chains on both sides of a
6-cut and check R_0 ∩ R_1 empirically.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 16:00:15 -04:00
didericis cb6a79f799 coloring_nested_tire_graphs: redefine cut tire bullet 2 as labelled pendants
Per user spec: instead of including the actual depth-(d±1) edges
incident to the face boundary, redefine the cut tire as:

  - Face boundary walk of f (depth-d edges in H_d).
  - For each vertex v on the boundary walk with degree-2 in H_d:
    add a fresh vertex n_v and fresh edge {v, n_v}, labelled
    "out spoke" if v has an incident depth-(d-1) edge in G'_i,
    "in spoke"  if v has an incident depth-(d+1) edge.

Result: each cut tire is intrinsically "cycle (or closed walk) +
labelled pendants," structurally isomorphic to the partial tire
dual D(T) from paper.tex.  Pendants ↔ D(T)'s leaves, face boundary
↔ T'_ann.

This means propositions about D(T) (chromatic polynomial counts,
S_3-orbit structure, rainbow conjecture, etc.) apply verbatim to
each cut tire.

Updates:
- notes/cut_depth_label.tex: Definition rewritten, structural
  remark added, table of spoke counts updated to match new defn.
- experiments/cut_tire.py: cut_tire_at() now computes labelled
  pendants instead of incident edges; draw_cut_tire renders
  pendant vertices (orange squares for out, green squares for in)
  with edges offset toward parent-graph neighbor.
- notes/fig_cut_tire.png: regenerated.

Note grows to 6 pages.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 15:56:26 -04:00
didericis a21aff7f65 coloring_nested_tire_graphs: remove cut_tire_chain_pigeonhole note (per user)
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 15:48:40 -04:00
didericis 96102e6d03 coloring_nested_tire_graphs: examine chain pigeonhole on cut tires
New note cut_tire_chain_pigeonhole.tex (3 pages) walking through the
chain pigeonhole argument applied to the cut-tire framework:

Setup: minimum counterexample G' to 4CT, 6-edge cut splits into
G'_0, G'_1, depth labelling gives chains of cut tires on each side.

Argument shape:
  (1) Minimality ⇒ both G'_i have proper 3-edge-colorings.
  (2) Restrict to depth-0 pendants → boundary configurations σ_0, σ_1.
  (3) Glue iff σ_0 = σ_1; counterexample ⇒ no such matching.
  (4) Layered description: each cut tire has inner/outer projection
      constraints; adjacent tires share layers (outer of T_d =
      inner of T_{d+1}).
  (5) Chain pigeonhole: if each π_in is "large enough,"
      R_0 ∩ R_1 ≠ ∅, contradiction.

What this needs to be a proof:
  (a) Chain well-definedness: each H_d has ≥ 1 face, adjacencies
      clean, no degenerate cases.
  (b) Quantitative chain pigeonhole at each layer (= the rainbow
      conjecture or König-lift conjecture from existing notes).
  (c) Cut-tire-specific issues: H_d not cubic, face boundaries may
      not be simple cycles, transfer of primal-tire results requires
      verification.

Empirical chain on G'_1 of Holton-McKay #0: chain length 7,
irregular face structure across depths.  No counterexample yet but
no proof either.

Net assessment: structurally sound reformulation, but inherits all
open conjectures from the existing approaches plus new technical
issues.

Concrete next step: extend tire_fiber_step2-style pairwise compatibility
check to the cut-tire setting and see if R_0 ∩ R_1 = ∅ empirically
on the Holton-McKay graphs.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 15:37:14 -04:00
didericis 3172371fb8 coloring_nested_tire_graphs: fix \newtheorem{definition} preamble in cut_depth_label
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 15:33:07 -04:00
didericis 53a676971c coloring_nested_tire_graphs: define "cut tire" with multi-depth visualisation
Adds Definition (cut tire) to cut_depth_label.tex:

  Given the depth labelling on G'_i, for each d > 0 let H_d be the
  subgraph on depth-d edges (with inherited planar embedding).  For
  each face f of H_d, the cut tire at (d, f) is the subgraph of G'_i
  consisting of:
    - every edge on the boundary walk of f (all depth d), and
    - every edge of G'_i incident to the boundary walk of f with
      depth d-1 or d+1.

The depth-d edges form the "face boundary"; the d-1 edges are
"inner spokes" (toward the cut); the d+1 edges are "outer spokes."

This is the dual-side analogue of the tire annular face connector
T'_{f'} (paper.tex Def. 1.16):
  face boundary ↔ T'_ann (annular subgraph at depth d)
  cut tire     ↔ T'_{f'} (annular face connector)
  inner/outer spokes ↔ inner/outer spokes of T'_{f'}

Adds experiments/cut_tire.py producing fig_cut_tire.png:
5-panel visualisation of cut tires at depths d = 1, 2, 4, 5, 6 on
G'_1 (V\S half of Holton-McKay #0). Outermost tire at d=1 (face
length 12, 5+4 spokes); innermost at d=6 (face length 12, 7+1).

Note grows from 3 → 5 pages.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 15:32:47 -04:00
didericis d065c5c31b coloring_nested_tire_graphs: shared-layout figure for cut-and-depth-label procedure
Computes a single nice layout for the full G' (Holton-McKay #0) by
trying sage-planar, sage-spring, and networkx-planar layouts and
picking the one with smallest edge-length coefficient of variation.
Spring layout wins (CV^2 = 0.049).

Then uses the SAME positions for G'_0 and G'_1, with pendant
vertices placed offset from their boundary vertex in the direction
of their cut-edge neighbor.  This makes the visual correspondence
between G' and its two halves immediate.

Layout: 3 vertical panels showing G' (with cut edges highlighted),
G'_0, G'_1.  Each subgraph draws only its own vertices (no orphan
vertices from the other side); all three share the same x-y limits
so positions align across panels.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 15:08:06 -04:00
didericis d9748e38d9 coloring_nested_tire_graphs: cut-and-depth-label procedure with Holton-McKay #0 example
Adds a new note describing a cut-and-depth-label procedure for
the dual G' of a maximal planar G:

  1. Find a 6-edge cut C in G'.
  2. Remove cut edges → G'_0, G'_1.
  3. In each G'_i:
     a. V_i = degree-2 vertices (vertices incident to exactly 1
        cut edge, hence degree 3-1=2 in induced subgraph).
     b. For each v ∈ V_i, add a pendant edge to a new vertex.
        Label pendants depth 0.
     c. BFS-propagate: edges adjacent to a depth-d edge get
        depth d+1, until all edges are labelled.

Worked example on Holton-McKay graph #0 (38-vertex non-Hamiltonian
cubic plane graph, dual of a 21-vertex triangulation):

  - 128 distinct 6-edge cuts found by greedy search.
  - Best matching cut: |S| = 10, cut = 6 edges with 12 distinct
    endpoints (6 per side).
  - G'_0: 10 + 6 = 16 vertices, max depth 2.
  - G'_1: 28 + 6 = 34 vertices, max depth 7.

The procedure mirrors the 4CT cut-and-reglue reducibility scheme:
each G'_i has pendants restoring cubicity at the boundary; the
depth labels organize G'_i into concentric layers by distance to
the cut. This is the dual analogue of plane depth from a level
cycle (cf. the level-cycle generalization discussion).

Files:
  experiments/cut_depth_label.py
  notes/cut_depth_label.tex (3 pages)
  notes/fig_cut_depth_label.png

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 15:00:42 -04:00
didericis 82f58f2f88 plane_depth: add level/interlevel dual edge definitions
Extends Definition 1.2 (level edge) to also define "interlevel edge"
for the primal, and adds Definition 1.3 (level/interlevel dual edge)
classifying dual edges by whether they cross a level or interlevel
primal edge.

Useful downstream: in coloring_nested_tire_graphs, the partial tire
dual's edges can now be classified cleanly as level or interlevel
dual edges using the same vocabulary, instead of ad hoc "interior
annular edge" / "spoke edge" naming.

Paper stays at 4 pages.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 14:17:09 -04:00
didericis 8b6c2b621c split: extract foundational depth material into new plane_depth paper
Splits the existing plane_depth_sequencing paper into two:

  papers/plane_depth/paper.tex (NEW, 4 pages):
    - Plane depth definition.
    - Level edge, up/down/neutral triangle classification.
    - Outerplanarity lemma (formerly Lemma 2.6 of PDS).
    - Deep embedding G' definition.
    - "Every face of G' is up or down" lemma.
    - Unique level edge per face; shared level edge between adjacent faces.
    - Quadrilateral decomposition definition with three types
      (shallow diamond, deep diamond, S quad).

  papers/plane_depth_sequencing/paper.tex (slimmed from 11 → 6 pages):
    - Cites plane_depth for all foundational definitions.
    - Keeps: slice, move definitions (anchor drop, level add, join,
      ring completion), move selection, termination theorem.

  papers/coloring_nested_tire_graphs/paper.tex:
    - Bibliography updated: cite bauerfeld-depth instead of bauerfeld-pds.
    - Two in-text references updated to cite the new outerplanarity
      lemma in plane_depth.

Rationale: the outerplanarity / deep-embedding / quadrilateral-
decomposition material is foundational and reused by multiple
papers (and by the proposed level-cycle generalization).  The
quadrilateral-sequencing programme is one specific application.
Splitting lets coloring_nested_tire_graphs cite the foundations
cleanly without dragging in the sequencing machinery.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 13:49:44 -04:00
didericis 1513922dec coloring_nested_tire_graphs: partial proof of closed-chain non-emptiness identifies the 4CT-equivalent gap
Attempts to prove item 1 (non-emptiness of state at L_n in closed
SR+PDS chains ending at outer triangle). Results:

PROVEN:
- S_3-closure preserved by chain propagation.
- State at L_n is either empty OR equals all 6 permutations of {1,2,3}
  (the only non-empty S_3-closed subset of permutations).
- Non-emptiness propagates through intermediate tires under outward
  PDS via step-1 saturation.

REMAINING GAP (conjecture, empirically true): state at L_{n-1}
intersects the "perm-paired" subset of T_n's σ_D-projection (the
σ_D values that pair with permutation σ_U). At the final step T_n
has m_n=3 < k_n, so saturation fails — chain state at L_{n-1} could
in principle lie entirely in the (non-perm-paired) parity-matching
σ_D's, but empirically doesn't.

KEY STRUCTURAL FINDING: for T=(3, k), the σ_D's paired with a
permutation σ_U equal exactly the (parity-matching σ_D's) ∩ (T's
σ_D-projection). Verified for k=3..10.

HONEST OBSERVATION: a structural proof of the remaining conjecture
(without invoking 4CT) would constitute a new proof of 4CT under
the SR+PDS modelling assumption. The chain-pigeonhole framework
reduces to this single reachability question.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 12:58:20 -04:00
didericis c8ddbb5d9f coloring_nested_tire_graphs: prove outer-triangle absorption via K_3-walk parity invariant
Investigation of the 'outer triangle absorption' hypothesis from
notes/outer_triangle_absorption.tex:

H2 (T_n alone absorbs anything to 6 perms): REFUTED. T_n=(3,k) alone
has σ_U-projection equal to all 27 elements of {1,2,3}^3.

H1 (chain does real work): TRUE, and structurally explained:

  K_3-walk parity invariant (Lemma): in any proper edge 3-coloring
  of C_n viewed as a closed walk in K_3, the 3 edge-traversal counts
  all have the same parity (follows from each vertex's walk-degree
  being even).

  σ-color count parity (Corollary): σ at the full n cycle positions
  has all-same-parity color counts.

  Chain preserves parity (Theorem): forward propagation through SR
  tire T=(m,k) maps state with parity matching k to state with parity
  matching m, via σ_U + σ_D = σ_total with parities adding mod 2.

  Outer-triangle absorption (Main Theorem): at L_n with |L_n|=3,
  state has all-odd color counts summing to 3, forcing each count =
  1, i.e., σ is a permutation of {1,2,3}.

Empirically verified: 0 parity violations across all chain states
in 3 representative chains (sizes 30-14643).

What's left:
  - Non-emptiness: state at L_n EQUALS (not just ⊆) the 6 permutations.
    Empirically yes. Likely via S_3-invariance argument.
  - SR-correctness for actual G (the modeling gap, not addressed here).

If non-emptiness and SR-correctness are closed, this is a structural
proof of 4CT under the PDS framework — fundamentally different from
Birkhoff/Heesch reducibility.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 12:42:28 -04:00
didericis 50183df6bc coloring_nested_tire_graphs: write up closed-chain SR+PDS experiment and the outer-triangle absorption hypothesis
Note records the closed-chain experiment: forward-propagate state
through SR+PDS tire chains with degenerate-inner T_1 and outer-
triangle T_n (m_n=3). All 10 tested chains converge to the same
final state at L_n — exactly the 6 permutations of {1,2,3}.

Introduces the "outer triangle absorption" framing: distinguishes
H1 (chain-dependent: pigeonhole does real work to filter input to
T_n) vs H2 (T_n-only absorption: T_n's σ_U-projection is intrinsically
the 6 permutations regardless of input). Conjecture: H2 (testable by
single-tire computation).

If H2 holds, items 3-4 of the 4CT-via-tire-decomposition outline
become automatic from local data. If H1, the chain-pigeonhole does
structural work and the question is sharper.

Three-panel figure: (A) closed PDS chain (5,6,5,3) with concentric
levels and source apex; (B) outer-face dual constraint requiring
permutation-of-{1,2,3} on outer triangle; (C) state-size trajectory
showing absorption to 6 at the outer step.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 12:31:48 -04:00
didericis c34c754c7e coloring_nested_tire_graphs: closed-chain SR+PDS converges to outer-triangle permutations
Tested 10 closed PDS chains under SR (degenerate-inner T_1, varied
middle tires, outer-triangle T_n with m_n=3). In all cases:

  - Forward state grows in the middle (widest tires), shrinks toward outer.
  - Final state at outer-triangle L_n has size EXACTLY 6.
  - Those 6 elements are EXACTLY the permutations of {1,2,3}.
  - Outer-face dual-vertex constraint (degree-3, distinct colors) is
    satisfied in every chain.

This is strong empirical evidence that under SR+PDS, the entire
chain-pigeonhole story closes for 4CT:
  step 1 (saturation): proven
  step 2 (pairwise): automatic from step 1
  step 3 (chain consistency, open): always works
  step 4 (closed with outer-triangle constraint): always works,
    with the 6 outer-permutations as a clean attractor.

If this holds for all internally 6-connected G under SR (likely from
Birkhoff degree ≥ 5), it's a structural proof path for 4CT for
PDS-decomposable triangulations.

Remaining: prove SR holds for all internally 6-connected G; verify
exhaustively across more chains; find symbolic proof of the
"final state = exactly 6 permutations" attractor behavior.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 12:21:39 -04:00
didericis a5332ab656 coloring_nested_tire_graphs: SR + PDS chain consistency holds robustly
Redo step 2 and step 3 under SR (no chord effect, the correct model
under PDS where O-faces are not G-faces).

Step 2 (pairwise, 14 cases): all compatible. T_1's γ-side projection
saturates {1,2,3}^γ under outward PDS (m_1 ≥ γ from step 1), so
intersection = T_2's projection, always nonempty.

Step 3 (chain consistency, 10 chains up to 6 tires): all compatible.
Forward propagation along the chain shows monotonically growing
support sizes (roughly 3x per step), never empties. Free choice
accumulates outward.

Implication: chain consistency under SR + PDS is essentially
automatic for "open" chains. The remaining gap is the boundary
condition at the outermost level (e.g., the outer triangle of a
triangulated sphere has only 6 valid σ-permutations); whether the
forward state always contains one of those is the next experiment.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 12:15:41 -04:00
didericis 570de6a171 coloring_nested_tire_graphs: A-irreducibility analysis of smallest strict-Latin SP failure
Joint-support analysis on (γ=6, T_1=(m_1=3, antipodal, SP), T_2=(k_2=3, no chord, SP)):

T_1's σ_D space = 18 elements (half of Latin set's 36; saturation-
threshold violated by m_1=3 < γ=6). T_2's σ_U space = 84 elements.
The two are intrinsically disjoint on γ, AND S_3-closure of T_1's
outer-ring colorings is already saturated (all 6 permutations
realised) — so abstract Kempe modification on the outside cannot
enlarge T_1's γ-support. The failure is A-IRREDUCIBLE in the
strict Birkhoff sense.

Significance: the SP failure cases aren't 4CT-relevant obstructions
but modeling artifacts. SP treats non-triangular O-faces as single
G-faces, which is incompatible with maximal-planar G. A faithful
maximal-planar G further triangulates these faces, changing the
face-connector and enlarging σ-supports.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 11:58:41 -04:00
didericis 3c1a548a01 coloring_nested_tire_graphs: threshold search at γ=13,14,15 — refined conjecture holds at γ=15
Completed 47-min threshold search using chunked enumeration. 18 pairs
tested; 4 non-strict-Latin counterexamples (all γ∈{13,14} paired with
T2 all-3 at k_2=15, structural mismatch from γ ∉ 3ℤ); 0 strict-Latin
threshold counterexamples.

γ=15 strict-Latin (all-3 ring) confirmed compatible: T1=T2=ring gives
|fwd|=|rev|=2976 ≈ 440 S_3-orbits. Mixed-config variants at γ=15 give
overlaps 2640-10752 (also large, also orbit-structured).

The refined Latin conjecture (m ≥ γ threshold) now holds across
γ ∈ {3, 6, 9, 12, 15} for all-3 configs.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 11:51:28 -04:00
didericis 1594a3f58a coloring_nested_tire_graphs: structural description of surviving γ-partitions at k=9 (positive result)
Investigated the 8 surviving triple-partitions of γ at k=k_2=9
(chord (0,3),(3,6) on B_in^(2)).  Found a clean structural
description.

CLASSIFICATION of γ-edges by T_2's face structure:
  For each O^(2)-face F_i, 2 γ-edges are "internal" to F_i
  (their adjacent D-triangles are both in F_i).
  For each adjacent face pair (F_i, F_{i+1}), 1 γ-edge is
  "boundary" between them.
  Total: 2r internal + r boundary = 3r γ-edges = |γ| when k=k_2.

STRUCTURAL DESCRIPTION (Prop face-pair-connection):
  Latin ⊆ π_U(T_2) iff the partition has the following form:
  - One block per cyclically-adjacent face pair (F_i, F_{i+1}).
  - Each block = 1 boundary edge δ_{i,i+1} + 1 internal of F_i
    + 1 internal of F_{i+1}.
  - For each face F_i, its 2 internal γ-edges are distributed
    one per block (the two blocks involving F_i).

  Count: 2^r partitions (each face has 2 choices of how to split
  its internals across its 2 adjacent blocks).

AT k = k_2 = 9 (r = 3 faces): 2^3 = 8 partitions, matching the
empirical survivors.

WHY NAIVE CANDIDATES FAIL: The next-D and prev-D candidates from
worst_case_proof_sketch.tex group BOTH internals of one face into
one block (e.g., {0,1,2} = both Internal_{F_A} + δ_{AB}, no internal
F_B).  This violates the "one internal per face per block" rule.

IMPLICATION: The König-lift approach can be RESCUED by replacing
the naive candidate F~_2 with any of the 2^r face-pair-connection
partitions.  Apply König's theorem on bipartite face-incidence
graph of F_1 vs this new F~_2.

NEXT STEP: prove Prop face-pair-connection for all r, then apply
König lift.  This is more leveraged than re-tackling the naive
construction.

Files:
  experiments/k9_surviving_analysis.py
  notes/k9_surviving_partitions.tex (3 pages)

Note also updates notes/induced_partition_findings.tex to point at
the new structural description.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 11:44:58 -04:00
didericis 6f541d2d68 coloring_nested_tire_graphs: empirical findings on the König-lift conjecture (negative)
Tested the candidate induced γ-partition from
worst_case_proof_sketch.tex (Conj t2-induces-partition).

Findings:

1. AT k = k_2 = 6 (antipodal chord, faces 3+3): Candidate
   partition (next-D or prev-D) gives Latin ⊆ π_U.  ✓

   But this is partly coincidental: |π_U| = 90 is so large that
   ALL 10 triple-partitions of {0,..,5} have Latin ⊆ π_U.

2. AT k = k_2 = 9 (chords (0,3)(3,6), faces 3+3+3): Candidate
   partition FAILS.  Only 8 of all 280 triple-partitions of
   {0,..,8} have Latin ⊆ π_U, and the candidate is not one of
   them.  The 8 surviving partitions have no obvious geometric
   interpretation.

3. ASYMMETRIC k ≠ k_2 (e.g. k=6, k_2=3): Candidate doesn't
   produce a triple-partition at all, and no triple-partition
   has Latin ⊆ π_U.  Conjecture as stated doesn't cover the
   case where the empirical worst-case overlap lives.

Implication: The candidate construction is wrong past k = 6.
Step 3 (prove inclusion) is not the right next move -- we'd
be proving a false statement.

Reassessment of Approach 2: the König-overlap proposition (when
both tires give direct γ-face partitions) is still cleanly proven,
but applies to fewer cases than hoped.  The asymmetric pairs that
witness the empirical worst case are not covered.

Both approaches now have known structural obstacles:
- Approach 1 (2-SAT): single open Conjecture 1.5, empirically true.
- Approach 2 (König): natural construction empirically wrong past
  k=6, plus asymmetric pairs out of scope.

Honest status: chain pigeonhole has no full proof yet.

Files:
  experiments/induced_partition.py
  notes/induced_partition_findings.tex (3 pages)

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 11:33:18 -04:00
didericis f0bc82b88d coloring_nested_tire_graphs: compare 2-SAT vs König-lift approaches to chain pigeonhole
Adds a side-by-side comparison of the two proof attempts now in
the repo:

  Approach 1 (cyclic 2-SAT, in rainbow_proof.tex):
    Proves π_D = P_m (perms-per-half) for one antipodal-chord SP
    tire when m_1 ≥ m - 1.  Open piece: 2-SAT solvability
    (Conjecture 1.5).

  Approach 2 (König lift, in worst_case_proof_sketch.tex):
    Proves |S_1 ∩ S_2| ≥ 6 for two adjacent SP tires sharing γ
    when both chords are on γ.  Open piece: T_2 induces a
    γ-face partition (Conj t2-induces-partition).

Assessment: Approach 2 is more promising because (a) the hard step
is already proven (König's theorem), (b) it proves exactly what we
need (chain-pigeonhole non-emptiness, not the full π_D
characterisation), and (c) it directly explains the empirical
worst-case |S_1 ∩ S_2| = 6 = single S_3-orbit phenomenon.

Approach 1 still has value if we need finer control over π_D's
shape, but for just establishing non-empty overlap Approach 2
suffices.

Both approaches witness the SAME canonical 6-element worst-case
intersection (the rainbow S_3-orbit at γ=6 = the König-lifted
Latin S_3-orbit).

Recommended next move: attack Conj t2-induces-partition.  Write
down the candidate induced γ-partition explicitly, verify it
computationally, then prove inclusion via transfer-matrix / fibre
lifting.

Note: two_approaches_comparison.tex (3 pages).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 11:19:39 -04:00
didericis 83df771199 coloring_nested_tire_graphs: add note explaining 2-SAT solvability
Standalone explanation of what "2-SAT solvability" means in the
context of the rainbow proof (rainbow_proof.tex, Conjecture 1.5):

- Defines 2-SAT in general (boolean variables, 2-variable clauses,
  P-time decidable).
- Maps it onto our rainbow proof: variables = orientation bits o_j
  at D-positions; clauses = inter-D-position gap constraints; cyclic
  chain wraps around T'_ann.
- "Solvable" ⇔ proper edge 3-coloring with given σ exists, i.e.
  σ ∈ π_D.
- Cyclic 2-SAT can in principle fail; toy example (3-cycle of
  not-equal clauses = odd-cycle 2-coloring obstruction).
- Empirically our system never fails for σ ∈ P_m (6-18 satisfying
  orientations per σ at m=6), but a structural proof is open.
- Why it matters: proving Conjecture 1.5 upgrades the rainbow
  proof's provisional corollary into a theorem and reduces chain
  pigeonhole to the perms-per-half overlap.

Note: two_sat_solvability.tex (3 pages).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 11:12:16 -04:00
didericis 659068fca7 coloring_nested_tire_graphs: worst-case proof sketch via König 3-edge-coloring; chunked enumeration + threshold search infrastructure
Proves the clean piece: when both T1 and T2 give direct all-3 γ-face
partitions of E(γ), the worst-case overlap is ≥ 6, witnessed by
König's edge-coloring theorem on the 3-regular bipartite "face-
incidence graph" G. A proper 3-edge-coloring of G lifts to a Latin
σ on γ satisfying both face partitions, and S_3 symmetry gives 6
distinct such σ.

Identifies the gap: T2's chord is on B_in_2, not on γ, so T2 doesn't
directly give a γ-partition. The proof closes if we exhibit an
"induced γ-partition" determined by T2's annular triangulation —
conjectured but not constructed here.

Also commits chunked enumeration code and threshold-search script
launched separately.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 11:12:15 -04:00
didericis d893860166 coloring_nested_tire_graphs: 6-hour counterexample search complete (2297 pairs)
Final tally across γ ∈ {3,...,15,18,21}:
- 2297 total pairs tested
- 48 strict-Latin (all-3-faces) counterexamples
- 0 threshold-satisfying (m_1 ≥ γ AND k_2 ≥ γ) counterexamples (882 such pairs)

Refined conjecture (with m_1 ≥ γ precondition) holds across all tested
threshold-satisfying pairs up to γ = 12. For γ ≥ 13, threshold pairs
were unreachable under the n ≤ 27 memory cap (m_1 ≤ 27 - γ < γ).

All 48 strict-Latin CEs violate the threshold on at least one side,
consistent with the saturation behavior identified in step 1.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 09:33:23 -04:00
didericis 56ebf49b48 coloring_nested_tire_graphs: rainbow theorem proof (sharp threshold + 2-SAT reduction)
Replaces the earlier proof sketch with a clearer attempt that:

1. Corrects the sharp threshold: m_1 >= m - 1 (not m_1 >= m).
   Empirically verified for m ∈ {4, 6} across m_1 ≥ m - 1.

2. Proves the ⊆ direction cleanly: each O-face dual vertex has
   degree m/2 ≤ 3 in T'_{f'}, so its incident spokes must be
   pairwise distinct, putting σ in the "perms-per-half" set P_m.

3. Reduces the ⊇ direction to a cyclic 2-SAT solvability claim
   (Conjecture 2sat): for each σ ∈ P_m, find an "orientation"
   o ∈ {0,1}^m at the m D-positions such that each length-1 gap
   has R_j = L_{j+1} and each length-2 gap has R_j ≠ L_{j+1}.

4. Acknowledges the gap: a naive "all-zero orientation" fails
   (e.g. rainbow at m_1 = 6 has the all-zero attempt fail at
   gap (4,5)).  A satisfying assignment exists in every tested
   case (6-18 per σ at m=6, m_1=6) but a clean general proof
   awaits.  Two routes outlined: S_3-equivariant case analysis,
   or global implication-graph analysis.

5. Confirms sharpness with explicit forcing-propagation
   counterexample at m=6, m_1=4 (rainbow not in π_D).

6. States provisional corollary: π_D = P_m at m_1 ≥ m - 1
   (conditional on Conjecture 2sat); chain pigeonhole reduces
   to π_U meeting P_m.

Honest about what's proven (the ⊆ half, the 2-SAT reduction,
the sharpness counterexample) and what's left (the 2-SAT
solvability proof).

Note: rainbow_proof.tex (4 pages).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 04:18:00 -04:00
didericis c900ec9a70 coloring_nested_tire_graphs: refute antipodal-chord rainbow conjecture as originally stated, add refined version with m_1 ≥ m precondition
Counterexample search uncovered:
  T1 = (m_1=3, chord=(0,3), SP) at γ=6
has |π_D| = 18, but the conjectured rainbow combined orbit has size 36 —
only 6 of the 36 elements actually lie in π_D, and the literal generator
pattern (1,2,3,2,3,1) is itself missing.

Refined conjecture adds m_1 ≥ m precondition (same threshold from step 1
"saturation iff m ≥ k"). Under this precondition all 44 tested
strict-Latin pairs are still compatible. Pointer to log path included.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 03:50:12 -04:00
didericis b27a4d20a3 coloring_nested_tire_graphs: rainbow-conjecture proof sketch + threshold counterexample
Attempts to prove the antipodal-chord rainbow conjecture; result is
nuanced:

1. Upper bound (proven cleanly): pi_D ⊆ {σ : (σ_0..σ_{m/2-1}) and
   (σ_{m/2}..σ_{m-1}) are both perms of {1,2,3}}.  This follows
   from the proper-coloring constraint at the two O-face dual
   vertices, each of degree m/2 in T'_{f'}.

2. Lower bound at m_1 ≥ m - 1 (constructive): every σ in the
   above set extends to a proper edge 3-coloring of T'_{f'}.
   Explicit construction at m=6, m_1=6.  In particular rainbow
   ⊂ pi_D.

3. Counterexample at m_1 ≤ m - 2 (refutes original conjecture):
   at m=6, m_1=4, the rainbow σ = (1,2,3,2,3,1) is NOT in pi_D.
   Explicit forcing-propagation contradiction: two length-1
   inter-D-position gaps on T'_ann force conflicting cycle-edge
   colors at a U-position.  Empirically |pi_D| = 18 (half the
   full set) at m=6, m_1 ∈ {3, 4}.

REVISED conjecture: pi_D equals the full "perm-per-face" set
(containing the rainbow orbit) iff m_1 ≥ m - 1.  The threshold
m_1 ≥ m - 1 is sharp.  Verified for m=4 (all m_1 ≥ 3) and m=6
(m_1 ≥ 5).

Consequence: chain-pigeonhole at γ length m reduces to a smaller
overlap condition under m_1 ≥ m - 1.  The case m_1 < m - 1
remains open -- pi_D still nonempty but the rainbow orbit is
missing; structural characterization of the surviving 18-element
support not addressed.

Note: rainbow_proof_sketch.tex (3 pages).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 03:48:48 -04:00
didericis f17dfdabd1 coloring_nested_tire_graphs: note the antipodal-chord rainbow conjecture; cross-link from step-2
Promotes the orbit_decomposition finding (rainbow orbit appears in 3
different (T_1, T_2) pairs, all with T_1 = (6, (0,3), SP)) into an
explicit conjecture:

  Conjecture (Obs:antipodal-rainbow-conjecture):
    For T = (m, (0, m/2), SP) (an antipodal-chord SP tire with m even),
    π_D(C(T)) always contains the combined orbit of
    (a, b, c, b, c, ..., b, c, a) under S_3 × C_m, with the a-positions
    at the chord endpoints and b/c alternating elsewhere.

If true, this gives a uniform structural property of antipodal-chord
SP tires: chain pigeonhole on |γ| = m shared cycles reduces to
"π_U of the other tire meets this fixed orbit."  Tested at m = 6 in
3 pairs; the m = 4 direct test (24-element conjectured orbit ⊂
36-element support) is mechanical.

Also adds a forward-pointer paragraph at the end of Obs:rainbow in
tire_fiber_step2.tex referencing orbit_decomposition.tex.

orbit_decomposition.tex: 3 pages -> 3 pages (added Conjecture section
and a "why antipodal?" paragraph).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 03:29:44 -04:00
didericis 374fca98a5 coloring_nested_tire_graphs: add Latin conjecture to paper; launch counterexample search
Adds Sec. 2 "A conjectural Latin-style substructure" with two
conjectures: (1) for tires whose every O-face has exactly 3 B_in
edges, π_D contains the Latin-flavoured subset L (where each O-face
gets a permutation of {1,2,3}); (2) adjacent tires both satisfying (1)
have compatible projections.

Adds tire_fiber_counterexample_search.py: append-log counterexample
hunt across increasing k with deduplication for resumability. Logs
to counterexample_search.log. Smoke-test data at k≤5 shows
non-all-3 SP-model artifacts produce empty intersections (the
conjecture's "exactly 3 B_in edges per face" precondition fails),
but no strict-Latin counterexample yet.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 03:26:17 -04:00
didericis 030ca67afb coloring_nested_tire_graphs: S_3-orbit decomposition of step-2 intersections
Adds orbit_decomposition note + script answering: do structurally
different (T_1, T_2) pairs share the same canonical orbits in
S_1 ∩ S_2?

Findings across the 23 step-2 pairs:

1. EVERY intersection is closed under S_3 color permutation
   (structural sanity check, follows from color-symmetry of
   proper edge 3-coloring).

2. EVERY S_3-orbit has size exactly 6, with one exception: the
   constant orbit {(c,c,c,c) : c ∈ {1,2,3}} of size 3 at γ=4,
   T_1=T_2=(4,-,SR).  So |S_1 ∩ S_2| = 6 × (# S_3-orbits) almost
   always.

3. The RAINBOW orbit (a,b,c,b,c,a) at γ=6 appears in 3 different
   (T_1, T_2) pairs -- all with T_1 = (6, (0,3), SP).  The two-
   chord SP tire (6, (0,2)(3,5), SP) never produces the rainbow
   orbit.  So rainbow is associated with the antipodal-chord
   topology, not the pair as a whole.

4. Other canonical orbits recur across structurally different
   pairs.  E.g. (1,2,1,3) at γ=4 appears in 7 of 12 tested
   γ=4 pairs.

This upgrades the step-2 finding: the intersection isn't just
non-empty -- it has full S_3-symmetric structure, contains at
least one size-6 orbit in essentially all cases, and shares
canonical orbits across varied (T_1, T_2) pairings.

Files:
  experiments/orbit_decomposition.py
  experiments/orbit_decomposition_data.txt
  notes/orbit_decomposition.tex (3 pages)

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 03:18:25 -04:00
didericis 8dd9d537f9 coloring_nested_tire_graphs: redraw rainbow orbit as edge colorings (σ on spoke edges, not vertices)
Previous figures drew σ as VERTEX colors on a 6-cycle.  This was
misleading: σ = (1,2,3,2,3,1) is not a proper vertex 3-coloring of
a hexagon (σ_5 = σ_0 = 1 at adjacent vertices), and the user
correctly flagged this.

σ is the coloring of the 6 *spoke edges* -- the G'-edges of G' that
cross γ, equivalently the 6 edges of γ ⊂ G under the duality
γ-edge ↔ crossing G'-edge.

Adjacent γ-edges meet at γ-vertices, which are not G'-vertices, so
σ has NO proper-coloring constraint on itself.  Proper-edge-coloring
constraints live on each tire's full annular cycle, which is longer
than 6 (T_1's is 12, T_2's is 9), with γ-spokes interleaved among
non-γ spokes; that's where the extendibility of σ is actually
checked.

Redrawn figures:
- fig_rainbow_orbit.png: σ drawn as edge colors of γ (not vertex
  colors), all 6 orbit elements.
- fig_rainbow_pattern.png: abstract pattern abcbca as edge labels,
  with explanatory text in the legend.
- fig_rainbow_setup.png: shows γ between the two tires with each
  tire's full annular cycle (length 12 and 9), the interleaved
  non-γ dual vertices, the dashed G'-spoke edges crossing γ
  colored by σ, and T_1's antipodal chord in O_1.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 03:03:56 -04:00
didericis 7b8a5eb81a coloring_nested_tire_graphs: numpy-optimize fiber enumeration; extend step-2 to k=9, 12
Bypasses the 3^n brute-force iteration in tire_fiber_chords.py by
directly constructing the 2^n proper edge 3-colorings of C_n via a
vectorized binary-branch numpy build. Benchmarked 146× speedup at n=12,
424× at n=15; brings n=18 to 0.1s and n=24 to 6.6s.

Step-2 extension at k=9 (13 pairs) and k=12 (10 pairs): every tested
pair is compatible (23/23, bringing total to 46/46 with the earlier
note). The S_3-orbit observation extends: the smallest tested
intersection at k=12 is again exactly 6 elements forming a single
S_3-orbit of the pattern (1,2,3,2,2,1,3,3,2,3,1,1) — each of T1's four
chord-induced faces receives a permutation of {1,2,3} as its σ-values,
a "Latin-style" assignment.

Note conjectures a structural theorem: every SP-feasible tire's
projection support contains the "Latin-flavoured" subset where each
O-face sees a permutation of {1,2,3}, and this gives a common
substructure that makes chain-pigeonhole succeed.

Caveat: intersection sizes are all multiples of 6, consistent with the
S_3 invariance of both supports.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 03:00:45 -04:00
didericis 37d139cbc9 coloring_nested_tire_graphs: figures for the rainbow-orbit result (step-2 obs:rainbow)
Adds three figures visualising the rainbow-orbit intersection from
tire_fiber_step2.tex (Observation rainbow):

  k=6, T_1=(m=6, chord=(0,3), SP) vs T_2=(k=3, no chord, SR)
  |S_1 ∩ S_2| = 6 = the S_3-orbit of (a,b,c,b,c,a)

Files:
- fig_rainbow_orbit.png: 6-panel grid showing all 6 orbit elements,
  each as a hexagon coloured by the corresponding σ.
- fig_rainbow_pattern.png: abstract pattern abcbca on the shared
  cycle γ with explicit position-class legend.
- fig_rainbow_setup.png: geometric setup — T_1 outside γ with its
  antipodal chord (v_0, v_3) ∈ O_1, T_2 inside γ (a triangle), and
  the orbit element σ = (1,2,3,2,3,1) shown on γ.

Adds experiments/draw_rainbow_orbit.py generator script.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 02:55:20 -04:00
didericis 8f3a1325ee coloring_nested_tire_graphs: step-2 adjacent-tire compatibility experiment
For pairs (T1, T2) sharing a cycle γ, intersect T1's D-projection
(inner-spoke pattern from outer tire) with T2's U-projection
(outer-spoke pattern from inner tire) on γ. Compatibility = nonempty
intersection.

Result: 23/23 tested pairs are compatible, spanning k ∈ {3,4,5,6},
both SR/SP models, and a range of chord configurations on each side.

Notable: small intersections have clean S_3-orbit structure. Worst
tested case (k=6, antipodal-chord T1 vs unchorded SR T2) has
intersection of size 6 — exactly the 3! rainbow patterns (a,b,c,b,c,a).
This suggests structural rather than accidental overlap, and points to
a theorem worth proving.

Caveats: 23 cases at k≤6 isn't a proof; longer chains (step 3) require
more than pairwise overlap.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 02:33:25 -04:00
didericis 5d81c1ed44 coloring_nested_tire_graphs: investigate chord case in O for tire face connectors
Companion to tire_fiber_data.tex. The chord case forces a modelling
choice for the surrounding G: Steiner-rich (each B_in edge gets its
own sub-triangle, chords are invisible to T'_{f'}) vs Steiner-poor
(each O-face is one G-face, chord set determines feasibility).

Under SP, a tire with k > 3 is infeasible unless O already contains
enough chords to keep every O-face at most 3 B_in edges. With chords:
support is positive but much smaller than SR — π_D never reaches 3^k,
and π_D's shrinkage is m-independent. More chords = smaller faces =
MORE support (each chord splits a hard constraint into easier ones).

Side-by-side data table for (m, k) ∈ {3,4,5,6,...}² with various
chord sets, plus 3-page note documenting the modelling choice and
implications for chain pigeonhole.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 02:11:33 -04:00