From d7c93cf2c28d076e3f0f4b529ea048d89281fe6e Mon Sep 17 00:00:00 2001 From: didericis Date: Wed, 17 Jun 2026 20:35:49 -0400 Subject: [PATCH] Test induction strategy for the irreducible lemma reduction_exists.py: every disk with k>=1 (and every irreducible disk) has a Phi-NON-INCREASING vertex removal (|Phi(D-v)| <= |Phi(D)|), 100% over thousands of disks -- so induction to the k=0 base case is viable. BUT the clean set-inclusion Phi(D-v) subset Phi(D) holds for only ~8%, so the size step cannot be proved by "re-inserting v loses no sequence"; it needs a genuine cardinality injection between non-nested sets. Co-Authored-By: Claude Opus 4.8 --- .../experiments/reduction_exists.py | 168 ++++++++++++++++++ 1 file changed, 168 insertions(+) create mode 100644 papers/heawood_restrictions_on_nested_tire_graph_duals/experiments/reduction_exists.py diff --git a/papers/heawood_restrictions_on_nested_tire_graph_duals/experiments/reduction_exists.py b/papers/heawood_restrictions_on_nested_tire_graph_duals/experiments/reduction_exists.py new file mode 100644 index 0000000..203c932 --- /dev/null +++ b/papers/heawood_restrictions_on_nested_tire_graph_duals/experiments/reduction_exists.py @@ -0,0 +1,168 @@ +""" +Proof strategy A for the irreducible lemma (|Phi| >= 2^(n-2)): + + induction on k via a Phi-NON-INCREASING vertex removal. Monotonicity is false + (some removals raise Phi), but we only need ONE good removal per disk: if every + disk with k>=1 has an interior vertex v and a link-retriangulation with + |Phi(D - v)| <= |Phi(D)|, then chaining down to k=0 gives |Phi(D)| >= 2^(n-2). + +This probe: for each disk, try removing each interior vertex (retriangulating its +link by a fan from every link vertex, keeping only valid retriangulations), and +record whether the BEST removal satisfies |Phi(D-v)| <= |Phi(D)|. Reports the +fraction of disks where such a removal EXISTS (strategy viable) vs disks where +EVERY removal strictly raises Phi (strategy fails) -- and dumps the failures. +""" + +import sys +from collections import Counter, defaultdict +from itertools import product + +import numpy as np +from scipy.spatial import Delaunay + +np.seterr(all="ignore") + + +def disk(n, k, rng): + ang = 2 * np.pi * np.arange(n) / n + rad = 1.0 + 0.18 * rng.random(n) + bpts = np.c_[rad * np.cos(ang), rad * np.sin(ang)] + r = 0.8 * np.sqrt(rng.random(k)); t = 2 * np.pi * rng.random(k) + pts = np.vstack([bpts, np.c_[r * np.cos(t), r * np.sin(t)]]) + return [tuple(int(x) for x in s) for s in Delaunay(pts).simplices] + + +def valid(faces, n, k): + if len(faces) != 2 * k + n - 2: + return False + ec = Counter() + for a, b, c in faces: + for e in ((a, b), (b, c), (a, c)): + ec[frozenset(e)] += 1 + return all(ec[frozenset((i, (i + 1) % n))] == 1 for i in range(n)) + + +def phi_size(faces, n): + interior = sorted(set(v for f in faces for v in f if v >= n)) + F = len(faces) + if F > 16: + return None + Bint = np.zeros((len(interior), F), dtype=np.int64) + Cinc = np.zeros((n, F), dtype=np.int64) + iidx = {w: r for r, w in enumerate(interior)} + for j, (a, b, c) in enumerate(faces): + for v in (a, b, c): + if v >= n: + Bint[iidx[v], j] = 1 + else: + Cinc[v, j] = 1 + labs = np.array(list(product((1, 2), repeat=F)), dtype=np.int64) + if interior: + labs = labs[np.all((labs @ Bint.T) % 3 == 0, axis=1)] + if labs.shape[0] == 0: + return 0 + return len(set(map(tuple, np.unique((labs @ Cinc.T) % 3, axis=0)))) + + +def edges_of(faces): + E = set() + for a, b, c in faces: + for e in ((a, b), (b, c), (a, c)): + E.add(frozenset(e)) + return E + + +def link_cycle(faces, v): + opp = [tuple(x for x in f if x != v) for f in faces if v in f] + adj = defaultdict(list) + for a, b in opp: + adj[a].append(b); adj[b].append(a) + if any(len(adj[u]) != 2 for u in adj): + return None # link not a simple cycle + start = opp[0][0]; cyc = [start]; prev = None; cur = start + while True: + nxt = [x for x in adj[cur] if x != prev] + if not nxt: + return None + nxt = nxt[0] + if nxt == start: + break + cyc.append(nxt); prev, cur = cur, nxt + if len(cyc) > len(adj): + return None + return cyc if len(cyc) == len(adj) else None + + +def removals(faces, v, n): + """Yield valid (faces of D - v) over fan retriangulations of v's link.""" + cyc = link_cycle(faces, v) + if cyc is None: + return + d = len(cyc) + rest = [f for f in faces if v not in f] + Erest = edges_of(rest) + for s in range(d): + order = cyc[s:] + cyc[:s] + diags = [frozenset((order[0], order[j])) for j in range(2, d - 1)] + if any(dg in Erest for dg in diags): + continue # duplicate-edge: invalid retriangulation + fan = [(order[0], order[j], order[j + 1]) for j in range(1, d - 1)] + yield rest + fan + + +def main(): + seed = int(sys.argv[1]) if len(sys.argv) > 1 else 0 + rng = np.random.default_rng(seed) + irreducible_only = "--irr" in sys.argv + + tested = 0 + has_good = 0 + fail_examples = [] + + for _ in range(4000): + n = int(rng.integers(4, 7)); k = int(rng.integers(1, 4)) + faces = disk(n, k, rng) + if not valid(faces, n, k) or len(faces) > 14: + continue + deg = Counter() + for f in faces: + for x in f: + if x >= n: + deg[x] += 1 + if irreducible_only and (len(deg) < k or any(deg[x] < 4 for x in deg)): + continue + base = phi_size(faces, n) + if base is None: + continue + best = None + for v in [x for x in deg]: + for D2 in removals(faces, v, n): + s = phi_size(D2, n) + if s is None: + continue + if best is None or s < best: + best = s + if best is None: + continue + tested += 1 + if best <= base: + has_good += 1 + elif len(fail_examples) < 6: + fail_examples.append((n, k, base, best, sorted(deg.values()))) + + tag = "irreducible" if irreducible_only else "all" + print(f"disks tested ({tag}, k>=1): {tested}") + print(f" have a Phi-non-increasing removal: {has_good}/{tested} " + f"({100*has_good/max(tested,1):.1f}%)") + if fail_examples: + print(" FAILURES (every removal raised Phi) " + "(n,k,|Phi(D)|,best|Phi(D-v)|,int-degs):") + for e in fail_examples: + print(f" {e}") + else: + print(" no failure: every disk had a non-increasing removal " + "=> induction strategy A is viable.") + + +if __name__ == "__main__": + main()