Prove confined two-clique P104 relays need eight paid units (no κ)

research/p104-two-clique-relay-floor/PROOF.md

@@ -0,0 +1,174 @@
+# A paid floor for confined two-clique relay networks
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract
+
+Let G=A disjoint-union B be a finite set of binary port labels in a binary
+space with a symmetric bilinear form, with both classes nonempty. Assume
+
+    <p_i,p_j> = 1 if i,j belong to the same class, and 0 otherwise.
+
+In particular every label has self-pairing one. Let W be the span of G.
+All source coordinates are independent over Q. No source is initialized to
+zero. Write e_i for the unit source row and X(g)=span_Q{e_i:p_i in g}.
+
+A finite ordered REL network consists of moves mu=1,...,M with binary frames
+
+    L_mu strictly contained in g_mu contained in W,
+    v_mu = l_mu + sum_(nu<mu) a_mu,nu v_nu,
+    l_mu in X(g_mu),
+    a_mu,nu != 0 only if L_nu is contained in g_mu.
+
+Coefficients are arbitrary rationals. These are the source-availability and
+chronological arrival constraints of PR6170's REL relaxation, confined to W.
+The sum permits any number of earlier parents, branching, merging, resets,
+cancellation and public re-ascents. Public transport and other scalar work
+are granted free for this lower bound. The paid bill is
+
+    P = sum_mu (dim g_mu - dim L_mu).
+
+A receiving column u_mu may be arbitrary except
+
+    u_mu(j) != 0 only if L_mu is contained in Q_j = p_j^perp.
+
+Set C=sum_mu u_mu v_mu^T and Gamma_ji=<p_j,p_i>, interpreted as the rational
+number zero or one. Correctness of the pattern requires C_ji=delta_ji
+whenever Gamma_ji=1. Thus H=C Hadamard-product Gamma=I_|G|. No condition
+is imposed on the two off-diagonal class blocks of C.
+
+## Theorem
+
+Every such network satisfies
+
+    rank_Q(H)
+      <= sum_mu [dim pi(g_mu) - dim pi(L_mu)]
+      <= P,                                                   (1)
+
+where pi:W -> F2^2 sends every A port to (1,0) and every B port to (0,1).
+Consequently every correct network has P>=|G|. Equality is attainable in
+REL. For two four-port cliques the exact minimum is eight.
+
+The first inequality is a statement about the complete network, including
+all relayed source content. It is not a rank bound on each term separately.
+
+## The rational subspace representation
+
+Choose representative ports a in A and b in B. Define
+
+    pi(x) = (<a,x>,<b,x>).
+
+The Gram assumption gives the asserted values on G. Since G spans W, this
+also proves that every p_j in a fixed class has the same pairing functional
+on W. For j in A it is the first coordinate of pi, and for j in B the second.
+
+Represent the five binary subspaces of F2^2 by rational subspaces of Q^2:
+
+| Binary subspace S | T(S) over Q |
+| --- | --- |
+| zero | zero |
+| span(1,0) | span_Q(1,0) |
+| span(0,1) | span_Q(0,1) |
+| span(1,1) | span_Q(1,1) |
+| F2^2 | Q^2 |
+
+This representation preserves all inclusions and dimensions. Write
+T_g=T(pi(g)) and t_j=(1,0) or (0,1) according to the class of j.
+Three properties follow.
+
+1. If p_i is in g, then t_i is in T_g.
+2. If L is contained in Q_j, then the rational functional t_j^T annihilates
+   T_L. For a coordinate functional, binary and rational annihilation have
+   exactly the same zero cases in the table.
+3. For L contained in g, T_L is contained in T_g and
+
+       dim T_g - dim T_L = dim pi(g) - dim pi(L)
+                         <= dim g - dim L.                    (2)
+
+The last inequality is the rank bound on the induced map g/L -> pi(g)/pi(L).
+In particular radical-only frame drops contribute zero to the first bill
+in (1), although they can cost positive P.
+
+## Cumulative information invariant
+
+For a rational source row v define the 2-by-|G| packet B(v) whose ith column
+is t_i v(i). Its two rows are the A and B restrictions of v. For a local
+source row l in X(g), every column of B(l) lies in T_g by property 1.
+
+We inductively construct a subspace D_mu of rational source rows. It obeys
+
+    z^T B(v_nu) is in D_mu for every nu<=mu
+      and every rational functional z annihilating T_Lnu,     (3)
+
+and has dimension at most the first mu summands of (1). Initially D_0=0.
+
+For move mu, take any z annihilating T_gmu. The local contribution vanishes.
+Every permitted earlier parent nu has T_Lnu contained in T_gmu. Therefore
+z also annihilates T_Lnu, and (3) for the earlier parent gives
+
+    z^T B(v_mu) = sum_(nu<mu) a_mu,nu z^T B(v_nu) in D_(mu-1). (4)
+
+Extend a basis of ann(T_gmu) to a basis of ann(T_Lmu). There are exactly
+dim T_gmu - dim T_Lmu new functionals. Adjoin their rows z^T B(v_mu) to
+D_(mu-1) to form D_mu. Equation (4) proves (3) for all functionals in the
+larger annihilator. Old invariants are retained because D only grows.
+Its dimension rises by at most that many new functionals. This proves the
+dimension bound without counting relayed content a second time.
+
+At the final boundary, the jth row of H is
+
+    H_j,* = sum_mu u_mu(j) t_j^T B(v_mu).
+
+Every nonzero coefficient has L_mu contained in Q_j. Property 2 and (3)
+place each summand in D_M. All rows of H therefore lie in D_M. This proves
+the first inequality of (1); (2) proves the second. If H is the identity,
+its row rank is |G|, proving the floor for every finite network.
+
+## Attainment and the shared-cost issue
+
+A simple attaining REL network uses one move per port, with
+g_i=span_F2(p_i), L_i=0, v_i=e_i and u_i=e_i. Every move has gap one and
+all availability constraints hold. It realizes C=I and P=|G|. This is an
+abstract REL realization, not a physical P104 word.
+
+For equal classes of size four, match their indices and use four moves
+
+    g_i=span(p_Ai,p_Bi), L_i=0,
+    v_i=u_i=e_Ai+e_Bi.
+
+Each gap is two. The endpoint C=[[I_4,I_4],[I_4,I_4]] has rank four,
+while H=I_8 and P=8. Low completion rank alone does not save paid cost.
+
+An explicitly relayed attaining network splits each move through the
+intermediate line span(p_Ai+p_Bi). The first move introduces v_i, and the
+second carries it unchanged to zero. Both gaps are one. Only the second
+move contributes to the endpoint. Its individual Hadamard term has rank
+two although its own gap is one. Summing independent per-move rank bounds
+would fail here; the cumulative invariant charges both moves once.
+
+## Application and limits
+
+The actual P104 fixture uses
+
+    A=(73,239,336,502), B=(81,247,328,494),
+    W=span_F2(81,502,239,73).
+
+The verifier checks membership in the pinned port definition, the complete
+eight-by-eight Gram table and all subspaces of this four-dimensional W.
+It constructs both attaining networks above. It does not recount PR6170's
+four-space census or replay any predecessor word, invoice or claimed floor.
+
+This closes the confined-chain part of PR6170 P104-LEMMAS.md section 11.5
+and permits more general confined relay graphs as well. It does not settle
+that source's outside-reaching case. On frames outside W, two ports in one
+class need not have the same pairing functional. Property 2 can then fail.
+The result also does not assert a rational inclusion representation of a
+higher-dimensional binary quotient lattice. The rank-two representation
+above is an essential hypothesis, not a model of the whole E8 interface.
+
+The rank and dimension arguments are classical linear algebra. The new
+contribution is their cumulative application to this REL question, allowing
+the cost sharing that the source explicitly leaves open. Independent human
+and formal proof-kernel review are unclaimed. No native realization,
+complete physical invoice, supplier admission or multiplication theorem
+follows. The selected frontier remains unchanged.

research/p104-two-clique-relay-floor/README.md

@@ -0,0 +1,149 @@
+# Two-clique relays still cost eight
+
+This is a scoped proof with exact finite corroboration. In the confined REL
+model, a block of two mutually orthogonal four-port cliques needs exactly
+eight units of owned paid frame descent. Arbitrary finite chains, branching,
+merging, cancellation and public re-ascents do not lower this bill. Both a
+four-move construction and an eight-move relayed construction attain eight.
+No new kappa or selected-frontier change is claimed.
+
+DreamingOfClouds's [PR6170](https://github.com/CrocSwap/integer-mult-bounds/pull/6170),
+`P104-LEMMAS.md` section 11.5, proves the isolated-move floor and explicitly
+leaves chains and moves outside the group unresolved. This closes the
+confined-chain case and also permits general confined acyclic relay graphs.
+The outside-reaching case remains open. No predecessor census, frontier
+word, invoice or theorem is re-verified as this contribution.
+
+## Result and its boundary
+
+Let Gamma be the binary Gram mask of the ports, interpreted over Q. For
+every finite REL network whose gathering and landing frames lie in the
+block span, the new cumulative information bound is
+
+```text
+rank_Q(C Hadamard-product Gamma)
+  <= sum_moves [dim pi(gather) - dim pi(landing)]
+  <= sum_moves [dim gather - dim landing] = owned paid.
+```
+
+Here C is the complete rational source/receiver map and pi is the binary
+two-dimensional quotient identifying the two cliques. Correctness requires
+the Hadamard product to be I_8. The bound therefore gives owned paid >= 8.
+[PROOF.md](PROOF.md) proves the statement for any finite two-clique port set.
+
+The proof uses an inclusion-preserving rational representation of the five
+binary quotient subspaces and maintains a cumulative row space. This is
+needed because one term in a legal chain can have Hadamard rank two while
+its own paid descent is only one. Counting that term independently would
+miss its predecessor's cost. The checker includes this exact counterexample.
+
+The attaining endpoint has rank four, C=[[I_4,I_4],[I_4,I_4]], but still costs
+eight. Thus the low completion rank in the proposed block construction
+cannot itself produce a cheaper confined owned layer.
+
+## Exact finite evidence
+
+The new concrete P104 block is
+
+```text
+A = 73, 239, 336, 502
+B = 81, 247, 328, 494
+W = span_F2(81, 502, 239, 73).
+```
+
+The pinned predecessor word is read only for its port definition. The replay
+checks membership of these eight ports, their complete Gram table and:
+
+- All 67 subspaces of W and all 513 nested frame pairs, including equality.
+  There are 128 local-source and 128 receiving-functional checks.
+- Two attaining networks, including every source-coordinate column of their
+  complete rank-four endpoint and identity Hadamard shadow.
+- 512 deterministic sixteen-move networks, containing 18,885 nonzero parent
+  edges, 4,429 branching parents and 4,407 moves with multiple parents.
+  Literal coordinate evaluation agrees with the packet calculation.
+- All 512 binary three-by-three rational matrices against a separate minor
+  rank oracle, five rejected invalid networks, and the shared-cost control.
+
+The relay fixtures are not an exhaustive network census. The all-finite-network
+claim is the written proof. The finite runs test its representation and
+invariant, with explicit exceptions that remain active under optimization.
+The replay prints a generated receipt bound to every package file's SHA256.
+No receipt is handwritten and the verifier writes no files.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p104-two-clique-relay-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/p104-two-clique-relay-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-two-clique-relay-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-two-clique-relay-floor --check-source-history
+```
+
+Another CPython 3.12 path can replace the local interpreter. The scientific
+marker is `PASS_P104_TWO_CLIQUE_RELAY_FLOOR`. The runner also checks exact
+source pins and metadata. The publication preflight checks committed bytes
+and source-history availability. These are different checks.
+
+## Limits and implementation bounds
+
+All gathering and landing frames must remain inside W. Two same-class ports
+can have different pairing functionals outside W, breaking the rational
+representation's reader condition. The proof grants free public re-ascents
+and arbitrary rational scalar coefficients, so it excludes a larger class
+than confined dyadic REL networks. It supplies no physical scalar word,
+native implementation, full productive/paid invoice or supplier admission.
+The five selected framework assumptions remain. No selected cold replay,
+Lean, Docker or historical scientific suite is required or claimed.
+Independent human and formal proof-kernel review are unclaimed.
+
+The finite reference implementation fixes eight ports, at most sixteen moves,
+binary dimension at most nine, and rational matrices at most 64 by 16. The
+registered fixtures use coefficients in {-1,0,1}. Matrix input parts are
+capped at 2,048 bits. There is no recursion, dynamic code evaluation, network
+access or subprocess creation. Functions stay below 60 physical lines.
+The checks run with warnings treated as errors, normally and under `-O`.
+
+Power-of-Ten rule 3 has a managed-runtime deviation. Python allocates Fraction
+and container objects during these finite replays. Fixed frame, port, move
+and coefficient domains bound live state, and no network history is retained
+across cases. The source is one pinned finite compressed JSON file, opened
+with a context manager. The replay exercises the maximum move count and
+invalid frame/arrival/receiver contracts. A fixed-capacity arithmetic backend
+would be needed if this became a production checker with external inputs.
+
+## Open next questions
+
+Can an outside-reaching network reduce the eight-unit cost? First specify
+one gathering/landing network and the exact source and receiving maps, then
+test the rational-lift reader condition. The blocker is that classwise
+pairing functionals agree only on W. Any physical successor must also pay
+public helper lifetimes, restoration, native access and all other charges.
+The structured question is in [TASK.json](TASK.json).
+
+## Provenance and credit
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+DreamingOfClouds PR6170 supplies the open two-clique question and REL
+contract, including its local-source, landing and paid definitions. Its
+isolated-move result is a cited predecessor, not an audit deliverable. Ali
+Romman's PR5599 supplies the retained port definition. Matarener's P104
+geometry and the retained P104/native/helper/controller/caller lineage keep
+their credit. Linear rank bookkeeping and the rational rank-two subspace
+representation use classical linear algebra.
+
+The base is canonical main `a5bff3bf133e482541c09eba4e773884bdb2b1b7`.
+[SOURCES.json](SOURCES.json) binds the exact source blobs and SHA256 values.
+The selected record and catalogue are historical provenance; only the port
+definition is a live external input. Task scope is explicitly changed from
+the card's selected-word experiment to this targeted obstruction.
+
+The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279674)
+follows checks of live handoffs, active Discussions, open/merged PRs, recent
+account contributions and local target reservations. The cached open snapshot
+covered 338 PRs and 5,957 Discussion records with complete pagination. The
+sparse local scan searched 84 notes and omitted 8,539; distinctive Git searches
+against main and separate merged-PR searches supplemented it. These searches
+do not cover unpublished work or prove global novelty.

research/p104-two-clique-relay-floor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-designer-toolkit-v2/P104-LEMMAS.md",
+      "usage": "provenance",
+      "git_blob": "129f28dd10c9e1c43d29a9dd280e022070288a73",
+      "sha256": "54263ecdcabb067b1f77749ae60cb1f430c02fd720b63e5e39f358f6bfee78ec"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb",
+      "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099"
+    }
+  ]
+}