#!/usr/bin/env python3
"""
PROVENANCE: PROOF

Computation 187 -- Only the atom eq:pos forces survives a generic admissible T, and that
is the one comp 183 bounds
=========================================================================================
WHY THIS FILE EXISTS.  comps 145, 180 and 183 all measure the Born obstruction as ATOMS in
the law of |T(C)|, and all three measure them on ONE object, the induced edge count

    T_ex(C) = |{(a,b) : a,b in C, a != b, delta(a,b)}|,

which sec:asymmetric-tension introduces as "a minimal example for the MAGNITUDE
structure".  T_ex is integer-valued, and an integer-valued functional on 2^|D| subsets has
ties FORCED on it by counting alone: there are only O(|D|^2) possible edge counts.  So the
question nobody had asked is which of the measured atoms are properties of the THEORY and
which are properties of the EXEMPLAR.

WHAT THE BOOK ALREADY SAYS, and it is the whole licence this file needs.  \\Pref{2} makes T
V_7-valued, so |T(C)| is a REAL number; and sec:asymmetric-tension says outright that T_ex
is not the theory's T:

    "Neither is the unique form of T; an admissible T pairs a magnitude satisfying
     eq:pos--eq:mon with a v-inherited V_7-direction"

    "the magnitude ranges over a family whose dimension grows as 2^|D|.  ANY
     order-preserving function on the configuration lattice that vanishes exactly on the
     distinction-free configurations is admissible, with T_ex ONE REPRESENTATIVE AMONG
     THEM"

So no new postulate is needed to ask this question, and none is used.  Everything below is
\\Pref{2} and eq:pos.

THE SPLIT, AND IT IS EXACT.  Call an atom FORCED if every admissible T has it.

    eq:pos says |T(C)| = 0 if and only if C has no distinct pairs.  That is not freedom;
    it is the definition of admissibility.  So EVERY admissible T puts the value 0 on
    exactly the distinction-free configurations, which are the INDEPENDENT SETS of
    (D, delta), and the atom there has mass mu(independent) whatever T is.

    Every other tie is a coincidence of the representative and can be removed.

Hence, for every admissible T,   largest atom  >=  mu(independent sets),
with equality for a generic one.  Part 3 measures it: taking T with positive real edge
weights, admissible by inspection and checked here against eq:pos and eq:mon, the largest
atom equals mu(independent) EXACTLY in every family comp 180 tabulated.

    family        |D|   atom, T_ex   atom, generic T   mu(independent)
    complete       14       0.2095            0.0009            0.0009
    cycle          14       0.1897            0.0515            0.0515
    Erdos-Renyi    14       0.0681            0.0068            0.0068
    star           14       0.5001            0.5001            0.5001
    K4 + isolated  14       0.3750            0.3125            0.3125
    K6 + isolated  14       0.3125            0.1094            0.1094

TWO CONSEQUENCES, ONE A CORRECTION AND ONE AN UPGRADE.

CORRECTION, to comp 180 and to the sentence it put in sec:crossing-born-consistency.  That
row reads "The regular graphs' floor vanishes, as |D|^-0.5, slower than generic but
vanishing".  The exponent is an artefact of integrality: under a generic admissible T the
complete graph's atom is 9e-4 at |D| = 14 and falling EXPONENTIALLY, not 0.21 falling as a
square root.  comp 180's VERDICT on those families is unchanged, they pass either way, but
its RATE is a property of T_ex and is corrected here.

UPGRADE, to comp 183.  Its bound is largest atom >= 2^-c with c the vertex cover number,
and the proof runs through the configurations contained in the cover's complement, which
are exactly independent sets.  So the chain is

    largest atom  >=  mu(independent)  >=  2^-c,

and BOTH steps are T-independent.  comp 183's result therefore holds for EVERY admissible
T and not only for the exemplar it was measured on, which is strictly stronger than it
claimed.  It also explains, rather than merely re-measuring, why comp 183's search for a
second mechanism found none: under a generic T there IS no second mechanism, the only
atom being the forced one.

WHAT THIS DOES NOT DO.  It does not remove the need for \\Pref{1}(iii).  The atom that
survives is precisely the atom reducedness kills, and the star still sits at 1/2 under
every admissible T.  So \\Pref{2}'s freedom in T disposes of the artefacts and sharpens
what is left; it does not dispose of what is left.
"""

import itertools
import sys
from collections import Counter

import numpy as np

SIZES = (10, 12, 14)
FAMILIES = ("complete", "cycle", "erdos", "star", "K4+iso", "K6+iso")


def rule():
    print("=" * 100)


def family(kind, D):
    if kind == "complete":
        return list(itertools.combinations(range(D), 2))
    if kind == "cycle":
        return [(i, (i + 1) % D) for i in range(D)]
    if kind == "star":
        return [(0, i) for i in range(1, D)]
    if kind == "K4+iso":
        return list(itertools.combinations(range(4), 2))
    if kind == "K6+iso":
        return list(itertools.combinations(range(6), 2))
    if kind == "erdos":
        r = np.random.default_rng(5)
        return [e for e in itertools.combinations(range(D), 2) if r.random() < 0.5]
    raise ValueError(kind)


def bits_of(D):
    m = np.arange(1 << D, dtype=np.int64)
    return np.array([(m >> a) & 1 for a in range(D)], dtype=np.int8)


def tension(D, edges, weights=None, bits=None):
    """T_ex when weights is None; a generic admissible magnitude otherwise."""
    bits = bits_of(D) if bits is None else bits
    out = np.zeros(1 << D, dtype=np.float64)
    for i, (u, v) in enumerate(edges):
        out += (1.0 if weights is None else weights[i]) * (bits[u] * bits[v])
    return out


def largest_atom(vals):
    return max(Counter(np.round(vals, 9).tolist()).values()) / len(vals)


def mu_independent(D, edges, bits=None):
    """mu of the configurations with no distinct pair, i.e. the independent sets."""
    return float(np.mean(tension(D, edges, bits=bits) == 0.0))


# ---------------------------------------------------------------------------
def part1():
    rule()
    print("  1.  THE FREEDOM IS THE BOOK'S OWN, AND IT IS LARGE")
    rule()
    print("      comps 145, 180 and 183 measure the Born obstruction on ONE object, the")
    print("      induced edge count T_ex, which sec:asymmetric-tension introduces as 'a")
    print("      minimal example for the MAGNITUDE structure'.  \\Pref{2} makes T")
    print("      V_7-valued, so |T(C)| is a REAL number, and the same section says what")
    print("      the admissible family is:")
    print()
    print("          'Neither is the unique form of T' ... 'the magnitude ranges over a")
    print("           family whose dimension grows as 2^|D|.  ANY order-preserving")
    print("           function on the configuration lattice that vanishes exactly on the")
    print("           distinction-free configurations is admissible, with T_ex ONE")
    print("           REPRESENTATIVE AMONG THEM'")
    print()
    print("      T_ex IS INTEGER-VALUED, and that alone forces ties: 2^|D| subsets carry")
    print("      only O(|D|^2) possible edge counts, so by pigeonhole almost every value")
    print("      is shared.  The question is which measured atoms belong to the THEORY")
    print("      and which to the EXEMPLAR.  Counting the collisions integrality forces:")
    print()
    print(f"      {'|D|':>6}{'configurations':>17}{'distinct T_ex values':>23}"
          f"{'mean tie size':>16}")
    ok = True
    for D in SIZES:
        E = family("erdos", D)
        v = tension(D, E)
        distinct = len(set(v.tolist()))
        ok &= distinct < (1 << D)
        print(f"      {D:>6}{1 << D:>17}{distinct:>23}{(1 << D) / distinct:>16.1f}")
    print()
    print("      At |D| = 14 the exemplar maps 16384 configurations onto a few dozen")
    print("      values.  No conclusion about ties can be read off that without first")
    print("      asking which of them survive the freedom the book states.")
    print()
    print(f"      -> the measured atoms are the exemplar's until shown otherwise: {ok}")
    print()
    return ok


def part2():
    rule()
    print("  2.  THE SPLIT IS EXACT: eq:pos FORCES ONE ATOM AND FREES EVERY OTHER")
    rule()
    print("      Call an atom FORCED if every admissible T has it.")
    print()
    print("      eq:pos is  |T(C)| = 0  <=>  C has no distinct pairs.  That is not a")
    print("      choice, it is the definition of admissibility.  So EVERY admissible T")
    print("      puts the value 0 on exactly the distinction-free configurations, which")
    print("      are the INDEPENDENT SETS of (D, delta), and the atom there has mass")
    print("      mu(independent) whatever T is.  Every other tie is a coincidence of the")
    print("      representative, and a representative taking real values generically has")
    print("      none.  Hence, for every admissible T,")
    print()
    print("          largest atom  >=  mu(independent sets),")
    print()
    print("      with equality for a generic one.  THE INEQUALITY IS THE WHOLE CONTENT:")
    print("      it says the Born obstruction cannot be argued away by choosing T, and")
    print("      it says nothing else can be argued INTO it either.")
    print()
    print("      The admissible representative used below is T with positive real edge")
    print("      weights.  Admissible by inspection, and checked rather than asserted:")
    print()
    print(f"      {'family':>12}{'|D|':>5}{'eq:pos holds':>15}{'eq:mon holds':>15}")
    rng = np.random.default_rng(20261001)
    ok = True
    for kind in FAMILIES:
        for D in (10, 12):
            E = family(kind, D)
            bits = bits_of(D)
            w = rng.random(len(E)) + 0.5
            t = tension(D, E, w, bits)
            zero_ok = bool(np.all((t == 0.0) == (tension(D, E, bits=bits) == 0)))
            mon_ok = True
            for a in range(D):
                add = bits[a] == 0
                idx = np.arange(1 << D)[add]
                mon_ok &= bool(np.all(t[idx | (1 << a)] >= t[idx] - 1e-12))
            ok &= zero_ok and mon_ok
            if D == 12:
                print(f"      {kind:>12}{D:>5}{str(zero_ok):>15}{str(mon_ok):>15}")
    print()
    print("      eq:pos and eq:mon hold for the weighted representative on every family,")
    print("      so it is an admissible T and not a convenient non-member.")
    print()
    print(f"      -> the forced atom is mu(independent), the rest is free : {ok}")
    print()
    return ok


def part3():
    rule()
    print("  3.  MEASURED: THE GENERIC ATOM IS mu(INDEPENDENT), EXACTLY")
    rule()
    print(f"      {'family':>12}{'|D|':>5}{'atom, T_ex':>13}{'atom, generic T':>18}"
          f"{'mu(independent)':>18}{'equal?':>9}")
    rng = np.random.default_rng(1)
    ok = True
    for kind in FAMILIES:
        for D in (10, 14):
            E = family(kind, D)
            bits = bits_of(D)
            w = rng.random(len(E)) + 0.5
            a_ex = largest_atom(tension(D, E, bits=bits))
            a_w = largest_atom(tension(D, E, w, bits))
            mu = mu_independent(D, E, bits)
            eq = abs(a_w - mu) < 1e-12
            ok &= eq
            print(f"      {kind:>12}{D:>5}{a_ex:>13.4f}{a_w:>18.4f}{mu:>18.4f}"
                  f"{str(eq):>9}")
    print()
    print("      Not approximately: EXACTLY, in every row.  Under a generic admissible T")
    print("      the only tie left is the one eq:pos forces.")
    print()
    print("      AND IT IS NOT ONE LUCKY DRAW.  Twenty independent weightings per family:")
    print()
    print(f"      {'family':>12}{'draws':>8}{'all equal to mu(independent)?':>32}")
    for kind in FAMILIES:
        D = 12
        E = family(kind, D)
        bits = bits_of(D)
        mu = mu_independent(D, E, bits)
        agree = 0
        for s in range(20):
            r = np.random.default_rng(900 + s)
            w = r.random(len(E)) + 0.5
            agree += abs(largest_atom(tension(D, E, w, bits)) - mu) < 1e-12
        ok &= (agree == 20)
        print(f"      {kind:>12}{20:>8}{('yes, 20/20' if agree == 20 else '%d/20' % agree):>32}")
    print()
    print(f"      -> the generic atom equals the forced atom              : {ok}")
    print()
    return ok


def part4():
    rule()
    print("  4.  A CORRECTION TO comp 180's RATE, NOT TO ITS VERDICT")
    rule()
    print("      comp 180's row, repeated in sec:crossing-born-consistency, reads: 'The")
    print("      regular graphs' floor VANISHES, as |D|^-0.5, slower than generic but")
    print("      vanishing.'  The verdict is right and is not disturbed.  THE EXPONENT")
    print("      IS AN ARTEFACT OF INTEGRALITY.")
    print()
    print(f"      {'family':>12}{'T_ex: atom and fit':>26}{'generic T: atom and fit':>29}")
    rng = np.random.default_rng(7)
    ok = True
    for kind in ("complete", "cycle", "erdos"):
        ex, gen = [], []
        for D in SIZES:
            E = family(kind, D)
            bits = bits_of(D)
            w = rng.random(len(E)) + 0.5
            ex.append(largest_atom(tension(D, E, bits=bits)))
            gen.append(largest_atom(tension(D, E, w, bits)))
        se = float(np.polyfit(np.log(SIZES), np.log(ex), 1)[0])
        sg = float(np.polyfit(np.log(SIZES), np.log(gen), 1)[0])
        ok &= sg < se - 0.5
        print(f"      {kind:>12}{('%.4f  ~|D|^%+.2f' % (ex[-1], se)):>26}"
              f"{('%.5f  ~|D|^%+.2f' % (gen[-1], sg)):>29}")
    print()
    print("      The complete graph's atom is 0.21 falling as a square root on the")
    print("      exemplar and 9e-4 falling far faster on a generic T, because its")
    print("      independent sets are only the empty set and the singletons, a mass of")
    print("      (|D|+1)/2^|D|.  So those families pass for a much better reason than")
    print("      comp 180 recorded, and the book's sentence is corrected to say so.")
    print()
    print("      THE FAILING FAMILIES STILL FAIL, and at exactly the forced value: the")
    print("      star at 1/2 + 2^-|D|, which is mu(centre not in C) plus the lone")
    print("      configuration that takes the centre and no leaf; K_k with isolated")
    print("      vertices at (1 + k)/2^k.  Checked against those closed forms:")
    print()
    print(f"      {'family':>12}{'|D|':>5}{'measured':>12}{'closed form':>14}")
    for kind, D, want in (("star", 12, 0.5 + 2.0 ** -12), ("star", 14, 0.5 + 2.0 ** -14),
                          ("K4+iso", 12, 5 / 16), ("K6+iso", 12, 7 / 64)):
        E = family(kind, D)
        bits = bits_of(D)
        r = np.random.default_rng(3)
        w = r.random(len(E)) + 0.5
        got = largest_atom(tension(D, E, w, bits))
        ok &= abs(got - want) < 1e-12
        print(f"      {kind:>12}{D:>5}{got:>12.6f}{want:>14.6f}")
    print()
    print(f"      -> comp 180's rate corrected, its verdict untouched      : {ok}")
    print()
    return ok


def part5():
    rule()
    print("  5.  AN UPGRADE TO comp 183: ITS BOUND HOLDS FOR EVERY ADMISSIBLE T")
    rule()
    print("      comp 183 proves largest atom >= 2^-c, c the vertex cover number, and the")
    print("      proof runs through the configurations contained in the cover's")
    print("      complement.  Those are exactly INDEPENDENT SETS.  So the chain is")
    print()
    print("          largest atom  >=  mu(independent)  >=  2^-c,")
    print()
    print("      and both steps are T-INDEPENDENT: the first is eq:pos, the second is")
    print("      counting.  comp 183 was measured on T_ex and therefore claimed less than")
    print("      it had proved; the bound holds for EVERY admissible T.")
    print()
    print(f"      {'family':>12}{'|D|':>5}{'cover c':>9}{'2^-c':>10}"
          f"{'mu(independent)':>18}{'chain holds':>13}")
    ok = True
    for kind in FAMILIES:
        D = 12
        E = family(kind, D)
        bits = bits_of(D)
        c = None
        for k in range(D + 1):
            for S in itertools.combinations(range(D), k):
                s = set(S)
                if all(u in s or v in s for u, v in E):
                    c = k
                    break
            if c is not None:
                break
        mu = mu_independent(D, E, bits)
        holds = (mu >= 2.0 ** -c - 1e-12)
        ok &= holds
        print(f"      {kind:>12}{D:>5}{c:>9}{2.0 ** -c:>10.5f}{mu:>18.5f}"
              f"{str(holds):>13}")
    print()
    print("      AND IT EXPLAINS A MEASUREMENT RATHER THAN REPEATING IT.  comp 183")
    print("      searched for a second mechanism over reduced graphs and found none,")
    print("      reporting that as measured and not proved.  Under a generic admissible T")
    print("      there IS no second mechanism to find: the only atom is the forced one,")
    print("      so the cover bound is not one mechanism among several but the whole of")
    print("      the obstruction.  The search was looking for something that cannot")
    print("      exist, which is why it kept not finding it.")
    print()
    print(f"      -> comp 183's bound is T-independent, and complete       : {ok}")
    print()
    return ok


def part6():
    rule()
    print("  6.  WHAT THIS DOES NOT DO, AND A TAMPER TEST ON THE ADMISSIBILITY ITSELF")
    rule()
    print("      IT DOES NOT REMOVE \\Pref{1}(iii).  The atom that survives is precisely")
    print("      the one reducedness kills.  The star keeps 1/2 under EVERY admissible T,")
    print("      because half of all configurations omit its centre and carry no")
    print("      distinction at all, and eq:pos sends every one of them to zero.  So")
    print("      \\Pref{2}'s freedom disposes of the artefacts and sharpens what is left;")
    print("      it does not dispose of what is left.")
    print()
    print("      TAMPER TEST.  If the result held for any weighting whatever, the appeal")
    print("      to ADMISSIBILITY would be decoration.  Allow a weight to vanish, which")
    print("      breaks eq:pos because a configuration carrying that distinction and no")
    print("      other now has |T| = 0:")
    print()
    D = 12
    E = family("erdos", D)
    bits = bits_of(D)
    mu = mu_independent(D, E, bits)
    r = np.random.default_rng(11)
    w_ok = r.random(len(E)) + 0.5
    w_bad = w_ok.copy()
    w_bad[: max(1, len(E) // 3)] = 0.0
    a_ok = largest_atom(tension(D, E, w_ok, bits))
    a_bad = largest_atom(tension(D, E, w_bad, bits))
    pos_bad = bool(np.all((tension(D, E, w_bad, bits) == 0.0)
                          == (tension(D, E, bits=bits) == 0)))
    print(f"      {'weighting':>34}{'eq:pos':>9}{'atom':>10}{'mu(ind)':>10}")
    print(f"      {'all weights positive (admissible)':>34}{'True':>9}{a_ok:>10.5f}"
          f"{mu:>10.5f}")
    print(f"      {'a third of the weights set to zero':>34}{str(pos_bad):>9}"
          f"{a_bad:>10.5f}{mu:>10.5f}")
    print()
    print("      The inadmissible weighting breaks eq:pos and its atom leaves")
    print("      mu(independent), so the equality in part 3 is a consequence of")
    print("      admissibility and not of using real numbers.  That is the step the")
    print("      argument actually rests on.")
    print()
    ok = (abs(a_ok - mu) < 1e-12) and (not pos_bad) and (abs(a_bad - mu) > 1e-9)
    print(f"      -> admissibility is load-bearing, not decoration        : {ok}")
    print()
    return ok


def main():
    rule()
    print("  COMPUTATION 187 -- ONLY THE ATOM eq:pos FORCES SURVIVES A GENERIC T")
    rule()
    print()
    r = [part1(), part2(), part3(), part4(), part5(), part6()]
    rule()
    print("  SUMMARY")
    rule()
    print(f"  1. the measured atoms were the exemplar's, and T_ex is integral  : {r[0]}")
    print(f"  2. eq:pos forces one atom, mu(independent), and frees the rest   : {r[1]}")
    print(f"  3. the generic atom equals that forced atom, exactly, 20/20      : {r[2]}")
    print(f"  4. comp 180's RATE corrected; its verdict untouched              : {r[3]}")
    print(f"  5. comp 183's bound upgraded: T-independent, and the whole story : {r[4]}")
    print(f"  6. P1(iii) still needed; admissibility is load-bearing           : {r[5]}")
    print()
    print("""  RESULT.  Every atom this book has measured in the Born obstruction was
  measured on T_ex, the induced edge count, which sec:asymmetric-tension introduces as
  a minimal EXAMPLE and names as one representative of a family whose dimension grows
  as 2^|D|.  T_ex is integer-valued, so ties are forced on it by counting alone: at
  |D| = 14 it maps 16384 configurations onto a few dozen values.  \\Pref{2} makes the
  theory's T V_7-valued, hence |T(C)| real, so the question of which atoms are the
  theory's and which are the exemplar's is the book's own and needs no new premise.

  The split is exact.  eq:pos says |T(C)| = 0 exactly on the configurations with no
  distinct pairs, which is admissibility rather than choice, so every admissible T
  carries an atom of mass mu(independent sets) and no other tie is forced.  Measured
  with positive real edge weights, admissible and checked here against eq:pos and
  eq:mon, the largest atom equals mu(independent) EXACTLY in every family comp 180
  tabulated, over twenty independent weightings each.

  Two things follow.  comp 180's RATE for the passing families is an artefact of
  integrality: the complete graph's atom is not 0.21 falling as |D|^-0.5 but 9e-4
  falling exponentially, its independent sets being only the empty set and the
  singletons.  Its verdict is untouched and the book's sentence is corrected to the
  better reason.  And comp 183's bound is UPGRADED: its proof runs through the
  configurations inside a cover's complement, which are independent sets, so the chain
  largest atom >= mu(independent) >= 2^-c is T-independent at both steps and holds for
  every admissible T rather than for the exemplar it was measured on.  That also
  explains, rather than re-measures, why comp 183's search for a second mechanism
  found none: under a generic T there is none, so the cover bound is the whole
  obstruction and not one mechanism among several.

  None of this removes \\Pref{1}(iii).  The surviving atom is exactly the one
  reducedness kills, and the star holds 1/2 under every admissible T.  \\Pref{2}'s
  freedom disposes of the artefacts and sharpens what is left; it does not dispose of
  what is left.""")
    print()
    return all(r)


if __name__ == "__main__":
    # Exit only on FAILURE.  The website runs these in the browser under Pyodide,
    # where SystemExit is fatal even at status 0: it tears the runtime down, and the
    # page prints ERROR after output that was in fact correct.  Falling off the end
    # hands the build gates the same status 0, and a failure still exits 1.
    if not main():
        sys.exit(1)
