Strategy A localization fails: local star-vs-fan domination is false

local_star_fan.py: the size step |Phi(D-v)| <= |Phi(D)| localizes to a
star-vs-fan contribution comparison at v. But |Star(t)| >= min_root
|Fan(t)| is FALSE (6586 violations) -- the star's extra v-constraint
(sum mu ≡ 0) can make it realize fewer boundary vectors than the fan when
the link has interior vertices. So Strategy A is globally true (100%) but
NOT via per-vertex local domination; the size inequality needs a global
union/choice-of-v argument. Useful byproduct: the Boolean-bit / mod-3
incidence reformulation of Phi.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

papers/heawood_restrictions_on_nested_tire_graph_duals/experiments/local_star_fan.py

@@ -0,0 +1,112 @@
+"""
+Local heart of the size-reduction lemma.
+
+Removing a degree-d interior vertex v swaps its star (d faces, contribution
+mu_{j-1}+mu_j at link vertex u_j, plus the v-constraint sum mu ≡ 0) for a fan
+(d-2 faces). Outside is shared, entering only as prescribed residues t_j at the
+INTERIOR link vertices. The boundary-link contribution sets are
+
+  Star(t) = {(mu_{j-1}+mu_j)_{u_j boundary} : mu in {+-1}^d, sum mu ≡ 0,
+                                              mu_{j-1}+mu_j ≡ t_j for interior u_j}
+  Fan_r(t)= {(fan_j)_{u_j boundary}        : nu in {+-1}^{d-2},
+                                              fan_j ≡ t_j for interior u_j}
+            (fan rooted at link vertex r; fan_j = contribution of the fan to u_j)
+
+The reduction may CHOOSE the fan root, so it wants min_r |Fan_r(t)|. For the
+induction |Phi(D-v)| <= |Phi(D)| to be locally supported we need, for every
+interior-mask and every t:
+
+        |Star(t)|  >=  min_r |Fan_r(t)|       (and Star(t) nonempty whenever some Fan is)
+
+We check this exhaustively for small d. (+-1 encoded as 1,2 mod 3.)
+"""
+
+import sys
+from itertools import product
+
+
+def star_contrib(d, interior, t):
+    """interior: set of link indices that are interior; t: dict j->residue for
+    interior j. Returns set of boundary contribution tuples."""
+    bnd = [j for j in range(d) if j not in interior]
+    out = set()
+    for mu in product((1, 2), repeat=d):           # +-1 as 1,2
+        if sum(mu) % 3 != 0:                        # v-constraint
+            continue
+        contrib = [(mu[(j - 1) % d] + mu[j]) % 3 for j in range(d)]
+        if any(contrib[j] != t[j] for j in interior):
+            continue
+        out.add(tuple(contrib[j] for j in bnd))
+    return out
+
+
+def fan_contrib(d, root, interior, t):
+    """Fan of the link d-gon rooted at vertex `root`. Reindex so root=0."""
+    bnd = [j for j in range(d) if j not in interior]
+    # contribution of a fan (root r) to vertex u_j, for nu over the d-2 fan faces.
+    # In root-0 coordinates faces are (0,j,j+1) for j=1..d-2 with labels nu[1..d-2].
+    # contribution: u0 -> sum(nu); u1 -> nu1; u_{d-1} -> nu_{d-2};
+    #               u_j (1<j<d-1) -> nu_{j-1}+nu_j.
+    out = set()
+    for nu in product((1, 2), repeat=d - 2):        # nu indexed 1..d-2 -> 0..d-3
+        nuf = {j: nu[j - 1] for j in range(1, d - 1)}
+        contrib = [0] * d
+        # in root coordinates u'_i = u_{(root+i) mod d}
+        c = [0] * d
+        c[0] = sum(nu) % 3
+        c[1] = nuf[1] % 3
+        c[d - 1] = nuf[d - 2] % 3
+        for j in range(2, d - 1):
+            c[j] = (nuf[j - 1] + nuf[j]) % 3
+        # map back: actual vertex = (root+i) mod d gets c[i]
+        for i in range(d):
+            contrib[(root + i) % d] = c[i]
+        if any(contrib[j] != t[j] for j in interior):
+            continue
+        out.add(tuple(contrib[j] for j in bnd))
+    return out
+
+
+def main():
+    print("Local claim:  |Star(t)| >= min_root |Fan_root(t)|  for all interior-masks, t\n")
+    fails = 0
+    checked = 0
+    worst = None
+    for d in range(3, 8):
+        for im in range(0, 1 << d):
+            interior = {j for j in range(d) if im >> j & 1}
+            if len(interior) == d:
+                continue                              # need a boundary vertex to see
+            int_list = sorted(interior)
+            for tvals in product((0, 1, 2), repeat=len(interior)):
+                t = dict(zip(int_list, tvals))
+                S = star_contrib(d, interior, t)
+                fans = [fan_contrib(d, r, interior, t) for r in range(d)]
+                # the reduction needs Star nonempty whenever it removes v; and
+                # it picks the fan, so compare to the SMALLEST fan that is itself
+                # achievable (nonempty) -- an empty fan means that root is invalid.
+                nonempty_fans = [len(f) for f in fans if f]
+                if not S:
+                    # star infeasible: then v cannot carry this context. Only a
+                    # problem if some fan IS feasible (then D-v has a seq D lacks).
+                    if nonempty_fans:
+                        fails += 1
+                    continue
+                checked += 1
+                if nonempty_fans:
+                    mn = min(nonempty_fans)
+                    if len(S) < mn:
+                        fails += 1
+                        if worst is None or len(S) - mn < worst[0]:
+                            worst = (len(S) - mn, d, sorted(interior), t,
+                                     len(S), mn)
+    print(f"  configurations checked: {checked}")
+    print(f"  violations of  |Star| >= min nonempty |Fan|: {fails}")
+    if worst:
+        print(f"  worst gap (|Star|-minFan, d, interior, t, |Star|, minFan): {worst}")
+    if fails == 0:
+        print("  => LOCAL CLAIM HOLDS: the star always dominates the best fan.")
+
+
+if __name__ == "__main__":
+    main()