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 <noreply@anthropic.com>

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()