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

Computation 184 -- Reducedness is a theorem of one coherence condition, and the
quotient of sec:phi-construction survives it
==================================================================================
WHY THIS FILE EXISTS.  comp 183 showed that the Born condition's whole residue is one
graph condition, REDUCEDNESS: no property has an empty distinction set and no two have
the same one.  It then declined to claim the item closed, because
sec:property-diff-math says "No further axioms are imposed on delta" and reducedness is
a further axiom, and because sec:phi-construction's appeal to the identity of
indiscernibles is made for the fibres of rho, where v can discern what delta cannot.

That objection is answered here, and the answer is NOT "assume reducedness".  It is a
different and much weaker premise, from which reducedness follows.

THE PREMISE: DELTA-FAITHFULNESS.  If v(a) != v(b) then delta(a,b).  In words: delta
records every difference the substrate carries.  It adds NO STRUCTURE.  Every disclaimer
in sec:property-diff-math survives verbatim, there being still no transitivity, no
totality, no metric on D, no topology and no ordering.  What it adds is a coherence
condition BETWEEN TWO COMPONENTS OF A TRIPLE THE BOOK ALREADY POSITS.  A delta that can
miss a difference the triple carries is not THE distinction relation of P1; it is A
relation on D with structure sitting beside it that it cannot see, which costs P1 its
central claim far more than the Born condition does.

THE DERIVATION, IN THREE STEPS, ALL PROVED AND ALL CHECKED HERE.

  1.  ADJACENT PAIRS ARE NEVER TWINS.  If delta(a,b) then b is in N(a) and, by
      irreflexivity, b is not in N(b), so N(a) != N(b).  The only pairs that can share a
      distinction set are the NON-ADJACENT ones, which delta says are not distinct.

  2.  A NON-ADJACENT TWIN PAIR WITH EQUAL v IS AN AUTOMORPHISM OF THE WHOLE TRIPLE.  The
      transposition (a b) preserves delta and preserves v, so a and b are indiscernible
      in (D, delta, v) and not merely in delta.  sec:phi-construction's own principle,
      "things that share all the same properties are the same thing", then applies
      exactly, one level below where the book already applies it.

  3.  UNDER DELTA-FAITHFULNESS THERE IS NO OTHER CASE.  A non-adjacent twin pair has
      delta(a,b) = 0, so faithfulness forbids v(a) != v(b), so every twin pair falls
      under step 2.  Collapsing them leaves a substrate in which NO TWO PROPERTIES
      SHARE A DISTINCTION SET, and comp 183's bound |D| - c <= 2^c applies to it.

AND ONE LIMIT, FOUND BY RUNNING THIS AND NOT BY WRITING IT.  comp 183 defined REDUCED
as two clauses, no property with an empty distinction set AND no two with the same one.
The argument above delivers the second clause outright and the first only up to ONE
property: two isolated properties are twins and collapse, so at most one survives, and
nothing here removes it.  The first run of part 3 reported three failures out of 1500 at
|D| = 6 and every one was exactly that, an isolated property, with zero duplicate pairs.

That costs nothing, because COMP 183'S PROOF NEVER USED THE FIRST CLAUSE.  The bound
comes from the injectivity of u -> {b : delta(u,b)} on D minus a cover, and the empty set
is a perfectly good value for it; one property may take it, no two may share it.  So comp
183's definition carries a clause stronger than its own proof, and this file delivers the
clause the proof uses.  Nothing in comp 183 moves, and part 3 now verifies the bound
directly on every collapsed substrate rather than testing the stronger predicate.

THE DEPENDENCY THAT HAD TO BE CHECKED, AND IT IS THE REASON THIS FILE IS NOT A FORMALITY.
Reducedness forbids two properties from sharing a distinction set.  rho's fibres ARE the
spacetime points, and several live passages need rho non-injective, so a fibre of size
greater than one must survive.  Does reducedness collapse every fibre to a point and make
M = D?  Part 4 answers NO, and the reason is exact:

  A FIBRE IS A CLIQUE, NOT AN INDEPENDENT SET.  eq:metric sets
  d(rho(a), rho(b)) = |T({a,b}) - tau_null|^(1/4), so same fibre means
  T({a,b}) = tau_null exactly; tau_null is in R^+ and eq:pos makes |T| vanish precisely
  on pairs carrying no distinction, so a within-fibre pair is DISTINCT, delta = 1.  By
  step 1 such a pair is never a twin.  Reducedness kills the INDEPENDENT modules, which
  are the false twins, and leaves the CLIQUE modules, which are what the quotient uses.

Measured exhaustively over every graph on 5 and 6 properties: reduced graphs carry clique
modules of size up to 6 and independent modules of size at most 1, always.  So rho stays
non-injective, sec:open-horizon's "its non-injectivity is generic" stands, and
sec:composite-systems' bipartition by preimage stands.

A false-twin pair, by contrast, has |T| = 0 != tau_null, so it sits at TWO DIFFERENT
spacetime points while carrying no distinguishing fact whatever.  That is the thing
Leibniz removes, and removing it costs the geometry nothing.

WHAT THE PREMISE DOES TO delta, WHICH PART 8 LOOKS AT RATHER THAN LEAVING.  Contraposed,
faithfulness says two properties carrying no distinction between them SHARE their
directional content.  So delta contains the complete multipartite graph on the partition
of D by v-value, and the only freedom left is inside a v-block; where v is injective,
delta is COMPLETE, which is admissible and whose atom comp 180 measured vanishing as
|D|^-0.48.  And comp 180's own counterexamples cease to exist: a star's leaves are
pairwise non-distinct, so faithfulness forces one v on all of them while they already
share one distinction set, and the star collapses to TWO properties at every size;
K_k with isolated vertices collapses to k+1.

WHAT IS ADDED, AT ITS TRUE STRENGTH.  Delta-faithfulness is a PREMISE and part 6 proves it
is not derivable from the stated axioms, by exhibiting a triple that satisfies every one
of them and violates it.  The book adopts it as P1 clause (iii) and carries it in the
premise register as an ontological clause of P1 rather than a fourth postulate, the count
of postulates still being three.  The order of discovery is recorded with it: the
condition is motivated by what makes delta the distinction relation at all, and its
consequence for Born agreement was found afterwards, in this file.  Writing it the other
way round would be the thing a critic is entitled to object to.

AND IT DOES NOT CLOSE THE BORN ITEM.  What is discharged is the GRAPH half: the failing
class comp 180 exhibited is gone, and comp 183 proves the mechanism behind it dead rather
than merely absent.  What remains is a PROOF that every admissible delta satisfies the
condition asymptotically, which comp 183 measures over the graphs it searches and does not
establish.  The register carries the missing theorem, not the answered objection.
"""

import itertools
import sys

import numpy as np


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


# --- substrate triples ----------------------------------------------------------
def nbrs(n, edges):
    N = [set() for _ in range(n)]
    for u, v in edges:
        N[u].add(v)
        N[v].add(u)
    return N


def twins(n, edges):
    """Pairs sharing a distinction set.  Returns (pair, adjacent?) for each."""
    N = nbrs(n, edges)
    E = {frozenset(e) for e in edges}
    out = []
    for a, b in itertools.combinations(range(n), 2):
        if N[a] == N[b]:
            out.append(((a, b), frozenset((a, b)) in E))
    return out


def is_reduced(n, edges):
    N = nbrs(n, edges)
    return all(N[a] for a in range(n)) and len({frozenset(s) for s in N}) == n


def faithful(n, edges, v):
    """delta records every difference: v(a) != v(b) implies delta(a,b)."""
    E = {frozenset(e) for e in edges}
    return all(frozenset((a, b)) in E
               for a, b in itertools.combinations(range(n), 2) if v[a] != v[b])


def is_triple_automorphism(n, edges, v, a, b):
    """Is the transposition (a b) an automorphism of (D, delta, v)?"""
    def swap(x):
        return b if x == a else (a if x == b else x)
    E = {frozenset(e) for e in edges}
    if {frozenset((swap(u), swap(w))) for u, w in edges} != E:
        return False
    return all(v[swap(x)] == v[x] for x in range(n))


def min_cover(n, edges):
    """Exact minimum vertex cover by search; n stays small here."""
    E = list(edges)
    for c in range(n + 1):
        for S in itertools.combinations(range(n), c):
            s = set(S)
            if all(u in s or w in s for u, w in E):
                return c
    return n


def all_graphs(n):
    pairs = list(itertools.combinations(range(n), 2))
    for mask in range(1 << len(pairs)):
        yield [p for i, p in enumerate(pairs) if (mask >> i) & 1]


def modules(n, edges):
    """Autonomous sets: every outside property is distinguished from all of S or none.
    Returns the ones of size >= 2, tagged clique / independent / mixed."""
    N = nbrs(n, edges)
    out = []
    for k in range(2, n + 1):
        for S in itertools.combinations(range(n), k):
            s = set(S)
            if not all(len(N[x] & s) in (0, k) for x in range(n) if x not in s):
                continue
            inside = [(a, b) in [(u, w) for u, w in edges] or (b, a) in
                      [(u, w) for u, w in edges]
                      for a, b in itertools.combinations(S, 2)]
            kind = "clique" if all(inside) else ("independent" if not any(inside)
                                                 else "mixed")
            out.append((S, kind))
    return out


# ---------------------------------------------------------------------------
def part1():
    rule()
    print("  1.  ADJACENT PAIRS ARE NEVER TWINS, SO EVERY TWIN PAIR IS NON-ADJACENT")
    rule()
    print("      PROOF.  Let delta(a,b).  Then b is in N(a).  By irreflexivity eq:irr,")
    print("      b is not in N(b).  So N(a) != N(b), and a, b do not share a distinction")
    print("      set.  The only candidates are pairs with delta(a,b) = 0: pairs delta")
    print("      itself says are NOT distinct.")
    print()
    print("      Checked on every graph, not a sample.")
    print()
    print(f"      {'|D|':>6}{'graphs':>12}{'twin pairs found':>20}"
          f"{'of them adjacent':>20}")
    ok = True
    for n in (4, 5, 6):
        tot = adj = cnt = 0
        for edges in all_graphs(n):
            cnt += 1
            for _, is_adj in twins(n, edges):
                tot += 1
                adj += is_adj
        ok &= (adj == 0)
        print(f"      {n:>6}{cnt:>12}{tot:>20}{adj:>20}")
    print()
    print("      Not one adjacent twin pair exists at any size.  The proof and the")
    print("      enumeration agree, and this is what makes part 4 work.")
    print()
    print(f"      -> every twin pair is non-adjacent                     : {ok}")
    print()
    return ok


def part2():
    rule()
    print("  2.  A TWIN PAIR WITH EQUAL v IS AN AUTOMORPHISM OF THE WHOLE TRIPLE")
    rule()
    print("      The objection comp 183 raised, and would not wave away, is that the")
    print("      substrate is the TRIPLE (D, delta, v), so two properties delta cannot")
    print("      separate may still differ in v, leaving Leibniz no purchase.")
    print()
    print("      That is right, and it is exactly half the story.  When v agrees, the")
    print("      transposition (a b) preserves delta AND v, so a and b are indiscernible")
    print("      in the whole triple and sec:phi-construction's own principle applies.")
    print()
    print(f"      {'triples drawn':>16}{'twin pairs':>13}{'equal v':>10}"
          f"{'automorphism of (D,delta,v)':>30}")
    rng = np.random.default_rng(20261001)
    drawn = pairs_eq = pairs_ne = auto_eq = auto_ne = 0
    for t in range(4000):
        n = int(rng.integers(5, 10))
        p = float(rng.integers(1, 6)) / 10.0
        edges = [e for e in itertools.combinations(range(n), 2) if rng.random() < p]
        v = [int(rng.integers(0, 3)) for _ in range(n)]
        drawn += 1
        for (a, b), _ in twins(n, edges):
            if v[a] == v[b]:
                pairs_eq += 1
                auto_eq += is_triple_automorphism(n, edges, v, a, b)
            else:
                pairs_ne += 1
                auto_ne += is_triple_automorphism(n, edges, v, a, b)
    print(f"      {drawn:>16}{pairs_eq + pairs_ne:>13}{pairs_eq:>10}{auto_eq:>30}")
    ok = (auto_eq == pairs_eq) and (auto_ne == 0) and pairs_eq > 0 and pairs_ne > 0
    print()
    print(f"      twin pairs with equal v   : {pairs_eq:>6}, automorphisms: {auto_eq}")
    print(f"      twin pairs with v differing: {pairs_ne:>6}, automorphisms: {auto_ne}")
    print()
    print("      EVERY equal-v twin pair is a triple-automorphism and NO differing-v twin")
    print("      pair is.  So the principle reaches exactly the pairs where v agrees, and")
    print("      the rest of the argument has to come from somewhere else.  It does, in")
    print("      part 3: under delta-faithfulness the second kind cannot exist.")
    print()
    print(f"      -> Leibniz reaches exactly the equal-v twin pairs      : {ok}")
    print()
    return ok


def part3():
    rule()
    print("  3.  DELTA-FAITHFULNESS LEAVES NO OTHER CASE, AND comp 183's BOUND FOLLOWS")
    rule()
    print("      PREMISE (delta-faithfulness).  v(a) != v(b)  implies  delta(a,b).")
    print()
    print("      PROOF.  Let a, b share a distinction set.  By part 1 they are")
    print("      non-adjacent, delta(a,b) = 0.  Faithfulness contraposed gives")
    print("      v(a) = v(b).  By part 2 the transposition is an automorphism of the")
    print("      whole triple, so a and b are indiscernible in (D, delta, v) and the")
    print("      identity of indiscernibles identifies them.  After the identification")
    print("      NO TWO PROPERTIES SHARE A DISTINCTION SET.")
    print()
    print("      WHAT IS NOT DELIVERED, AND THIS RUN IS WHERE IT WAS FOUND.  comp 183")
    print("      defined reduced with a second clause, that no property has an EMPTY")
    print("      distinction set.  Two isolated properties are twins and collapse, so at")
    print("      most one survives, and nothing here removes the last one.  The earlier")
    print("      draft of this part tested comp 183's two-clause predicate and reported")
    print("      three failures in 1500 at |D| = 6; all three were a lone isolated")
    print("      property, with zero duplicate pairs.  comp 183's PROOF never used that")
    print("      clause: the bound comes from injectivity of u -> N(u), and the empty set")
    print("      is a legal value that one property may take and no two may share.  So")
    print("      the bound is what gets verified below, directly.")
    print()
    print(f"      {'|D|':>5}{'faithful':>10}{'twin pairs':>12}{'v differs':>11}"
          f"{'no two share N':>16}{'empty N: 0 or 1':>17}{'|D|-c <= 2^c':>14}")
    rng = np.random.default_rng(11)
    ok = True
    for n in (6, 8, 10):
        made = tw = bad = inj = lone = bound = 0
        for t in range(1500):
            p = float(rng.integers(0, 6)) / 10.0
            edges = {frozenset(e) for e in itertools.combinations(range(n), 2)
                     if rng.random() < p}
            v = [int(rng.integers(0, 3)) for _ in range(n)]
            for a, b in itertools.combinations(range(n), 2):   # impose the premise
                if v[a] != v[b]:
                    edges.add(frozenset((a, b)))
            edges = [tuple(sorted(e)) for e in edges]
            if not faithful(n, edges, v):
                continue
            made += 1
            tp = twins(n, edges)
            tw += len(tp)
            bad += sum(1 for (a, b), _ in tp if v[a] != v[b])
            # collapse every class of mutual twins to one representative
            N = nbrs(n, edges)
            seen, keep = set(), []
            for x in range(n):
                key = frozenset(N[x])
                if key in seen:
                    continue
                seen.add(key)
                keep.append(x)
            idx = {x: i for i, x in enumerate(keep)}
            m = len(keep)
            q = [(idx[u], idx[w]) for u, w in edges if u in idx and w in idx]
            Nq = nbrs(m, q)
            inj += (len({frozenset(s) for s in Nq}) == m)
            lone += (sum(1 for s in Nq if not s) <= 1)
            bound += (m - min_cover(m, q) <= 2 ** min_cover(m, q))
        ok &= (bad == 0) and (inj == made) and (lone == made) and (bound == made)
        print(f"      {n:>5}{made:>10}{tw:>12}{bad:>11}{inj:>16}{lone:>17}{bound:>14}")
    print()
    print("      No faithful triple anywhere carries a twin pair whose v differs, which")
    print("      is the proof's only load-bearing step.  Every collapse leaves distinct")
    print("      distinction sets, at most one of them empty, and satisfies comp 183's")
    print("      bound directly.")
    print()
    print(f"      -> comp 183's bound follows from faithfulness + Leibniz: {ok}")
    print()
    return ok


def part4():
    rule()
    print("  4.  THE DEPENDENCY: DOES REDUCEDNESS COLLAPSE rho's FIBRES?  NO")
    rule()
    print("      This is the check that had to be made before any wording goes near P1.")
    print("      sec:phi-construction makes a spacetime point BE a fibre of rho, and the")
    print("      book leans on rho being non-injective in at least three live places:")
    print("      sec:open-horizon's 'its non-injectivity is generic rather than")
    print("      horizon-specific', sec:composite-systems' bipartition by preimage, and")
    print("      the diffeomorphism-invariance reading of rho's non-uniqueness.  If")
    print("      reducedness forced every fibre to a singleton, rho would be injective,")
    print("      M would be D, and all three would fall.")
    print()
    print("      IT DOES NOT, AND THE REASON IS EXACT.  eq:metric reads")
    print()
    print("          d(rho(a), rho(b)) = |T({a,b}) - tau_null|^(1/4),")
    print()
    print("      so a and b share a fibre exactly when T({a,b}) = tau_null.  tau_null is")
    print("      in R^+, and eq:pos makes |T| vanish precisely on pairs carrying no")
    print("      distinction, so a WITHIN-FIBRE PAIR IS DISTINCT: delta(a,b) = 1.  By")
    print("      part 1 such a pair is never a twin.  A fibre is a CLIQUE.")
    print()
    print("      A false-twin pair is the opposite case: |T| = 0, which is not tau_null,")
    print("      so the two sit at DIFFERENT spacetime points while carrying no")
    print("      distinguishing fact at all.  That is what Leibniz removes, and removing")
    print("      it costs the geometry nothing.")
    print()
    print("      Measured over every graph on 5 and 6 properties, splitting the")
    print("      autonomous sets (the candidate fibres) by type:")
    print()
    print(f"      {'|D|':>5}{'reduced graphs':>16}{'with a clique module >= 2':>28}"
          f"{'largest':>9}{'with an independent module >= 2':>33}")
    ok = True
    for n in (5, 6):
        red = cl = ind = 0
        biggest = 0
        for edges in all_graphs(n):
            if not is_reduced(n, edges):
                continue
            red += 1
            mods = modules(n, edges)
            cs = [len(S) for S, k in mods if k == "clique"]
            isz = [len(S) for S, k in mods if k == "independent"]
            if cs:
                cl += 1
                biggest = max(biggest, max(cs))
            if isz:
                ind += 1
        ok &= (ind == 0) and (cl > 0)
        print(f"      {n:>5}{red:>16}{cl:>28}{biggest:>9}{ind:>33}")
    print()
    print("      Independent modules of size two or more do not occur in a reduced graph")
    print("      at all, which is part 1 again: they would be twins.  Clique modules of")
    print("      size up to |D| are everywhere.  So the fibres the quotient needs survive")
    print("      reducedness exactly, and the ones it loses are the ones that were two")
    print("      spacetime points with nothing to tell them apart.")
    print()
    print(f"      -> rho stays non-injective under reducedness           : {ok}")
    print()
    return ok


def part5():
    rule()
    print("  5.  THE REST OF THE BOOK, CHECKED RATHER THAN ASSUMED")
    rule()
    print("      Four more places could have depended on duplicate properties.  None does.")
    print()
    print("      (a) THE BERNOULLI MEASURE AND THE BIPARTITION IT CARRIES.  mu is a")
    print("          product over D, so collapsing twins changes |D| and nothing about")
    print("          its form.  The claim that matters downstream is the one")
    print("          sec:composite-systems uses: mu factors over ANY bipartition of the")
    print("          surviving D.  Checked exhaustively on the collapsed index set:")
    print()
    print(f"          {'|D|':>7}{'splits':>9}{'bijection':>12}{'factorises to':>16}")
    ok = True
    for n in (8, 10):
        worst, sp = 0.0, 0
        for cut in range(1, n):
            A = list(range(cut))
            B = list(range(cut, n))
            sp += 1
            seen = set()
            for mask in range(1 << n):
                C = frozenset(i for i in range(n) if (mask >> i) & 1)
                seen.add((C & frozenset(A), C & frozenset(B)))
            assert len(seen) == 1 << n
            worst = max(worst, abs(2.0 ** -n - (2.0 ** -len(A)) * (2.0 ** -len(B))))
        ok &= (worst < 1e-15)
        print(f"          {n:>7}{sp:>9}{'exact':>12}{worst:>16.1e}")
    print()
    print("      (b) A1's |D_n| -> infinity.  comp 183's bound is |D| - c <= 2^c, which")
    print("          constrains the COVER, not the cardinality: c grows like log|D| and")
    print("          nothing caps |D|.  A1 is untouched.  Checked at the sizes A1 reaches:")
    print()
    print(f"          {'|D|':>10}{'cover needed':>15}{'any obstruction?':>20}")
    import math
    for D in (10 ** 6, 10 ** 40, 10 ** 80):
        c = 1
        while D - c > 2 ** c:
            c += 1
        print(f"          {('10^%d' % round(math.log10(D))):>10}{c:>15}{'none':>20}")
        ok &= (D - c <= 2 ** c)
    print()
    print("      (c) THE BALANCE COUNTING of comp 178, C(|D|,|D|/2) 2^-|D|.  It is a")
    print("          function of |D| alone and says nothing about delta, so a smaller")
    print("          reduced |D| changes the number and not the argument.")
    print()
    print("      (d) comp 182's FINDING that D is A1's sequence.  Independent of this:")
    print("          it turns on D being finite at every stage, which collapsing twins")
    print("          preserves.  Nothing in this file disturbs it or is disturbed by it.")
    print()
    print(f"      -> no other dependency found                           : {ok}")
    print()
    return ok


def part6():
    rule()
    print("  6.  WHAT IS ADDED: FAITHFULNESS IS A PREMISE, NOT A THEOREM")
    rule()
    print("      This file would be worthless if it quietly treated its own premise as")
    print("      forced.  It is not forced, and the counterexample is one line.")
    print()
    print("      Take D = {a, b}, delta empty, v(a) != v(b).  Every stated axiom holds:")
    print("      delta is symmetric eq:sym and irreflexive eq:irr, v maps into V_7, and")
    print("      sec:property-diff-math imposes nothing else.  Faithfulness fails.")
    print()
    n, edges, v = 2, [], [0, 1]
    E = {frozenset(e) for e in edges}
    sym = all(frozenset((u, w)) in E for u, w in edges)
    irr = all(frozenset((x, x)) not in E for x in range(n))
    print(f"      symmetric eq:sym                                      : {sym}")
    print(f"      irreflexive eq:irr                                    : {irr}")
    print(f"      v well defined into V_7 (equality is all that is used) : True")
    print(f"      delta-faithful                                        : "
          f"{faithful(n, edges, v)}")
    ok = sym and irr and not faithful(n, edges, v)
    print()
    print("      So delta-faithfulness is a FOURTH commitment and belongs in the premise")
    print("      register, declared.  What can be said for it, and what cannot:")
    print()
    print("      FOR.  It adds no structure.  Every disclaimer of sec:property-diff-math")
    print("      survives word for word: no transitivity, no totality, no metric on D, no")
    print("      topology, no ordering.  It is a coherence condition between two")
    print("      components of a triple the book already posits, and without it delta is")
    print("      not THE distinction relation of P1 but A relation on D with structure")
    print("      beside it that delta cannot see.")
    print()
    print("      AGAINST, and it should be printed rather than buried.  P1 is sold on")
    print("      minimality, as 'the unique weakest condition' with 'no further axioms',")
    print("      and this is an amendment to that.  The order of discovery is the honest")
    print("      defence and is recorded here: the condition is motivated by what makes")
    print("      delta the distinction relation at all, and its consequence for Born")
    print("      agreement was found afterwards, in this file, not before it.")
    print()
    print(f"      -> the premise is declared, not smuggled                : {ok}")
    print()
    return ok


def part7():
    rule()
    print("  7.  TAMPER TESTS: DOES EITHER INGREDIENT DO NOTHING?")
    rule()
    print("      Two ways this could be an empty argument.  Both are tested.")
    print()
    print("      (a) DROP FAITHFULNESS.  If reducedness followed without it the premise")
    print("      would be decoration.  Draw triples and do NOT impose it:")
    rng = np.random.default_rng(77)
    unfaithful_twins = 0
    drawn = 0
    for t in range(3000):
        n = int(rng.integers(5, 9))
        edges = [e for e in itertools.combinations(range(n), 2) if rng.random() < 0.25]
        v = [int(rng.integers(0, 3)) for _ in range(n)]
        if faithful(n, edges, v):
            continue
        drawn += 1
        unfaithful_twins += sum(1 for (a, b), _ in twins(n, edges) if v[a] != v[b])
    a_ok = unfaithful_twins > 0
    print(f"          unfaithful triples drawn                          : {drawn}")
    print(f"          twin pairs in them whose v DIFFERS                : "
          f"{unfaithful_twins}")
    print("          Those are the pairs Leibniz cannot touch, and they exist in")
    print(f"          quantity without the premise, so the premise does work : {a_ok}")
    print()
    print("      (b) DROP LEIBNIZ.  Faithfulness alone forbids a twin pair from differing")
    print("      in v; it does not by itself remove the pair.  Count faithful triples")
    print("      that still carry a twin pair, which is what is left to identify:")
    rng = np.random.default_rng(78)
    carry = made = 0
    for t in range(3000):
        n = int(rng.integers(5, 9))
        edges = {frozenset(e) for e in itertools.combinations(range(n), 2)
                 if rng.random() < 0.25}
        v = [0] * n
        edges = [tuple(sorted(e)) for e in edges]
        if not faithful(n, edges, v):
            continue
        made += 1
        carry += bool(twins(n, edges))
    b_ok = carry > 0
    print(f"          faithful triples drawn                            : {made}")
    print(f"          of them still carrying a twin pair                 : {carry}")
    print("          So faithfulness narrows the case and Leibniz closes it; neither")
    print(f"          ingredient is redundant                            : {b_ok}")
    print()
    ok = a_ok and b_ok
    print(f"      -> both ingredients are load-bearing                   : {ok}")
    print()
    return ok


def part8():
    rule()
    print("  8.  WHAT THE PREMISE DOES TO THE SHAPE OF delta, WHICH HAD TO BE LOOKED AT")
    rule()
    print("      Adopting a condition without asking what it implies would be the same")
    print("      mistake this file was written to avoid.  Faithfulness is a condition ON")
    print("      delta, so it changes which distinction graphs exist.  Three consequences,")
    print("      all measured.")
    print()
    print("      (a) THE NON-DISTINCTIONS REFINE THE v-PARTITION.  Contraposing the")
    print("      premise: delta(a,b) = 0 implies v(a) = v(b).  So delta CONTAINS the")
    print("      complete multipartite graph on the partition of D by v-value, and the")
    print("      only freedom left is inside a v-block.")
    print()
    rng = np.random.default_rng(3)
    drawn = viol = 0
    for t in range(3000):
        n = int(rng.integers(4, 9))
        v = [int(rng.integers(0, 3)) for _ in range(n)]
        E = {frozenset(e) for e in itertools.combinations(range(n), 2)
             if rng.random() < 0.3}
        for a, b in itertools.combinations(range(n), 2):
            if v[a] != v[b]:
                E.add(frozenset((a, b)))
        drawn += 1
        viol += sum(1 for a, b in itertools.combinations(range(n), 2)
                    if frozenset((a, b)) not in E and v[a] != v[b])
    a_ok = (viol == 0) and drawn > 0
    print(f"          faithful triples drawn                            : {drawn}")
    print(f"          non-distinct pairs whose v differs                : {viol}")
    print()
    print("      (b) IF v IS INJECTIVE, delta IS COMPLETE.  |D| is around 10^80 and V_7")
    print("      is a real 7-space, so an injective v is available, and then every pair")
    print("      is distinguished.  This is worth stating plainly rather than leaving a")
    print("      reader to find it: in that regime delta carries no information beyond")
    print("      |D| and the whole structure sits in v.")
    print()
    print(f"          {'|D|':>7}{'pairs in delta':>17}{'all pairs':>12}{'complete':>11}"
          f"{'reduced':>10}{'atom':>10}")
    b_ok = True
    for n in (5, 8, 12):
        E = [tuple(sorted(e)) for e in itertools.combinations(range(n), 2)]
        comp = len(E) == n * (n - 1) // 2
        t = np.zeros(1 << n, dtype=np.int32)
        m = np.arange(1 << n, dtype=np.int64)
        for u, w in E:
            t += (((m >> u) & 1) * ((m >> w) & 1)).astype(np.int32)
        atom = int(np.bincount(t).max()) / (1 << n)
        b_ok &= comp and is_reduced(n, E)
        print(f"          {n:>7}{len(E):>17}{n * (n - 1) // 2:>12}{str(comp):>11}"
              f"{str(is_reduced(n, E)):>10}{atom:>10.4f}")
    print()
    print("      That regime is ADMISSIBLE and its Born behaviour is already known:")
    print("      comp 180 measured the complete graph's atom vanishing as |D|^-0.48, and")
    print("      it is reduced, having no two distinction sets alike.  So the premise")
    print("      does not break the Born side in its own extreme case.")
    print()
    print("      (c) AND comp 180's CLEANEST COUNTEREXAMPLE IS NOT A FAITHFUL SUBSTRATE.")
    print("      In a star the leaves are pairwise non-distinct, so faithfulness forces")
    print("      them ALL to share one v, and they already share one distinction set, so")
    print("      they are one property.  A star collapses to two properties at EVERY")
    print("      size.  The counterexample does not survive the premise even before")
    print("      comp 183's bound is reached for:")
    print()
    print(f"          {'star |D|':>12}{'distinct distinction sets':>28}{'|D| after':>12}")
    c_ok = True
    for n in (5, 10, 20, 100):
        E = [(0, i) for i in range(1, n)]
        N = nbrs(n, E)
        k = len({frozenset(s) for s in N})
        c_ok &= (k == 2)
        print(f"          {n:>12}{k:>28}{k:>12}")
    print()
    print("      The same happens to K_k with isolated vertices: the isolated properties")
    print("      are pairwise non-distinct, so they share one v and one distinction set,")
    print("      the empty one, and collapse to a single property.")
    print()
    print(f"          {'K_k + iso, |D|':>16}{'k':>4}{'distinct sets':>16}{'|D| after':>12}")
    for n, k in ((10, 4), (20, 4), (10, 6), (40, 6)):
        E = list(itertools.combinations(range(k), 2))
        N = nbrs(n, E)
        m = len({frozenset(s) for s in N})
        c_ok &= (m == k + 1)
        print(f"          {n:>16}{k:>4}{m:>16}{m:>12}")
    print()
    print("      So both of comp 180's families are removed by the premise itself, and")
    print("      comp 183's cover bound is what rules out everything of that SHAPE rather")
    print("      than only these two instances.")
    print()
    ok = a_ok and b_ok and c_ok
    print(f"      -> the premise's effect on delta is stated, not left   : {ok}")
    print()
    return ok


def main():
    rule()
    print("  COMPUTATION 184 -- REDUCEDNESS FOLLOWS FROM delta RECORDING WHAT v CARRIES")
    rule()
    print()
    r = [part1(), part2(), part3(), part4(), part5(), part6(), part7(),
         part8()]
    rule()
    print("  SUMMARY")
    rule()
    print(f"  1. adjacent pairs are never twins, proved and enumerated     : {r[0]}")
    print(f"  2. an equal-v twin pair is a triple-automorphism             : {r[1]}")
    print(f"  3. faithfulness + Leibniz give comp 183's bound, not clause 1: {r[2]}")
    print(f"  4. rho stays non-injective: a fibre is a clique, not a twin  : {r[3]}")
    print(f"  5. no other dependency on duplicate properties found         : {r[4]}")
    print(f"  6. faithfulness is a premise, exhibited as underivable       : {r[5]}")
    print(f"  7. tamper tests: both ingredients load-bearing               : {r[6]}")
    print(f"  8. what it does to delta: star and K_k+iso cease to exist    : {r[7]}")
    print()
    print("""  RESULT.  comp 183 left the Born condition waiting on reducedness and declined
  to assume it, because sec:property-diff-math imposes no further axiom on delta and
  because v can discern what delta cannot.  Reducedness need not be assumed.  It
  follows from ONE coherence condition, that delta record every difference the
  substrate carries: if v(a) != v(b) then delta(a,b).

  The chain is three steps and each is proved and enumerated here.  Irreflexivity
  makes every twin pair non-adjacent, so faithfulness forces its two properties to
  share their directional content, so the transposition is an automorphism of the
  whole triple (D, delta, v) and not merely of delta.  sec:phi-construction's own
  principle then identifies them, one level below where the book already applies it,
  and what is left has no two properties sharing a distinction set.

  ONE CLAUSE IS NOT DELIVERED, AND RUNNING THIS IS HOW IT WAS FOUND.  comp 183
  defined reduced with a second clause, no property with an EMPTY distinction set.
  Two isolated properties are twins and collapse, so at most one survives, and
  nothing here removes the last.  The first run reported exactly that, three times
  in 1500 at |D| = 6, with zero duplicate pairs in any of them.  It costs nothing:
  comp 183's PROOF never used that clause, the bound resting on injectivity of
  u -> N(u), for which the empty set is a legal value one property may take and no
  two may share.  comp 183's definition is stronger than comp 183's proof; nothing
  in it moves, and part 3 verifies the bound itself on every collapsed substrate.

  The dependency that had to be checked is rho.  A spacetime point IS a fibre, and
  three live passages need rho non-injective, so reducedness had to leave fat fibres
  alone.  It does, exactly.  eq:metric makes a within-fibre pair satisfy
  T({a,b}) = tau_null, and tau_null being positive while eq:pos vanishes only on
  pairs carrying no distinction, a within-fibre pair is DISTINCT.  A fibre is a
  clique, and part 1 says a clique holds no twins.  Over every graph on five and six
  properties, reduced graphs carry clique modules of every size and independent
  modules of size at most one.  What reducedness removes is the opposite object: a
  pair with |T| = 0, which is not tau_null, hence sitting at two DIFFERENT spacetime
  points with no fact whatever to tell them apart.

  Nothing else in the book depends on duplicates.  The Bernoulli measure stays a
  product, A1's cardinality is unconstrained because comp 183's bound constrains the
  cover rather than |D|, the balance counting is a function of |D| alone, and comp
  182's decision turns on finiteness, which collapsing twins preserves.

  Part 8 asks what the premise does to delta rather than leaving it.  Contraposed, it
  says two properties carrying no distinction share their directional content, so
  delta contains the complete multipartite graph on the v-partition and the freedom
  left is inside a v-block; where v is injective delta is complete, which is
  admissible and whose atom vanishes as |D|^-0.48.  And comp 180's own counterexamples
  cease to exist: a star collapses to TWO properties at every size, K_k with isolated
  vertices to k+1.

  What this does NOT do is make the condition free.  Part 6 exhibits a triple
  satisfying every stated axiom and violating faithfulness, so it is a premise; the
  book adopts it as P1 clause (iii) and carries it in the register as a clause of P1
  rather than a fourth postulate, with the order of discovery printed beside it.

  Nor does it close the Born item.  What is discharged is the GRAPH half.  What is
  left is a proof that every admissible delta satisfies the condition asymptotically,
  which comp 183 measures over the graphs it searches and does not establish, so item
  1's second disjunct stays open with it.  The register carries the missing theorem
  rather than the answered objection.""")
    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)
