Add tire Kempe and D-reducibility experiments

This commit is contained in:
2026-06-08 14:24:32 -04:00
parent 35d226f8f8
commit a00bc70fec
3 changed files with 663 additions and 0 deletions
@@ -0,0 +1,263 @@
"""D-style reducibility checks for tire dual connectors.
This is an edge-side analogue of the Heesch/Appel-Haken
D-reducibility test. A tire connector is represented by its boundary
spoke state sigma in {1,2,3}^n, where n = m + k. The good states are
those that extend to a proper edge 3-coloring of the tire dual
connector, computed by tire_fiber_chords_fast.
The D-test here is intentionally explicit about its model:
* Boundary states are restricted by the Tait parity condition for an
outside cubic graph: for every pair of colors, the number of boundary
edges using those colors is even. Equivalently, all three color
counts have the same parity.
* For a bad state to survive as a possible outside obstruction, each
two-color boundary set must admit a noncrossing perfect pairing whose
single Kempe swaps all remain bad. This is the standard consistency
shape of a D-reducibility check, translated to dangling edge colors.
If the final consistent bad set is empty, the tire is D-reducible in
this edge-boundary model. If it is nonempty, the survivors are an
explicit obstruction to this D-test, not a 4CT counterexample.
Run examples:
python3 tire_d_reducibility.py --m-max 8 --k-max 8
python3 tire_d_reducibility.py --m 3 --k 6 --chords 0-3 --show-survivors
"""
from __future__ import annotations
import argparse
from functools import lru_cache
from itertools import product
from pathlib import Path
import sys
HERE = Path(__file__).resolve().parent
sys.path.insert(0, str(HERE))
from tire_fiber_chords import compute_faces_from_chords
from tire_fiber_chords_fast import fiber_distribution_fast, spoke_only_fiber_distribution_fast
COLORS = (1, 2, 3)
COLOR_PAIRS = ((1, 2), (1, 3), (2, 3))
def parse_chords(text: str) -> list[tuple[int, int]]:
if not text:
return []
chords = []
for part in text.split(","):
a, b = part.split("-")
chords.append(tuple(sorted((int(a), int(b)))))
return sorted(chords)
def chord_crosses(c1: tuple[int, int], c2: tuple[int, int]) -> bool:
a, b = sorted(c1)
c, d = sorted(c2)
return (a < c < b < d) or (c < a < d < b)
def all_noncrossing_chord_sets(k: int, max_chords: int | None = None):
candidates = [
(a, b)
for a in range(k)
for b in range(a + 2, k)
if not (a == 0 and b == k - 1)
]
out: list[tuple[tuple[int, int], ...]] = [()]
def rec(start: int, chosen: tuple[tuple[int, int], ...]) -> None:
if max_chords is not None and len(chosen) >= max_chords:
return
for idx in range(start, len(candidates)):
ch = candidates[idx]
if any(chord_crosses(ch, old) for old in chosen):
continue
nxt = chosen + (ch,)
out.append(nxt)
rec(idx + 1, nxt)
rec(0, ())
return sorted(set(out), key=lambda cs: (len(cs), cs))
def sp_feasible(k: int, chords: tuple[tuple[int, int], ...]) -> bool:
"""Steiner-poor feasibility: no inner O-face may hit >3 B_in edges."""
if not chords:
return k <= 3
return max(len(face) for face in compute_faces_from_chords(k, list(chords))) <= 3
def parity_feasible(state: tuple[int, ...]) -> bool:
counts = [state.count(c) for c in COLORS]
return (counts[0] % 2) == (counts[1] % 2) == (counts[2] % 2)
def boundary_universe(n: int) -> set[tuple[int, ...]]:
return {s for s in product(COLORS, repeat=n) if parity_feasible(s)}
def toggle_pair(state: tuple[int, ...], i: int, j: int, a: int, b: int) -> tuple[int, ...]:
values = list(state)
for idx in (i, j):
values[idx] = b if values[idx] == a else a
return tuple(values)
@lru_cache(maxsize=None)
def noncrossing_matchings(positions: tuple[int, ...]) -> tuple[tuple[tuple[int, int], ...], ...]:
"""All noncrossing perfect matchings of positions on a circle.
Positions are listed in cyclic order. The recursion pairs the
first position with another position that leaves an even number of
positions on each side.
"""
positions = tuple(positions)
if not positions:
return ((),)
if len(positions) % 2:
return ()
first = positions[0]
results = []
for idx in range(1, len(positions)):
left = positions[1:idx]
right = positions[idx + 1 :]
if len(left) % 2 or len(right) % 2:
continue
for lm in noncrossing_matchings(left):
for rm in noncrossing_matchings(right):
results.append(((first, positions[idx]),) + lm + rm)
return tuple(results)
def has_consistent_pairing(state: tuple[int, ...], bad: set[tuple[int, ...]], a: int, b: int) -> bool:
positions = tuple(i for i, color in enumerate(state) if color in (a, b))
if not positions:
return True
for matching in noncrossing_matchings(positions):
if all(toggle_pair(state, i, j, a, b) in bad for i, j in matching):
return True
return False
def maximal_consistent_bad_set(initial_bad: set[tuple[int, ...]]) -> set[tuple[int, ...]]:
bad = set(initial_bad)
changed = True
while changed:
changed = False
keep = set()
for state in bad:
if all(has_consistent_pairing(state, bad, a, b) for a, b in COLOR_PAIRS):
keep.add(state)
if len(keep) != len(bad):
bad = keep
changed = True
return bad
def analyze_tire(m: int, k: int, chords: tuple[tuple[int, int], ...], model: str) -> dict:
n = m + k
if model == "SR":
fibers = spoke_only_fiber_distribution_fast(n)
faces = (tuple(range(n)),)
else:
fibers, _, faces = fiber_distribution_fast(m, k, list(chords))
good = set(fibers)
universe = boundary_universe(n)
good_feasible = good & universe
bad = universe - good_feasible
survivors = maximal_consistent_bad_set(bad)
return {
"m": m,
"k": k,
"n": n,
"chords": chords,
"model": model,
"faces": tuple(tuple(face) for face in faces),
"universe": len(universe),
"good": len(good_feasible),
"bad": len(bad),
"survivors": len(survivors),
"a_reducible": len(bad) == 0,
"d_reducible": len(survivors) == 0,
"survivor_examples": tuple(sorted(survivors)[:10]),
}
def format_chords(chords: tuple[tuple[int, int], ...]) -> str:
return "-".join(f"{a}{b}" for a, b in chords) if chords else "none"
def print_rows(rows: list[dict]) -> None:
print(
"m k n model chords universe good bad survivors A D faces"
)
print(
"- - - ----- ------------ -------- ---- --- --------- - - ----------------"
)
for r in rows:
faces = "|".join("{" + ",".join(map(str, f)) + "}" for f in r["faces"])
print(
f"{r['m']:>1} {r['k']:>1} {r['n']:>2} {r['model']:<5} {format_chords(r['chords']):<12} "
f"{r['universe']:>8} {r['good']:>4} {r['bad']:>3} {r['survivors']:>9} "
f"{'Y' if r['a_reducible'] else 'N'} {'Y' if r['d_reducible'] else 'N'} {faces}"
)
def main() -> None:
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("--m", type=int, help="single outer boundary length")
parser.add_argument("--k", type=int, help="single inner boundary length")
parser.add_argument("--chords", default="", help="comma-separated chords like 0-3,4-6")
parser.add_argument("--m-max", type=int, default=8)
parser.add_argument("--k-max", type=int, default=8)
parser.add_argument("--max-chords", type=int, default=None)
parser.add_argument("--model", choices=("SP", "SR", "both"), default="SP")
parser.add_argument("--include-infeasible-sp", action="store_true")
parser.add_argument("--show-survivors", action="store_true")
args = parser.parse_args()
rows = []
if args.m is not None or args.k is not None:
if args.m is None or args.k is None:
raise SystemExit("--m and --k must be supplied together")
chords = tuple(parse_chords(args.chords))
models = ("SP", "SR") if args.model == "both" else (args.model,)
for model in models:
rows.append(analyze_tire(args.m, args.k, chords, model))
else:
for m in range(3, args.m_max + 1):
for k in range(3, args.k_max + 1):
models = ("SP", "SR") if args.model == "both" else (args.model,)
for model in models:
if model == "SR":
rows.append(analyze_tire(m, k, (), model))
continue
for chords in all_noncrossing_chord_sets(k, args.max_chords):
if not args.include_infeasible_sp and not sp_feasible(k, chords):
continue
rows.append(analyze_tire(m, k, chords, model))
print_rows(rows)
if args.show_survivors:
print()
for r in rows:
if r["survivor_examples"]:
print(
f"survivors m={r['m']} k={r['k']} model={r['model']} "
f"chords={format_chords(r['chords'])}: "
f"{r['survivor_examples']}"
)
n_d = sum(1 for r in rows if r["d_reducible"])
print()
print(f"checked {len(rows)} tire types; D-reducible in this model: {n_d}; non-D: {len(rows) - n_d}")
if __name__ == "__main__":
main()
@@ -0,0 +1,109 @@
# Tire D-Reducibility Analysis
This note records the first computational pass at applying the
Heesch/Appel-Haken idea of D-reducibility to tire dual connectors.
The executable experiment is
`../experiments/tire_d_reducibility.py`.
## Model
The test is on the Tait edge-coloring side, consistent with the
existing fiber notes:
- A tire connector has boundary state
`sigma in {1,2,3}^n`, where `n = m + k`.
- A state is **good** if it extends to a proper edge 3-coloring of the
tire dual connector.
- A state is **bad** if it is parity-feasible for an outside cubic
graph but not good.
- The D-style consistency prune starts with all bad states and deletes
a bad state whenever some color pair has no noncrossing perfect
pairing of its boundary positions whose elementary Kempe swaps all
remain inside the bad set.
Thus the conclusion is an edge-boundary analogue of classical
D-reducibility:
- `D = yes`: no nonempty consistent bad set survives.
- `D = no`: a consistent bad set survives, so this tire is not
D-reducible in this model.
This is deliberately not stated as a classical primal-side
configuration certificate. The boundary object here is a sequence of
Tait spoke colors, not a 4-colored vertex ring.
## Commands Run
Small Steiner-poor sweep:
```bash
python3 papers/coloring_nested_tire_dual_graphs/experiments/tire_d_reducibility.py --m-max 6 --k-max 6
```
Small Steiner-rich / spoke-only sweep:
```bash
python3 papers/coloring_nested_tire_dual_graphs/experiments/tire_d_reducibility.py --model SR --m-max 6 --k-max 6
```
Targeted strict-Latin-style obstruction:
```bash
python3 papers/coloring_nested_tire_dual_graphs/experiments/tire_d_reducibility.py --m 3 --k 6 --chords 0-3 --show-survivors
```
Targeted `m = k = 6` comparison:
```bash
python3 papers/coloring_nested_tire_dual_graphs/experiments/tire_d_reducibility.py --m 6 --k 6 --model both --chords 0-3 --show-survivors
```
## Findings
For `3 <= m,k <= 6`, every checked tire is non-D in this model.
- Steiner-poor sweep: 204 tire types checked, 0 D-reducible.
- Steiner-rich sweep: 16 spoke-only tire types checked, 0 D-reducible.
- In all checked cases, the maximal consistent bad set equals the
initial bad set. In other words, the D-prune does not rescue any
bad boundary states.
Representative outputs:
```text
m k n model chords universe good bad survivors A D
3 3 6 SP none 183 24 159 159 N N
3 3 6 SR none 183 63 120 120 N N
3 6 9 SP 03 4920 24 4896 4896 N N
6 6 12 SR none 132861 4095 128766 128766 N N
```
The `m=3, k=6, chord=(0,3)` case is especially severe: only 24
parity-feasible boundary states are good, while 4896 are bad and all
4896 survive the D-consistency check.
## Interpretation
The tire connector supports are much too sparse for single-connector
D-reducibility to be the right tool. In the checked range, a tire
does not behave like Birkhoff's diamond, where every bad ring coloring
can be Kempe-moved to a good one. Instead, the bad set is itself
Kempe-consistent under the edge-boundary abstraction.
This supports the strategic conclusion from
`birkhoff_heesch_reducibility.tex`: classical D-reducibility is useful
as vocabulary and as a finite verification framework, but the tire
program probably needs a compositional support-overlap or transfer
argument across adjacent/nested tires rather than single-tire
D-reducibility.
## Next Checks
The natural follow-up is not to keep searching for D-reducible
individual tires, but to test stronger compositional statements:
- classify when adjacent tire supports on a shared cycle intersect;
- run the D-consistency prune on composed two-tire or three-tire
connectors;
- compare the edge-boundary result against a primal-side free
completion for the same small tire patches.
@@ -0,0 +1,291 @@
"""Kempe-class enumeration for vertex 4-colorings of tires.
For each tire T = (B_out, O, E_ann), we:
1. enumerate every proper vertex 4-coloring of V(T);
2. quotient by S_4 (color relabeling) via a first-appearance canonical
form, giving the set Q of canonical colorings;
3. build the *Kempe graph* on Q: for every canonical c in Q, every
color pair {a,b} in {0,1,2,3}, and every connected component K of
the subgraph of T induced by vertices colored a or b, swap
a <-> b on K, canonicalize the result, and add an edge;
4. count connected components of the Kempe graph.
A tire is *single-class* if its Kempe graph has one component, i.e. all
S_4-classes of 4-colorings are mutually Kempe-reachable.
The tire family enumerated is the (m, k, chord-set, lattice-path)
parameterization from the companion `coloring_nested_tire_dual_graphs`
paper: outer cycle on m vertices, inner cycle on k vertices with
non-crossing chords inside, annulus triangulated by a lattice path
(m 'O' moves, k 'I' moves) anchored at the spoke outer[0]-inner[0].
Note: distinct lattice paths can yield isomorphic tires, so the counts
here are over labeled-tire combinatorial classes, not isomorphism types.
Run:
python3 kempe_classes.py # default m,k<=5, no chords
python3 kempe_classes.py --m-max 6 --k-max 6 --max-chords 1
python3 kempe_classes.py --m 5 --k 4 --path OIOIOIOI --chords '' --dump
"""
from __future__ import annotations
import argparse
from collections import defaultdict, deque
from itertools import combinations
import time
def all_lattice_paths(m, k):
n = m + k
paths = []
def rec(prefix, o_left, i_left):
if o_left == 0 and i_left == 0:
paths.append(prefix)
return
if o_left:
rec(prefix + 'O', o_left - 1, i_left)
if i_left:
rec(prefix + 'I', o_left, i_left - 1)
rec('', m, k)
return paths
def chord_crosses(c1, c2):
a, b = c1; c, d = c2
return (a < c < b < d) or (c < a < d < b)
def all_noncrossing_chord_sets(k, max_chords):
candidates = [(a, b) for a in range(k) for b in range(a + 2, k)
if not (a == 0 and b == k - 1)]
out = [()]
def rec(start, chosen):
if len(chosen) >= max_chords:
return
for idx in range(start, len(candidates)):
ch = candidates[idx]
if any(chord_crosses(ch, old) for old in chosen):
continue
nxt = chosen + (ch,)
out.append(nxt)
rec(idx + 1, nxt)
rec(0, ())
return out
def build_tire(m, k, chords, lattice_path):
outer = list(range(m))
inner = list(range(m, m + k))
adj = [set() for _ in range(m + k)]
def add(u, v):
if u != v:
adj[u].add(v); adj[v].add(u)
for i in range(m):
add(outer[i], outer[(i + 1) % m])
for j in range(k):
add(inner[j], inner[(j + 1) % k])
for (a, b) in chords:
add(inner[a], inner[b])
add(outer[0], inner[0])
i, j = 0, 0
for mv in lattice_path:
if mv == 'O':
add(inner[j % k], outer[(i + 1) % m])
i += 1
else:
add(outer[i % m], inner[(j + 1) % k])
j += 1
return [tuple(sorted(s)) for s in adj]
def proper_4colorings(adj):
n = len(adj)
colors = [-1] * n
out = []
def rec(v):
if v == n:
out.append(tuple(colors))
return
used = 0
for u in adj[v]:
if u < v:
used |= 1 << colors[u]
for c in range(4):
if used & (1 << c):
continue
colors[v] = c
rec(v + 1)
colors[v] = -1
rec(0)
return out
def canonicalize(coloring):
mapping = {}
out = []
for c in coloring:
if c not in mapping:
mapping[c] = len(mapping)
out.append(mapping[c])
return tuple(out)
def kempe_neighbors(coloring, adj, a, b):
n = len(coloring)
in_set = [coloring[v] == a or coloring[v] == b for v in range(n)]
seen = [False] * n
out = []
for start in range(n):
if not in_set[start] or seen[start]:
continue
comp = []
q = deque([start])
seen[start] = True
while q:
v = q.popleft()
comp.append(v)
for u in adj[v]:
if in_set[u] and not seen[u]:
seen[u] = True
q.append(u)
new = list(coloring)
for v in comp:
new[v] = b if new[v] == a else a
out.append(tuple(new))
return out
def kempe_components(adj):
raw = proper_4colorings(adj)
canon = sorted({canonicalize(c) for c in raw})
index = {c: i for i, c in enumerate(canon)}
parent = list(range(len(canon)))
def find(x):
while parent[x] != x:
parent[x] = parent[parent[x]]
x = parent[x]
return x
def union(x, y):
rx, ry = find(x), find(y)
if rx != ry:
parent[rx] = ry
for c in canon:
ci = index[c]
for a, b in combinations(range(4), 2):
for swapped in kempe_neighbors(c, adj, a, b):
cs = canonicalize(swapped)
if cs == c:
continue
union(ci, index[cs])
classes = defaultdict(list)
for c, ci in index.items():
classes[find(ci)].append(c)
return list(classes.values()), len(raw)
def format_chords(chords):
return ','.join(f'{a}-{b}' for a, b in chords) if chords else 'none'
def sweep(m_max, k_max, max_chords, verbose=False):
multi = []
rows = []
t0 = time.time()
for m in range(3, m_max + 1):
for k in range(3, k_max + 1):
chord_sets = all_noncrossing_chord_sets(k, max_chords)
paths = all_lattice_paths(m, k)
n_tires = len(chord_sets) * len(paths)
t_mk = time.time()
for chords in chord_sets:
for path in paths:
adj = build_tire(m, k, chords, path)
classes, n_raw = kempe_components(adj)
n_classes = len(classes)
n_canon = sum(len(cl) for cl in classes)
rows.append((m, k, chords, path, n_raw, n_canon, n_classes))
if n_classes > 1:
multi.append((m, k, chords, path, n_raw, n_canon,
n_classes, classes))
if verbose:
print(f" m={m} k={k}: {n_tires} tires in "
f"{time.time() - t_mk:.2f}s")
elapsed = time.time() - t0
return rows, multi, elapsed
def print_summary(rows, multi, elapsed):
by_count = defaultdict(int)
for r in rows:
by_count[r[6]] += 1
print(f"# tires checked: {len(rows)} in {elapsed:.2f}s")
print("Kempe class count distribution:")
for nc, cnt in sorted(by_count.items()):
print(f" {nc} class(es): {cnt} tires")
print(f"# multi-class tires: {len(multi)}")
if multi:
by_mk = defaultdict(int)
for (m, k, *_rest) in multi:
by_mk[(m, k)] += 1
print("multi-class breakdown by (m, k):")
for (m, k), cnt in sorted(by_mk.items()):
print(f" (m={m}, k={k}): {cnt}")
def dump_multi(multi, limit=10, show_classes=False):
if not multi:
return
print()
print(f"first {min(limit, len(multi))} multi-class tires:")
for (m, k, chords, path, n_raw, n_canon, n_classes, classes) in multi[:limit]:
print(f" m={m} k={k} chords={format_chords(chords)} path={path}: "
f"raw={n_raw} canon={n_canon} classes={n_classes}")
if show_classes:
for i, cl in enumerate(classes):
rep = sorted(cl)[0]
print(f" class {i} (size {len(cl)}): rep={rep}")
def main():
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument('--m', type=int, help='single tire: outer length')
parser.add_argument('--k', type=int, help='single tire: inner length')
parser.add_argument('--path', type=str, help='single tire: lattice path')
parser.add_argument('--chords', type=str, default='',
help='single tire: e.g. "0-2,1-3" or empty')
parser.add_argument('--m-max', type=int, default=5)
parser.add_argument('--k-max', type=int, default=5)
parser.add_argument('--max-chords', type=int, default=0)
parser.add_argument('--show-multi', type=int, default=10,
help='print up to N multi-class tires (default 10)')
parser.add_argument('--dump', action='store_true',
help='print full class data for each multi-class tire')
parser.add_argument('-v', '--verbose', action='store_true')
args = parser.parse_args()
if args.m is not None and args.k is not None and args.path is not None:
chords = ()
if args.chords:
chords = tuple(tuple(sorted((int(a), int(b))))
for a, b in (p.split('-') for p in args.chords.split(',')))
adj = build_tire(args.m, args.k, chords, args.path)
classes, n_raw = kempe_components(adj)
n_classes = len(classes)
n_canon = sum(len(cl) for cl in classes)
print(f"m={args.m} k={args.k} chords={format_chords(chords)} "
f"path={args.path}")
print(f" raw 4-colorings: {n_raw}")
print(f" canonical (mod S_4): {n_canon}")
print(f" Kempe classes: {n_classes}")
for i, cl in enumerate(classes):
rep = sorted(cl)[0]
print(f" class {i}: size={len(cl)} rep={rep}")
return
rows, multi, elapsed = sweep(args.m_max, args.k_max, args.max_chords,
verbose=args.verbose)
print_summary(rows, multi, elapsed)
dump_multi(multi, limit=args.show_multi, show_classes=args.dump)
if __name__ == '__main__':
main()