Skip to content

Refute the B2 quotient-direction edge bound (no κ) - #6424

Open
petalas wants to merge 2 commits into
CrocSwap:mainfrom
petalas:research/w8-1102c-pending
Open

petalas wants to merge 2 commits into
CrocSwap:mainfrom
petalas:research/w8-1102c-pending

Conversation

@petalas

@petalas petalas commented Nov 2, 2026 •

Copy link
Copy Markdown
Contributor

Summary

A new six-line rational witness refutes the quotient-direction repair proposed as the first step in Aaron Wang / navinor's PR2340 Open next question 1. Both factor families have six distinct projective directions, so the quotient collapses nothing.

B = diag(J3,J3)                         minimum cost 6
W = two bidirected triangles + 3 edges  acyclic edge count 9
q-direction quotient = W               proposed bound fails by 3

Claim type: finite counterexample with an exact scoped proof and exhaustive finite corroboration. The proof also establishes the minimum cost directly: rank one with unit binary diagonal would force an inadmissible all-ones matrix. PR2340's broader request for the strongest rank-aware replacement remains open. No new kappa, supplier admission, selected-frontier change or complete multiplication theorem is claimed.

The witness, proof and verifier are produced by Nick Petalas. Credit Aaron Wang / navinor for PR2340's repair question and PR2293's edge/vertex distinction, DreamingOfClouds for PR2162's rank-three model and valid vertex theorem with the retained PR2111/PR1590 lineage, and ROTl24 for PR2334's separate repeated-direction and selected-edge counterexamples. Those packages are cited context; no predecessor scientific suite was replayed.

Evidence

Before, collapsing proportional q directions was an explicitly proposed repair. After, this all-distinct witness has exact minimum cost 6 and quotient acyclic-edge count 9. All 36 rational dot products, actual supports and primitive projective directions are checked. Full enumeration covers all 32,768 admissible pairings, with elimination and explicit row-space ranks agreeing on each. All 720 vertex orders agree with a 64-subset graph dynamic program. Ten controls cover seven malformed witnesses, one edge-deletion sensitivity check and two rank fixtures.

Locally passed on macOS arm64, CPython 3.12.15, standard library only:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/quotient-direction-edge-counterexample/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/quotient-direction-edge-counterexample/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/quotient-direction-edge-counterexample
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/quotient-direction-edge-counterexample --check-source-history --check-modes

Both registered commands were individually timed locally below one second, with 120-second manifest limits. The registered runner, exact committed bytes/modes/source ancestry, official package export and declared-input coverage pass. The mathematical verifier passed normally and optimized from a read-only Git-free export with empty PATH; all six exported files including its manifest retained their hashes. Optional receipts are generated from execution and bind the result to package hashes; none is hand-written or committed. The current selected-source metadata orientation also passed. Use any CPython 3.12 path in place of the absolute interpreter elsewhere.

Scientific base and refreshed canonical main are 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision eight. TASK.json explicitly records the changed side-result scope of the complex-rank-shape-decoder card. The advance CLAIM retains the original question and scope.

Limitations

This is one explicit six-line configuration. No globally smallest counterexample or general optimal replacement bound is claimed. The valid vertex bound and the separate cost(B)>=v target are unaffected. Three extra wild edges are unselected by the attaining B, so this witness does not refute the combined restriction of distinct factor families and counting only B-selected wild edges.

Physical/native realization, arbitrary-dirty restoration, full paid/target invoices, compiler, stock, hosting, precision/tape and outer admission remain unproved. Selected scientific cold replay, Lean, independent human and formal proof-kernel review were not run or claimed.

Open next questions

Does the selected-edge bound hold when both factor families are projectively distinct? First derive a rank-sensitive constraint under both restrictions. PR2334 already refutes an unrestricted selected-edge bound when directions repeat. No proof or counterexample for the combined restrictions is supplied here. This contribution stops at its first verified quotient-repair counterexample.

Related open work

The completion refresh inspected this account's 14 open PRs created since the advance CLAIM, including their bodies. None computes this six-line quotient-direction acyclic-edge quantity. Adjacent decoder work has separate objects and numerical claims:

Merged sources PR2340, PR2293, PR2334 and PR2162 retain the roles stated above. No additional computations were run to check other PRs' numerical claims. Arbitrary diffs and unpublished work remain outside the inspected coverage.

CI notes

Both hosted checks, plan and replay (research/quotient-direction-edge-counterexample), passed at exact head 090953af3c999a33ff4ed1f9e7dbf53c2dba3f56 in run 41536571519. The completed checks were read once with gh pr checks 6424 --repo CrocSwap/integer-mult-bounds; run metadata confirms the matching head and successful conclusion. Hosted replay covers both registered normal and optimized commands. Local registered replay and committed-byte/source-history/mode checks also passed. This is executable certificate coverage, not independent human or formal proof-kernel acceptance.

Merge Danger

Door: two-way. Blast radius: isolated. Five new files under research/quotient-direction-edge-counterexample only; no shared implementation, frozen predecessor or selected record changes.

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