Skip to content

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

Open
petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w15-1102g-scoped-obstruction
Open

petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w15-1102g-scoped-obstruction

Conversation

@petalas

@petalas petalas commented Nov 3, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Scoped written algorithmic proof with an exact finite certificate. Cost-aware read-set dominance reduces the complete six-transfer search from 463 expanded states to 89, while preserving every legal minimum-read continuation. No new kappa.

at the same source cut and physical frame
  S contains T and cost(S) <= cost(T)
  discard the label for T

This answers the pruning lemma in ywz65's PR2538. Its graph semantics are cited premises; its executable and four published fixture optima are not replayed or audited. The new instance has source order (0,0,1,1,2,2), colors (1,2,3), and all seven nonzero targets. The connector-alphabet card is explicitly changed to this search-method side result.

This contribution was produced by Nick Petalas. Credit ywz65 / PR2538, conorholds / PR2208, Ross Richardson / PR934 and PR943, and the retained connector lineage. Shortest paths and dominance pruning are classical.

Evidence

  • Before: 463 complete bounded-graph states. After: 89 retained/expanded states, 102 discovered records. Every original state has a same-cut/frame dominator of no greater cost. Separate pairwise postprocessing of the entire unpruned graph exactly matches the incremental frontier.
  • Minimum read bill 15; minimum root-transfer bill six. The five-transfer graph rejects. A formal-polynomial interpreter checks the emitted 27-operation word and its inverse for arbitrary dirty inputs and opaque noncommuting maps.
  • Ten semantic/resource controls pass. Warning-strict normal and optimized checks produce identical source-bound receipts. The two registered commands were timed locally at 0.037 s and 0.061 s. These are completion times, not a speedup claim.
  • Registered replay, metadata/pins, committed bytes/modes/source history and official export/input coverage pass at efd1f40a5ff783373f3104a1200f3c0f0a9e6ccc. Both read-only Git-free export modes pass with empty PATH, preserving all nine exported files and modes.

CPython 3.12.15, macOS 27.0.1 arm64, standard library only. Exact reproduction from the repository root:

/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 --check-modes
/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

Any CPython 3.12 executable can replace the local path. Expected markers are PASS_REGISTERED_RESEARCH_PACKAGE, PASS_RESEARCH_COMMIT_BYTES and PASS_CONNECTOR_READ_SET_DOMINANCE.

Limitations

The written simulation covers this fixed minimum-read interface; the finite certificate covers one three-source instance. Implementation limits are six sources, 24 transfers and 250,000 discovered labels, with explicit rejection on exhaustion. No n9/n12 optimum, weighted read/transfer envelope, runtime speedup, physical caller, complete child tariff or supplier admission is supplied. Native/hosting/precision/tape obligations remain separate. Selected cold replay, Lean and Docker were not run. The selected frontier and all five framework assumptions retain their status. Independent human and formal proof-kernel review are unclaimed.

Open next questions

  • Can indexed superset queries support the predecessor's n9/n12 walks under a separately justified larger resource contract?
  • Can an actual recursive caller host the two-root interface at a favorable complete tariff, with admission, preparation, routing, restoration, precision and tape return paid?

Related open work

No open PR for this exact read-availability graph or its state-count quantity was located in the live targeted searches. PR2538 is the merged source; merged PR2561 studies the separate read/transfer tradeoff, which this fixed minimum-read objective leaves unchanged.

  • PR6564 studies rounded signed dyadic connector calls and dirty-root carry restoration. This contribution preserves the exact binary joint-root interface and computes no rounded carry or error quantity.
  • PR6568 improves unsigned one-connector capacity using balanced closed walks in finite characteristic. This contribution prunes a fixed two-root read-availability graph; it computes no competing capacity or characteristic threshold.

The completion refresh inspected all 112 account open PRs, including 15 created since the advance CLAIM and this PR. The other fourteen supply no competing state count or optimum for the displayed fixed source/color instance. The two adjacent connector contributions are distinguished above. No extra computations checked another contribution's numbers.

Main/merged searches, live claims and local reservations were checked before publication. The overlap cache covered 506 open PRs and 6,503 Discussion records, but local sparse-note coverage was incomplete; unpublished work and arbitrary historical diffs remain unknown.

CI notes

Both hosted checks, plan and replay (research/connector-read-set-dominance), passed at exact head efd1f40a5ff783373f3104a1200f3c0f0a9e6ccc in Registered research packages run 41609930842. The completed checks were read once with gh pr checks 6566 --repo CrocSwap/integer-mult-bounds: plan passed in 4m31s and registered replay passed in 1m30s. Run metadata confirms completed success and the matching head.

Hosted success covers execution of the registered normal/optimized finite certificate and its package checks. It does not establish independent mathematical acceptance, a physical supplier, or a complete multiplication theorem. All registered local commands, committed-byte/source-history checks and read-only export checks also passed. No check was deferred solely to CI, and no CI failure remains.

Merge Danger

Door: two-way. Blast radius: isolated research package. Seven new opt-in files; no shared implementation, frozen predecessor evidence or selected-result edit.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant