diff --git a/papers/heawood_restrictions_on_nested_tire_graph_duals/experiments/local_star_fan.py b/papers/heawood_restrictions_on_nested_tire_graph_duals/experiments/local_star_fan.py new file mode 100644 index 0000000..cae3cb2 --- /dev/null +++ b/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 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()