Prune 374 states from exact joint connector synthesis (no κ)

research/connector-read-set-dominance/PROOF.md

@@ -0,0 +1,126 @@
+# Continuation-safe read-set dominance
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+The state model and its dirty-root semantics are those of ywz65's
+[PR2538](https://github.com/CrocSwap/integer-mult-bounds/pull/2538), building
+on conorholds's PR2208 and Ross Richardson's connector interface. Their
+completeness argument is a cited premise. The new step is the dominance
+simulation below and its bounded implementation. Shortest paths and
+superset dominance are classical; no general literature priority is claimed.
+
+## Interface and state
+
+The field is F2. Sources x_j are immutable, the two roots start with arbitrary
+dirty rows d_0,d_1, and each target y_m also starts arbitrarily dirty. The
+opaque linear maps B_j and A_m need not commute and may be singular. All B
+and A calls use physical root 0. A root shear C_p adds root 1-p to root p.
+The desired endpoint adds A_m(sum_{j in m} B_j x_j) to each target and restores
+both roots. Targets are never read and have no intermediate deadlines. Each
+complete child call must restore its own scratch and heads.
+
+Fix a source word with each label occurring twice and a nonzero color
+v_j in F2^2 for each source. At cut t let Q_t be the two normalized source
+coefficient rows. A frame G in GL2(F2) represents physical roots
+G(d + Q_t X), where X_j = B_j x_j. Its first row a exposes the read vector
+(a,a Q_t) in F2^(n+2). A source event j is legal precisely when G v_j = e_0.
+
+A graph state is (t,G,S), with S the set of all exposed read vectors on the
+path so far. A B edge advances t at fixed common source price, represented
+as zero in the transfer objective. Either C edge costs one and changes G.
+Both edge types add the newly current read vector to S. Edges depend on
+t,G and the fixed instance, never on S. The initial state is the identity
+frame at cut zero, with its current vector included in S.
+
+Let V be the complete set of possible read vectors at all cuts and frames.
+For each target m let d_m be the shortest XOR decomposition length of (0,m)
+over V. The predecessor establishes simultaneous attainability of these
+individual minima. Thus a terminal state is accepted when t is the final
+cut, G=I, and every target has a length-d_m decomposition over S. This is
+the fixed minimum-read objective; it does not optimize read/transfer tradeoffs.
+
+## Dominance theorem
+
+Suppose two reached states have the same t,G and respective labels (S,c)
+and (T,b), where c and b are transfer costs. If S contains T and c <= b,
+the first label can replace the second for every continuation.
+
+Proof. Take any continuation from (t,G,T). Starting from (t,G,S), repeat
+exactly the same B and C operations. Every operation is legal because
+legality depends only on t,G. The future cuts and frames therefore agree.
+After every step the first availability set still contains the second,
+since both sets are united with the same newly exposed vector. The first
+total transfer cost remains no larger. If the second state eventually
+accepts, its target decompositions remain available in the first. Their
+lengths cannot be smaller than d_m, since both availability sets are subsets
+of V. Consequently the first state also accepts with the minimum read bill.
+This proves the assertion for every finite continuation, without a length
+bound. The converse is unnecessary. QED.
+
+The proof uses historical availability rather than simultaneous stored
+copies. Once the path is chosen, reads can be emitted at the first visit to
+their vectors. Targets are independent and unread, so these insertions do
+not affect any B or C operation. No extra physical storage or free child
+call is inferred from this search representation.
+
+## Incremental pruning and a finite certificate
+
+At each fixed cut/frame, retain labels that are undominated in the joint
+order of greater availability and lower cost. Reject a dominated offer.
+When a new label dominates retained labels, retire those labels from the
+expansion queue. Parent records remain available for witness reconstruction.
+Equal sets and equal costs retain one copy. Superset inclusion alone is
+insufficient when the superset costs more.
+
+For a finite transfer budget K, explore every unretired queue entry with
+cost at most K. Every label in the unpruned graph has a reached dominating
+label in the pruned graph. Induct on an unpruned path: start at the shared
+initial state, simulate its next edge from a dominating label, then replace
+the offered label by any retained dominator. Dominance is transitive, and
+costs never increase under replacement. Finite retirement chains therefore
+preserve a retained representative. This proves acceptance equivalence up
+to K, and hence exact minimum transfer cost whenever an accepting bound is
+found. The algorithm reports resource exhaustion as an error, not an optimum.
+
+The certificate checks more than agreement of the two minima. It enumerates
+the complete unpruned graph through six transfers, computes its undominated
+frontier afterward with a separate pairwise subset test, and compares every
+retained label against the incremental result. It also finds a retained
+dominator for every unpruned state, with matching cut/frame and no greater
+cost. All these are explicit finite checks.
+
+The fixture is source word (0,0,1,1,2,2), colors (1,2,3), and all seven
+nonzero target masks. Its global minimum read bill is 15. Both complete
+searches find minimum transfer cost six; the pruned five-transfer graph has
+no accepting state. The emitted 27-operation program contains six B calls,
+15 A calls and six C calls. A separate free-algebra interpreter proves its
+arbitrary-input endpoint and literal inverse without identifying A_m B_j
+with B_j A_m. This certificate concerns this one fixed source/color instance.
+
+## Termination and implementation limits
+
+The implementation accepts one through six sources and transfer limits
+0 through 24. There are at most 39 distinct read vectors and 256 XOR-space
+vertices. For every source instance the graph is finite. The implementation
+additionally caps discovered labels at 250,000. An individual state's best
+integer cost decreases at most K+1 times, so at most cap*(K+1) queue entries
+are created. The explicit queue-pop bound includes one extra iteration to
+observe an empty queue. Witness reconstruction uses at most one iteration
+per stored parent plus one. Resource limits fail closed.
+
+The code has no recursion, dynamic imports or generated code. Python's
+managed allocation is a deviation from fixed preallocated memory. Live
+collections are bounded by the source, transfer and state caps; this is
+not a measured peak-byte guarantee. The certificate uses a quadratic
+postprocessing oracle only on its fixed small graph. It imposes no runtime
+performance threshold and claims no timing speedup.
+
+## Scope
+
+This answers the same-cut/frame dominance part of PR2538's open next
+question. It supplies neither a practical n9/n12 solver nor those instances'
+optima. No predecessor executable or published fixture is replayed. No
+weighted read/transfer envelope, recursive caller, native price, hosting,
+precision, tape, supplier admission, new kappa or selected-frontier change
+follows. The five selected framework assumptions keep their prior status.
+Independent human and formal proof-kernel review are unclaimed.

research/connector-read-set-dominance/README.md

@@ -0,0 +1,122 @@
+# Prune 374 states from a joint dirty-connector search
+
+A cost-aware superset rule reduces the complete six-transfer search from
+463 expanded states to 89 on one new fixed instance, while preserving
+every possible minimum-read continuation. Claim type: scoped written
+algorithmic proof with an exact finite certificate. No new kappa.
+
+At the same source cut and physical frame, label (S,c) dominates (T,b)
+when S contains T and c <= b. S and T are historical sets of available
+read vectors; c and b are paid root-transfer costs. Reject dominated
+offers and retire dominated queue entries. [PROOF.md](PROOF.md) proves
+the simulation and acceptance equivalence, including arbitrary dirty roots
+and noncommuting opaque child maps.
+
+This answers the dominance-pruning part of ywz65's
+[PR2538](https://github.com/CrocSwap/integer-mult-bounds/pull/2538)
+Open next questions. Its graph semantics and completeness are cited premises.
+Its four published fixture optima and executable are not replayed or audited.
+The new fixture has source order (0,0,1,1,2,2), colors (1,2,3), and all seven
+nonzero target masks. The alphabet is unchanged, so [TASK.json](TASK.json)
+records a changed scope from the connector-alphabet card to a search method.
+
+## Exact result and evidence
+
+The minimum read counts are two for masks 1 through 6 and three for mask 7.
+At this total of 15 reads, the exact minimum is six root transfers. The
+certificate enumerates every state through this accepting budget. It
+independently postprocesses the unpruned graph to obtain its full undominated
+frontier and compares every label with the incremental result.
+
+| Transfer cost | Complete graph expansions | Pruned graph expansions |
+| --- | ---: | ---: |
+| 0 | 3 | 3 |
+| 1 | 9 | 7 |
+| 2 | 23 | 12 |
+| 3 | 44 | 16 |
+| 4 | 84 | 20 |
+| 5 | 145 | 18 |
+| 6 | 155 | 13 |
+| Total | 463 | 89 |
+
+The pruned run discovers 102 labels, retires 13 and rejects ten dominated
+offers. Each of the complete graph's 463 states has a retained dominator
+with the same cut/frame and no greater cost. The complete graph digest is
+`18712a812ab2c5613dbb9486f1a5d0383883865d127ce59c2562429e883589e5`;
+the retained frontier digest is
+`7f457ff549506542344ea4297f089b3e7ed91fcfed45518869801ac9cc56963d`.
+Both are regenerated from the entire sorted state/cost lists.
+
+The five-transfer graph rejects the minimum-read target. The emitted
+27-operation witness has six B calls, 15 A calls and six root shears.
+A separate formal-polynomial interpreter checks its endpoint and inverse
+for arbitrary dirty inputs without commuting any A and B operators.
+
+Ten controls check subset direction, incomparable sets, the cost condition,
+retirement, an omitted read, state-cap exhaustion, transfer-limit rejection
+and two invalid instances. Checks use explicit exceptions under both normal
+and optimized Python. The generated stdout receipt hashes every package file
+and binds the complete graph, retained frontier and emitted word. No receipt
+is handwritten or stored in the checkout.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/connector-read-set-dominance
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/connector-read-set-dominance --check-source-history
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/connector-read-set-dominance/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/connector-read-set-dominance/verify.py
+```
+
+Another CPython 3.12 executable can replace the local interpreter path.
+The direct commands emit `PASS_CONNECTOR_READ_SET_DOMINANCE` inside a JSON
+receipt. The registered runner executes both modes. No timing speedup is
+claimed; state counts are the measured improvement.
+
+Local checks used CPython 3.12.15, macOS 27.0.1 arm64 and no dependencies
+beyond the standard library. The registered normal and optimized commands
+were also timed directly at 0.037 s and 0.061 s, with empty stderr and identical
+receipts. These are completion durations, not performance comparisons.
+
+## Limits
+
+The proof covers this fixed minimum-read interface. The implementation accepts
+one through six sources, transfer budgets through 24 and a discovered-label
+cap of 250,000. Exceeding a resource limit fails explicitly. Verification
+certifies the displayed three-source fixture, not every accepted instance.
+Python managed allocation is bounded by these finite input/resource caps,
+rather than fixed preallocation. [PROOF.md](PROOF.md) states loop bounds.
+
+No n9/n12 solver result, weighted read/transfer envelope, runtime speedup,
+physical child tariff, recursive caller, native admission, hosting,
+precision/tape proof, selected cold replay, Lean or Docker run is supplied.
+No new supplier or complete multiplication theorem is claimed. The selected
+frontier and all five framework assumptions retain their status. Independent
+human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+1. Can an indexed superset query make this exact pruning practical for the
+   predecessor's n9/n12 walks? Start with one pinned word and measure the
+   nondominated frontier. The present implementation's six-source and
+   resource caps are blockers; this package claims no scaling result.
+2. Can a concrete caller use the two-root interface at a favorable complete
+   tariff? First bind its child ports and pay admission, preparation, routing,
+   restoration, precision and tape return. Search-state reduction alone
+   supplies none of those costs.
+
+Structured questions and scope are in [TASK.json](TASK.json).
+
+## Credit
+
+This contribution was produced by Nick Petalas. Credit ywz65 / PR2538 for
+the read-availability graph, the open pruning question and its retained
+joint synthesis lineage; conorholds / PR2208 for fixed-color dirty-root
+framing; Ross Richardson / PR934 and PR943 for the connector interface.
+ywz65 / PR2561 studies the separate read/transfer tradeoff. Dominance and
+shortest-path methods are classical. [SOURCES.json](SOURCES.json) pins the
+predecessor statement and the originating catalogue and selected record.
+Only the predecessor README is a live source input; no predecessor code is
+imported. Apache-2.0.

research/connector-read-set-dominance/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/joint-connector-read-synthesis/README.md",
+      "usage": "input",
+      "git_blob": "23853715881a818ca7a33ac54d6809d202814e4d",
+      "sha256": "4ec9fb65d7cb6c5701d36715a9a34739fe3a2e0b4502a8b254622969c0e7526a"
+    }
+  ]
+}

research/connector-read-set-dominance/TASK.json

@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove continuation-safe cost-aware read-set dominance for PR2538 and certify a reduction from 463 to 89 complete bounded-search expansions on one new three-source instance.",
+  "scope_change_reason": "The operation alphabet stays fixed. This answers the explicit search-method question in PR2538 rather than constructing a newly priced connector operation.",
+  "bottleneck_link": "Exact joint synthesis can remove avoidable root transfers from a candidate interface. This result reduces its search states; a favorable physical supplier bill remains a separate obligation.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified state reduction, package its proof and certificate, and leave larger instances for later work.",
+  "outcome": "completed",
+  "evidence": "Complete six-transfer graph: 463 states; cost-aware dominance: 89 retained/expanded states and 102 discovered records. Every original state has a retained dominator. Independent postprocessing gives the same frontier. Minimum reads 15, minimum transfers 6; formal endpoint/inverse and ten controls pass.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can indexed superset queries make exact dominance practical for the predecessor n9/n12 walks?",
+      "why_it_matters": "It could extend exact joint synthesis to the intended larger fixed source words.",
+      "first_step": "Pin one larger source word and measure its nondominated frontier under a separately justified larger resource contract.",
+      "blocked_by": "The present implementation accepts at most six sources and 250000 discovered labels; no scaling result is supplied."
+    },
+    {
+      "question": "Can an actual recursive caller host the two-root interface with a favorable complete tariff?",
+      "why_it_matters": "Fewer search states do not themselves improve a supplier invoice.",
+      "first_step": "Bind actual child ports and charge admission, preparation, routing, restoration, precision and tape return.",
+      "blocked_by": "No physical caller or complete tariff is supplied."
+    }
+  ]
+}

research/connector-read-set-dominance/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/joint-connector-read-synthesis/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Complete bounded graph and incremental-frontier equality, all-state dominance coverage, exact endpoint/inverse, minimum-read optimum and ten controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same exact certificate and rejecting controls with Python assertions disabled."
+    }
+  ]
+}