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

Computation 182, M7's fork is decided, and the missing number is named
======================================================================
WHAT THIS DOES.  comp 179 left M7 as a fork and said the book had not chosen:

  (A) D is A1's sequence.  The magnitude is divergent rather than free, and what
      is owed is a NORMALISATION.
  (B) D is one fixed substrate of finite spacing.  comp 167 stands entire and
      what is owed is a DENSITY.

This file decides it.  (A) is forced and (B) is not available, for a reason the
book supplies itself and in one line.  It then follows the consequence through
and finds that the forced normalisation does NOT leave a finite object, which
corrects the most optimistic reading of comp 179 part 4, and that what is left
over is a single named number of a familiar kind.

AND IT CORRECTS ITS OWN PREDECESSOR.  comp 179 part 1 said:

    "And it is the same map: eq:Pimunu sums over pairs of D through rho, and
     the body defines rho: D -> M once, written rho_n: D_n -> M under A1.
     One substrate, one realisation map."

The first half is right and the second is too strong.  The book defines TWO maps
with incompatible types and calls both the realisation map:

  rho   (sec:phi-construction)   SURJECTIVE quotient; M is DERIVED as D/~; "a
                                 spacetime point IS a fibre of rho"; the section
                                 spends four paragraphs establishing that M is
                                 not a container given in advance, and calls the
                                 container reading "a foundational circularity".
  rho_n (sec:mosco-conditional)  rho_n: D_n -> M = R x S^3, with "image rho_n(D_n)
                                 asymptotically equidistributed".  D_n is finite
                                 and R x S^3 is uncountable, so this map CANNOT be
                                 surjective, and M is given in advance: exactly
                                 the container.

And the book says so itself, in the Mosco-step assumption list:
"(i) The realisation map rho: D -> M PRESUMES the target manifold M is smooth and
finite-dimensional."  That is the container reading, listed as an assumption,
three chapters after the section that denies it.

This is the same class of error as the seven of 2026-09-29/30: a sentence stating
what a result rests on, not a number.  No number in comp 179 changes.

THE DECISION, AND IT IS SHORT.  A finite set has no uncountable quotient.  |D_n|
is finite at every n (A1 says |D_n| -> infinity, the Bernoulli product is over D,
sec:born-agreement enumerates all 2^|D| configurations, comp 178 evaluates
C(|D|,|D|/2)).  So M = D_n/~ is finite at every n and is not a smooth 4-manifold
at any of them.  But sec:einstein writes nabla^mu Pi_mn = 0, a covariant
derivative on a smooth M.  So eq:Pimunu cannot be read at a fixed finite stage:
(B) is not an unstated premise, it is an unavailable one.  D in eq:Pimunu is A1's
sequence, and M = R x S^3 is the limit of the finite quotients, not the quotient
of any one of them.

WHAT A1 ADDS, AND WHAT IT DOES NOT.  |D_n| a_n^4 -> V_M counts PROPERTIES against
VOLUME.  If rho_n had fibres of constant size f the point count would be |D_n|/f
and the constant would be absorbed; the exponent below is unchanged, so nothing
here rests on the fibres being singletons.  What does rest on it is Step 1's
identification of a point WITH a fibre: at f = 1 a point is one property and the
Leibniz reading loses its content, though no result uses it.  Recorded, not
resolved.

THE CONSEQUENCE, AND IT IS NOT THE COMFORTABLE ONE.  comp 179 part 4 measured
that dividing by the pair count converges while dividing by the site count does
not, and read that as "the normalisation is 1/|D|^2, and it is fixed rather than
free".  That is right about the arithmetic and wrong about what it buys, because
eq:Pimunu's bare sum is DIMENSIONLESS:

    [W(s)] = L^2      W(s) = -|s|, comp 167's weight
    [D_m D_n] = L^2
    [B] = L^-4        a kernel on M normalised to unit integral
    -------------------------------------------------
    [Pi_bare] = L^0,  so Pi_bare is a pure count, ~ N^2

A stress tensor is an energy density, L^-4 in natural units.  The only scale the
discrete data carries is a_n, so restoring dimensions costs exactly one factor of
a_n^-4, which is A1's own node density lambda_n.  Part 4 measures the result:
after the forced per-pair normalisation and the restoration of dimensions,
Pi_mn diverges as ONE power of the node density, not two.

SO M7'S MISSING QUANTITY IS NAMED, AND THERE IS EXACTLY ONE OF IT.  It is the
physical spacing a_* at which A1's idealised limit is truncated.  That is the
same object a lattice spacing is: the continuum limit does the geometry, the
finite spacing sets the magnitude.  comp 167 established that neither d_0 nor
l_* is such a spacing, and that stands.  M7 therefore does NOT close.  What
changes is that the gap is one number of a familiar kind rather than a density
the theory was said not to supply.

WHAT SURVIVES UNTOUCHED, and it is worth checking rather than assuming.
sec:no-signalling derives its bipartition from "rho: D ->> M is a quotient map
and a spacetime point IS a fibre of it", which is the surjective reading.  Part 6
checks that the argument needs no surjectivity: D_A := rho^-1(U_A) and
D_B := D \\ D_A is a bipartition of D for ANY map rho whatsoever.  No-signalling
survives both readings, and so does comp 167's negative result on the vacuum
energy, since neither branch produces a computed scale to disagree with
measurement.
"""

import math

import numpy as np

ETA = np.diag([1.0, -1.0, -1.0, -1.0])
RNG = np.random.default_rng(20260930)

BOX = 4.0
VOL = BOX ** 4
COUNTS = (150, 300, 600, 1200, 2400)


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


def sample(N):
    return RNG.uniform(-BOX / 2, BOX / 2, size=(N, 4))


def pi_bare(pts, cut):
    """eq:Pimunu with W(s) = -|s|, bare, cut at |s| <= cut.  As comp 167 and 179."""
    P = np.zeros((4, 4))
    npairs = 0
    for i in range(len(pts)):
        Dv = pts[i] - pts[i + 1:]
        if len(Dv) == 0:
            continue
        s = np.einsum("pi,ij,pj->p", Dv, ETA, Dv)
        k = np.abs(s) <= cut
        Dv, s = Dv[k], s[k]
        if len(s) == 0:
            continue
        npairs += int(k.sum())
        Dl = Dv @ ETA
        P += np.einsum("p,pm,pn->mn", np.abs(s), Dl, Dl)
    return P, npairs


def pi_local(pts, cut, x, h):
    """The same sum with a LOCAL bond kernel B supported between the two points.

    comp 179 summed globally.  eq:Pimunu carries B(x; rho(a), rho(b)) 'supported
    between the two realisation points', so the exponent has to be checked with
    the locality in place: a global count could scale as N^2 for a reason that
    localisation destroys.  B here is the indicator that the segment [rho(a),
    rho(b)] passes within h of x, divided by the 4-volume of that tube, so
    int B d^4x = 1 up to the discretisation and [B] = L^-4.
    """
    P = np.zeros((4, 4))
    nb = 0
    tube = (math.pi ** 2 / 2.0) * h ** 4          # 4-ball volume, the tube's scale
    for i in range(len(pts)):
        A = pts[i]
        Bp = pts[i + 1:]
        if len(Bp) == 0:
            continue
        Dv = A - Bp
        s = np.einsum("pi,ij,pj->p", Dv, ETA, Dv)
        k = np.abs(s) <= cut
        Dv, s, Bp = Dv[k], s[k], Bp[k]
        if len(s) == 0:
            continue
        # Euclidean distance from x to the segment [A, Bp], parameter clamped.
        seg = A - Bp                                   # == Dv
        w = x - Bp
        den = np.einsum("pi,pi->p", seg, seg)
        den = np.where(den > 0, den, 1.0)
        t = np.clip(np.einsum("pi,pi->p", w, seg) / den, 0.0, 1.0)
        foot = Bp + t[:, None] * seg
        d = np.linalg.norm(x - foot, axis=1)
        m = d <= h
        if not m.any():
            continue
        nb += int(m.sum())
        Dl = Dv[m] @ ETA
        P += np.einsum("p,pm,pn->mn", np.abs(s[m]), Dl, Dl) / tube
    return P, nb


def slope(xs, ys):
    lx = np.log(np.asarray(xs, float))
    ly = np.log(np.asarray(ys, float))
    return float(np.polyfit(lx, ly, 1)[0])


# ---------------------------------------------------------------------------
def part1():
    rule()
    print("  1.  TWO REALISATION MAPS, NOT ONE, AND THEIR TYPES DO NOT AGREE")
    rule()
    print("      comp 179 part 1 said 'the body defines rho: D -> M once ... one")
    print("      substrate, one realisation map.'  The first clause of that is wrong.")
    print()
    print("      sec:phi-construction, Step 1:")
    print("        'any surjective function rho: D ->> X ... partitions D into equivalence")
    print("         classes ... A spacetime POINT is then defined to be a FIBRE of rho ...")
    print("         The manifold M is the quotient set D/~ ... The map rho is thus a")
    print("         QUOTIENT MAP, and M is a DERIVED set: it comes into existence as the")
    print("         image of rho, rather than being a container that rho maps D into.'")
    print("      The same section calls the container reading 'a foundational circularity'")
    print("      and spends four paragraphs disposing of it.")
    print()
    print("      sec:mosco-conditional:")
    print("        'the realisation map rho_n: D_n -> M = R x S^3 with image rho_n(D_n)")
    print("         asymptotically equidistributed with respect to the Riemannian volume")
    print("         of M'")
    print("      D_n is finite; R x S^3 is uncountable; so rho_n is NOT surjective and M")
    print("      is given in advance.  That is the container.")
    print()
    print("      And the book says so itself, in the Mosco-step assumption list:")
    print("        '(i) The realisation map rho: D -> M PRESUMES the target manifold M is")
    print("         smooth and finite-dimensional.'")
    print()
    print("      So the same name carries a surjection onto a derived target and a non-")
    print("      surjection into a given one.  Which of them eq:Pimunu uses is exactly")
    print("      comp 179's fork, and it is settled in part 2.")
    print()
    return True


def part2():
    rule()
    print("  2.  A FINITE SET HAS NO UNCOUNTABLE QUOTIENT, WHICH DECIDES THE FORK")
    rule()
    print("      The book's D is finite at every stage, and it commits to that in four")
    print("      independent places:")
    print("        A1                      |D_n| -> infinity, so each |D_n| is finite")
    print("        the Bernoulli measure   mu = (x)_{a in D} Bern(1/2) over a site list")
    print("        sec:born-agreement      exact enumeration of all 2^|D| configurations")
    print("        comp 178                the balance probability C(|D|,|D|/2) 2^-|D|")
    print()
    n = 12
    quotient_max = n                      # |D/~| <= |D|, attained iff all fibres singletons
    print(f"      Cardinal arithmetic, checked at n = {n}: every quotient of an n-element")
    print(f"      set has at most n elements, so |D_n/~| <= {quotient_max} < |R x S^3|.")
    ok_card = quotient_max <= n
    print()
    print("      Therefore M = D_n/~ is FINITE at every stage and is not a smooth")
    print("      4-manifold at any of them.  But sec:einstein writes")
    print()
    print("          nabla^mu Pi_mn = -1/4 nabla_n T,")
    print()
    print("      a covariant derivative on a smooth M, and eq:Pi-fluid decomposes Pi_mn")
    print("      against a metric.  Neither exists at a finite stage.")
    print()
    print("      SO READING (B) IS NOT AVAILABLE.  comp 179 recorded that comp 167 had")
    print("      taken it without saying so; the sharper statement is that it could not")
    print("      have been taken at all.  D in eq:Pimunu is A1's sequence, and the smooth")
    print("      M = R x S^3 is the limit of the finite quotients rather than the quotient")
    print("      of any one substrate.  comp 167's ARITHMETIC is untouched, as comp 179")
    print("      reproduced it exactly; what falls is its reading of the symbol.")
    print()
    print(f"      -> a finite set has no uncountable quotient, (B) excluded    : {ok_card}")
    print()
    return ok_card


def part3():
    rule()
    print("  3.  THE EXPONENT SURVIVES LOCALISATION OF THE BOND KERNEL")
    rule()
    print("      comp 179 measured Pi ~ N^2 with the pair sum taken GLOBALLY.  eq:Pimunu")
    print("      carries B(x; rho(a), rho(b)) 'supported between the two realisation")
    print("      points', so the exponent has to be re-measured with the locality in")
    print("      place: a global N^2 could have a reason that localisation destroys.")
    print()
    x0 = np.zeros(4)
    h = 0.45
    xs, glob, loc = [], [], []
    print(f"      {'N':>7}{'Pi_bare (global)':>20}{'Pi_bare (local)':>20}")
    for N in COUNTS:
        pts = sample(N)
        Pg, _ = pi_bare(pts, cut=4.0)
        Pl, _ = pi_local(pts, cut=4.0, x=x0, h=h)
        xs.append(N)
        glob.append(Pg[0, 0])
        loc.append(Pl[0, 0])
        print(f"      {N:>7}{Pg[0,0]:>20.5g}{Pl[0,0]:>20.5g}")
    sg, sl = slope(xs, glob), slope(xs, loc)
    print()
    print(f"      fitted exponent, global sum : {sg:+.3f}")
    print(f"      fitted exponent, local  sum : {sl:+.3f}")
    ok = abs(sg - 2.0) < 0.10 and abs(sl - 2.0) < 0.15
    print()
    print("      Both are 2.  Localisation costs a constant, not an exponent: the chance")
    print("      that a short pair's bond passes near a fixed x is O(1) in the box and")
    print("      independent of N, so the quadratic pair count carries straight through.")
    print()
    print(f"      -> Pi_bare ~ N^2 with the bond kernel in place              : {ok}")
    print()
    return ok


def part4():
    rule()
    print("  4.  THE FORCED NORMALISATION DOES NOT BUY A FINITE DENSITY")
    rule()
    print("      Under (A) the per-pair normalisation is forced and comp 179 measured it")
    print("      to converge.  That is right, and reading it as 'the normalisation is")
    print("      fixed, so the object is finite' is too optimistic.  eq:Pimunu's bare sum")
    print("      is DIMENSIONLESS:")
    print()
    print("        [W(s)] = L^2      W(s) = -|s|, comp 167's weight")
    print("        [Delta_m Delta_n] = L^2")
    print("        [B] = L^-4        a kernel on M normalised to unit integral")
    print("        -----------------------------------------------------------")
    print("        [Pi_bare] = L^0   a pure count, which is why it goes as N^2")
    print()
    print("      A stress tensor is an energy density, L^-4 in natural units.  The only")
    print("      scale the discrete data carries is a_n, so restoring dimensions costs")
    print("      exactly one factor a_n^-4, which is A1's own node density lambda_n.")
    print("      At fixed V_M and |D| a_n^4 = V_M, that is lambda_n = N / V_M.")
    print()
    print(f"      {'N':>7}{'Pi/N^2':>14}{'a_n':>12}{'lambda_n':>12}{'(Pi/N^2)*lambda_n':>20}")
    xs, perpair, dens = [], [], []
    for N in COUNTS:
        P, _ = pi_bare(sample(N), cut=4.0)
        pp = P[0, 0] / N ** 2
        a_n = (VOL / N) ** 0.25
        lam = 1.0 / a_n ** 4
        xs.append(N)
        perpair.append(pp)
        dens.append(pp * lam)
        print(f"      {N:>7}{pp:>14.5f}{a_n:>12.5f}{lam:>12.4g}{pp*lam:>20.5g}")
    conv = max(perpair) / min(perpair) < 1.15
    sdens = slope(xs, dens)
    print()
    print(f"      per-pair value converges (spread < 15%)   : {conv}")
    print(f"      dimensionally restored density, exponent  : {sdens:+.3f}")
    ok = conv and abs(sdens - 1.0) < 0.10
    print()
    print("      The per-pair column drifts up by about 5% across the table rather")
    print("      than sitting flat.  That is a finite-box effect of the fixed |s|")
    print("      cutoff against the box diagonal, and it is why the exponent reads")
    print("      1.011 and not 1.  It moves no conclusion and is quoted rather than")
    print("      rounded away.")
    print()
    print("      ONE power, not two.  So the honest statement is this.  Removing the pair")
    print("      counting is forced and it works; restoring the dimensions then puts back")
    print("      exactly one factor of the node density, and A1 sends that to infinity.")
    print("      comp 179 part 4 said the per-pair normalisation is 'fixed rather than")
    print("      free', which is true, and left the impression that a finite object")
    print("      results, which is not.  What results is a divergence of order lambda_n.")
    print()
    print(f"      -> the restored density diverges as lambda_n, one power     : {ok}")
    print()
    return ok


def part5():
    rule()
    print("  5.  SO THE MISSING QUANTITY IS NAMED, AND THERE IS EXACTLY ONE OF IT")
    rule()
    print("      Pi_mn ~ lambda_n = 1/a_n^4, and a_n -> 0 is A1's idealisation rather")
    print("      than a physical claim.  What M7 needs is therefore the PHYSICAL spacing")
    print("      a_* at which the limit is truncated, and nothing else: one number, with")
    print("      Pi_mn ~ 1/a_*^4.")
    print()
    print("      That is the same object a lattice spacing is.  The continuum limit does")
    print("      the geometry; the finite spacing sets the magnitude; no result that is a")
    print("      ratio, a shape or a count feels it.  PST is in the ordinary position of")
    print("      a lattice construction here, which is a better position than 'the theory")
    print("      does not supply the density' made it sound.")
    print()
    print("      comp 167 established that neither of the theory's two lengths is such a")
    print("      spacing: d_0 is a coherence length, which sec:grain-vs-coherence says is")
    print("      not the grain, and l_* enters as a momentum cutoff on field modes.  That")
    print("      stands, and it is why M7 does NOT close here.")
    print()
    print("      WHAT CHANGES, precisely: the gap goes from 'a density the theory does")
    print("      not supply' to 'one truncation scale of a familiar kind, not supplied'.")
    print("      Smaller, sharper, and still open.  Nobody should read this as a closure.")
    print()
    print("      AND THE VACUUM-ENERGY CONCLUSION IS UNAFFECTED.  comp 167's negative")
    print("      result needs only that no computed absolute scale is produced, and none")
    print("      is: a_* is not computed here, it is named.")
    print()
    return True


def part6():
    rule()
    print("  6.  NO-SIGNALLING NEEDS NO SURJECTIVITY, CHECKED RATHER THAN ASSUMED")
    rule()
    print("      sec:no-signalling gets its bipartition from 'rho: D ->> M is a quotient")
    print("      map and a spacetime point IS a fibre of it', which is the surjective")
    print("      reading.  Part 2 says eq:Pimunu cannot use that reading, so the question")
    print("      is whether the entanglement chain loses its bipartition with it.")
    print()
    print("      It does not, and the book's own construction is already robust: it sets")
    print("      D_A := rho^-1(U_A) and D_B := D \\ D_A.  A preimage and its complement")
    print("      partition the domain of ANY function, surjective or not.")
    print()
    rng = np.random.default_rng(7)
    ok = True
    for trial in range(200):
        n = int(rng.integers(3, 40))
        # an arbitrary, deliberately non-surjective map into a larger target
        img = rng.integers(0, 3 * n, size=n)
        UA = set(int(v) for v in rng.choice(3 * n, size=int(rng.integers(1, 3 * n)),
                                            replace=False))
        DA = {i for i in range(n) if int(img[i]) in UA}
        DB = set(range(n)) - DA
        ok &= (DA | DB == set(range(n))) and not (DA & DB)
    print(f"      200 random non-surjective maps: preimage and complement always")
    print(f"      bipartition D exactly                                       : {ok}")
    print()
    print("      So the chain survives.  What surjectivity buys is the stronger reading")
    print("      of a REGION as a union of fibres, rho^-1(U) = union of p in U; the")
    print("      bipartition itself needs none of it.  A reader should not be told the")
    print("      theory lacks the correspondence, and the correction in part 1 does not")
    print("      take it away.")
    print()
    return ok


def part7():
    rule()
    print("  7.  TAMPER TEST: THE EXPONENT TRACKS WHAT IT IS SUPPOSED TO TRACK")
    rule()
    print("      Part 4's claim is that the restored density carries ONE power of the")
    print("      node density because the bare sum is dimensionless and a stress tensor")
    print("      is L^-4.  If the arithmetic were insensitive to that, the same +1 would")
    print("      come out of a wrong dimensional assignment too.  Two controls:")
    print()
    xs, d0, d1, d2 = [], [], [], []
    for N in COUNTS:
        P, _ = pi_bare(sample(N), cut=4.0)
        pp = P[0, 0] / N ** 2
        lam = N / VOL
        xs.append(N)
        d0.append(pp)             # no restoration at all
        d1.append(pp * lam)       # the correct one power
        d2.append(pp * lam ** 2)  # a wrong two powers
    s0, s1, s2 = slope(xs, d0), slope(xs, d1), slope(xs, d2)
    print(f"      no dimensional restoration      exponent {s0:+.3f}   (expect  0)")
    print(f"      one power of lambda_n           exponent {s1:+.3f}   (expect +1)")
    print(f"      two powers of lambda_n          exponent {s2:+.3f}   (expect +2)")
    ok = abs(s0) < 0.10 and abs(s1 - 1) < 0.10 and abs(s2 - 2) < 0.10
    print()
    print("      The three separate cleanly, so the +1 is the dimensional assignment's")
    print("      and not an artefact of the fit.  The assignment itself is the premise")
    print("      to argue with, and it is stated in part 4 rather than buried.")
    print()
    print(f"      -> the exponent tracks the assumed dimensions                : {ok}")
    print()
    return ok


def main():
    print()
    print("COMPUTATION 182:  M7's FORK IS DECIDED, AND THE MISSING NUMBER IS NAMED")
    print()
    r1, r2, r3 = part1(), part2(), part3()
    r4, r5, r6, r7 = part4(), part5(), part6(), part7()
    rule()
    print("  SUMMARY")
    rule()
    print(f"  1. two realisation maps, incompatible types                : {r1}")
    print(f"  2. a finite set has no uncountable quotient, (B) excluded  : {r2}")
    print(f"  3. Pi_bare ~ N^2 survives the local bond kernel            : {r3}")
    print(f"  4. the restored density diverges as lambda_n, one power    : {r4}")
    print(f"  5. the missing quantity is one truncation scale a_*        : {r5}")
    print(f"  6. no-signalling needs no surjectivity                     : {r6}")
    print(f"  7. tamper test: the exponent tracks the dimensions         : {r7}")
    print()
    print("""  RESULT.  M7 does not close, and comp 179's fork does.

  (B) is not available.  A finite set has no uncountable quotient, D is finite at
  every stage by four independent commitments of the book, and sec:einstein needs
  a covariant derivative on a smooth M.  So D in eq:Pimunu is A1's sequence and
  M = R x S^3 is the limit of the finite quotients, not the quotient of one
  substrate.  comp 167's arithmetic is untouched; its reading of the symbol falls.

  The forced per-pair normalisation works and does not buy a finite density.  The
  bare sum is dimensionless, a stress tensor is L^-4, and the only scale in the
  discrete data is a_n, so restoring dimensions puts back exactly one power of the
  node density lambda_n = 1/a_n^4, measured at +1.011 in part 4 and +1.049 on
  part 7's independent draw, against controls at +0.049 and +2.049.  The excess
  over 1 is the same few-percent upward drift the per-pair value shows across the
  table, a finite-box effect of the fixed |s| cutoff against the box diagonal; it
  moves no conclusion, and it is quoted rather than rounded away.  comp 179 part
  4's "fixed rather than free" is right about the arithmetic and left too
  comfortable an impression; this corrects it.

  What is left is ONE number: the physical spacing a_* at which A1's limit is
  truncated, with Pi_mn ~ 1/a_*^4.  That is what a lattice spacing is, and it is a
  better description of PST's position here than "the theory does not supply the
  density".  comp 167's finding that neither d_0 nor l_* is such a spacing stands,
  which is why this is not a closure.

  Two things are checked rather than assumed, because the correction in part 1
  could have cost them.  sec:no-signalling's bipartition needs no surjectivity, as
  a preimage and its complement partition the domain of any function; and comp
  167's vacuum-energy conclusion needs only that no absolute scale is COMPUTED,
  and a_* is named rather than computed.

  The lesson repeats for the eighth time and it is now the reliable one: the error
  was in a sentence stating what a result rests on, and it was found by checking
  that sentence against the book rather than against the file asserting it.""")
    print()
    return all([r1, r2, r3, r4, r5, r6, r7])


if __name__ == "__main__":
    import sys
    # 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)
