diff --git a/papers/coloring_nested_tire_dual_graphs/experiments/tire_d_reducibility.py b/papers/coloring_nested_tire_dual_graphs/experiments/tire_d_reducibility.py new file mode 100644 index 0000000..29c8424 --- /dev/null +++ b/papers/coloring_nested_tire_dual_graphs/experiments/tire_d_reducibility.py @@ -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() diff --git a/papers/coloring_nested_tire_dual_graphs/notes/tire_d_reducibility_analysis.md b/papers/coloring_nested_tire_dual_graphs/notes/tire_d_reducibility_analysis.md new file mode 100644 index 0000000..9c10010 --- /dev/null +++ b/papers/coloring_nested_tire_dual_graphs/notes/tire_d_reducibility_analysis.md @@ -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. diff --git a/papers/coloring_nested_tire_graphs/experiments/kempe_classes.py b/papers/coloring_nested_tire_graphs/experiments/kempe_classes.py new file mode 100644 index 0000000..aa0ca6e --- /dev/null +++ b/papers/coloring_nested_tire_graphs/experiments/kempe_classes.py @@ -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()