Skip to content

Exclude one-triple ten-step connectors and prove a strict 122-leaf floor #5876

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 27, 2026
+549 −0
Merged

Exclude one-triple ten-step connectors and prove a strict 122-leaf floor #5876

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
194 changes: 194 additions & 0 deletions research/one-triple-ten-step-obstruction/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,194 @@
# A single triple cannot complete a ten-step five-source connector

This contribution was produced by Nick Petalas. Apache-2.0.
Independent human and formal proof-kernel review are unclaimed.

**Claim type: exact finite certificate with a written model reduction.**
A restored ten-step walk on five binary sources, with exactly one triple-source
step and nine singleton steps, cannot have every mask as a difference of two
prefixes. Among walks using every source, the sharp maximum is **30 of 32
masks**. This answers Open next question 1 of unpaidmoon's
[PR #4137](https://github.com/CrocSwap/integer-mult-bounds/pull/4137).

Consequently, every covering ten-step walk containing any source step of arity
at least three has source-leaf bill **at least 122** at prices
`(1,4,10,16,28)`. Aaron Wang's pair-source word already attains bill 120.
The new lower bound is strict; attainment of 122 is unclaimed.
There is no new kappa, supplier admission or complete multiplication theorem.

## Model and scope

Use Ross Richardson's paired-readout model: five immutable sources, one
arbitrarily dirty connector, 31 distinct nonzero output masks, two readouts per
output, and connector restoration. Each source step adds a nonempty subset of
sources. Each step is one query, and each included source pays its own leaf
price. Triple and higher-arity calls are charged operations.

For a source word `w=(s_1,...,s_10)`, let `q_0=0` and
`q_i=q_(i-1) XOR s_i`. Restoration means `q_10=0`. The available masks are
`D(w)={q_i XOR q_j: 0<=i,j<10}`. The credited prefix criterion says that the
paired readouts implement all requested masks exactly when `D(w)=F_2^5`.
The dirty connector cancels between each pair. This criterion and its arbitrary
linear-operator interpretation are inherited, not new results.

The certificate decides the finite source-word question. It does not execute a
native array program or certify physical frames, routing, source preparation,
scratch, tape, precision, recursive charges or a complete consumer invoice.
Specialized operators, additional connectors and more than two readouts per
output are outside this contract.

## Complete reduction and finite exclusion

Every coordinate in a covering walk must occur: otherwise all differences lie
in a coordinate hyperplane. Restoration makes every incidence positive and
even. One triple and nine singletons have total incidence 12, so the five
incidences must be `(4,2,2,2,2)` up to source permutation.

Rename the four-use source as coordinate zero. Rotate the unique triple to the
last step. A rotation translates every prefix by the same vector, preserving
all differences; it does not require a free physical operation. Thus all
candidates are exhausted by fixing the final triple and permuting the nine
singleton steps with the remaining incidences.

There are two types of triple:

| Triple includes the four-use source | Triple choices | Singleton multiplicities | Words per triple | Sharp mask maximum |
| --- | ---: | --- | ---: | ---: |
| Yes | 6 | `(3,1,1,2,2)` up to the other labels | `9!/(3!2!2!)=15120` | 30 |
| No | 4 | `(4,1,1,1,2)` up to the other labels | `9!/(4!2!)=7560` | 26 |

The primary census visits all `6*15120+4*7560=120960` words and finds zero
covers. No word is pruned. A lexicographic successor visits each multiset
permutation exactly once: it increases the rightmost increasable entry and
puts the suffix in its least ordering. The factorial count checks exhaustion.

A separate implementation places each label in disjoint subsets of the nine
positions. It checks all 15,120 and 7,560 words for the canonical triples
`{0,1,2}` and `{1,2,3}`. Its mask oracle uses intersections with XOR-translated
bitsets, rather than enumerating prefix pairs. The complete coverage histograms
agree. The primary census also checks agreement within each of the two source
permutation classes. Both algorithms are retained in this package.

The maximum 30 is attained by step masks

```text
1, 8, 1, 2, 1, 16, 4, 8, 16, 7
```

with prefixes

```text
0, 1, 9, 8, 10, 11, 27, 31, 23, 7, 0.
```

The verifier computes its two missing masks and every histogram afresh.
Thus 30 is a sharp finite maximum, and complete 32-mask coverage is impossible.
Walks with an unused source have at most 16 masks, so they do not enlarge it.

## The strict source-leaf gap

For any covering restored ten-step walk, write its positive even coordinate
incidences as `c_i`. The base incidences two on every coordinate cost
`2*(1+4+10+16+28)=118`. If total incidence is at least 14, its four additional
incidences cost at least four, giving bill at least 122, even after relabeling.

A bill at most 120 therefore forces total incidence at most 12. A step of
arity at least three rules out total incidence ten. At total incidence twelve,
there are exactly two excess incidences beyond ten singleton steps. Such a
word with a step of arity at least three must have exactly one triple and nine
singletons. The finite exclusion above rules it out. This proves the 122
lower bound without asserting that any word attains it.

This uses no replay of #4137's nine-point set exclusion, length floor or old
bill comparison. Those results and Aaron Wang's positive pair construction are
cited predecessors. The new computation is the previously open ten-step
one-triple case, not an audit of those predecessors.

## Reproduction and evidence

From the repository root, with CPython 3.12 and its standard library:

```sh
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/one-triple-ten-step-obstruction/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/one-triple-ten-step-obstruction/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/one-triple-ten-step-obstruction
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/one-triple-ten-step-obstruction --check-source-history
```

Replace the absolute interpreter path with another CPython 3.12 installation
elsewhere. Both registered commands have 120-second limits and retain every
check under optimization. The verifier emits
`PASS_ONE_TRIPLE_TEN_STEP_OBSTRUCTION` inside a generated JSON receipt with
package SHA256 hashes. It writes no files. Redirect logs and receipts outside
the checkout. Historical source pins are provenance; no predecessor executable
or mutable external input is used by this certificate.

Seven invalid-word controls reject wrong length, zero, Boolean and out-of-range
steps, absence of the triple, changed incidence, and multiple triples.
All ten rotations of an attaining word preserve its complete difference set.
A planted full Gray-cycle cover exercises successful 32-mask recognition in
both implementations; a repeated-prefix fixture exercises duplicate handling.
These controls test the new census, not the predecessor results.

The prescribed card command was run once as orientation and passed
`PASS_UNIVERSAL_CONNECTOR_BOUNDARY pairings=945 max_coverage=31 queries=74 leaves=182`.
The current selected-baseline metadata control also passed. Neither supplies
new evidence for this certificate. The selected full cold replay, Lean, Docker,
production native execution and independent scientific acceptance are unrun.

## Implementation bounds

The Power of Ten scope is the two new Python files. They use structured control
flow without recursion, network access, subprocesses or dynamic evaluation.
Every word has nine singleton positions and one triple; the primary loop has an
explicit `9!` cap with exact exhaustion checks. The independent placement loops
range over subsets of nine fixed positions. Bitset indices range over 32 masks
and five coordinates. Functions fit within 60 physical lines. Invalid words
raise exceptions, and the registered warning-strict checks remain active with
optimization. No external static analyzer or repository-wide diagnostic change
is claimed.

Rule 3 deviation: CPython and its standard library allocate managed objects.
The primary census streams words and retains at most 32 histogram counters,
one best ten-step word, eleven prefixes and a 32-element difference set per
iteration. The independent census streams nine-position placements and retains
32-bit prefix/difference bitsets and at most 32 counters. The package hash scan
is capped at 16 entries. These fixed domains bound live data; fixed allocation
is not claimed. Verification exercises both enumeration paths and their exact
bounds. A fixed-capacity implementation is a follow-up only if these domains
or the runtime contract change.

## Sources and credit

Credit **unpaidmoon #4137** for the explicit open question, charged triple
extension and earlier lower bounds; **Aaron Wang** for the pair-source word
and its 72-query interface; **Ross Richardson #943** for the universal dirty
connector model and prefix-difference criterion; and **Adam Gall** for the
fixed-alphabet all-tariff work credited by the predecessors. Their source
notices and results are unchanged. The source paths and exact blobs are
historical provenance in [SOURCES.json](SOURCES.json). No broader literature
priority is claimed for permutation enumeration or the prefix argument.

Canonical base is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
[TASK.json](TASK.json) refines the connector-alphabet card to its explicit
one-triple attainment question. Live open PRs, recent account PR bodies,
handoffs, local reservations, merged-title searches and all-main distinctive
README terms were checked before reserving the question. The overlap helper's
local coverage was sparse and its remote cache was historical; live queries
supplemented it. No search proves novelty against unpublished work.

Advance claim: [handoff #1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214969).

## Open next questions

1. What is the exact minimum source-leaf bill for a covering ten-step walk
containing a step of arity at least three? The strict 122 lower bound does
not establish attainment. Start with incidence total 14 and price the full
source profile before a search. No witness or exclusion there is supplied.
2. Is there a short structural proof of the sharp 30-mask ceiling? It could
replace the census. Start with the five even and five odd prefix positions,
distinguishing whether the triple contains the four-use coordinate. A
structural argument for the sharp maximum remains missing.

The same questions, relevance and blockers are recorded in TASK.json. No
follow-on search is part of this contribution.
36 changes: 36 additions & 0 deletions research/one-triple-ten-step-obstruction/SOURCES.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
{
"schema_version": 1,
"base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
"files": [
{
"path": "certificates/selected-result.json",
"usage": "provenance",
"git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
"sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
},
{
"path": "docs/research/agent-task-catalog.json",
"usage": "provenance",
"git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
"sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
},
{
"path": "research/connector-triple-query-floor/README.md",
"usage": "provenance",
"git_blob": "c290f6381de73f1b1868404544698ac08f72c9cd",
"sha256": "9c81c56e361bbf9e2f392dd61958493a79b194b9ec70913c548b1da501c05c81"
},
{
"path": "research/connector-pair-source-path-seed2cdb/README.md",
"usage": "provenance",
"git_blob": "22aade420aef3f395792cac576a41a98d8c986f5",
"sha256": "ec2be09ba0ef27862ce880ae7bf2e0b6be3dd32fccaed70e0b6fd4e96d19e8d3"
},
{
"path": "research/universal-connector-boundary/README.md",
"usage": "provenance",
"git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f",
"sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476"
}
]
}
68 changes: 68 additions & 0 deletions research/one-triple-ten-step-obstruction/TASK.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
{
"schema_version": 1,
"task_id": "connector-alphabet-change",
"priority_revision": 8,
"base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
"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": "refined",
"actual_scope": "Exclude a covering ten-step five-source walk with one triple and nine singletons; deduce a 122 source-leaf lower bound for ten-step covering walks containing any step of arity at least three.",
"scope_change_reason": "Take the explicit attainment question in unpaidmoon PR4137 rather than introduce an unpriced new operation. This is an exact finite obstruction in its already charged triple alphabet.",
"bottleneck_link": "The result separates pair and higher-arity source calls at the minimum ten-step boundary: higher arity cannot tie the 120 source-leaf fixture bill. It does not admit a supplier or improve kappa.",
"budget_minutes": 60,
"stop_rule": "Stop at the first exact exclusion, corroborate by an independent position-placement census, and package without searching a larger incidence class.",
"outcome": "negative-result",
"evidence": "120960 lexicographic words and 22680 independently placed representatives exclude complete coverage. The sharp mask maxima are 30 and 26 according to whether the triple contains the four-use source.",
"author": "Nick Petalas",
"ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
"open_questions": [
{
"question": "What is the exact minimum source-leaf bill for a covering ten-step walk containing a step of arity at least three?",
"why_it_matters": "The new 122 lower bound is a strict gap over pair-only bill 120, but attainment of 122 is not established.",
"first_step": "Study restored incidence total 14 and price the complete source profile before searching words.",
"blocked_by": "No witness or complete exclusion for incidence total 14 is provided."
},
{
"question": "Is there a short structural proof of the sharp 30-mask ceiling for the one-triple ten-step class?",
"why_it_matters": "It would replace the finite census with a transparent combinatorial obstruction.",
"first_step": "Use the five even and five odd prefix positions and distinguish whether the triple contains the four-use coordinate.",
"blocked_by": "The present proof of the sharp ceiling uses complete finite enumeration."
}
]
}
32 changes: 32 additions & 0 deletions research/one-triple-ten-step-obstruction/VERIFY.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
{
"schema_version": 1,
"status": "ready",
"python": "3.12",
"requirements": [],
"inputs": [],
"commands": [
{
"argv": [
"{python}",
"-W",
"error",
"-B",
"{package}/verify.py"
],
"timeout_seconds": 120,
"checks": "Complete lexicographic and independent position-placement censuses, sharp witnesses, rotation, positive coverage and invalid-word controls."
},
{
"argv": [
"{python}",
"-W",
"error",
"-O",
"-B",
"{package}/verify.py"
],
"timeout_seconds": 120,
"checks": "Repeat all finite proof obligations with optimization enabled; checks use explicit exceptions."
}
]
}
52 changes: 52 additions & 0 deletions research/one-triple-ten-step-obstruction/oracle.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
"""Independent position-placement census and bitset difference test."""
from collections import Counter
from itertools import combinations


def position_words(counts):
"""Place four labels in disjoint subsets; the fifth fills the remainder."""
positions = tuple(range(9))
for a in combinations(positions, counts[0]):
left_a = tuple(p for p in positions if p not in a)
for b in combinations(left_a, counts[1]):
left_b = tuple(p for p in left_a if p not in b)
for c in combinations(left_b, counts[2]):
left_c = tuple(p for p in left_b if p not in c)
for d in combinations(left_c, counts[3]):
word = [16] * 9
for label, slots in enumerate((a, b, c, d)):
for slot in slots:
word[slot] = 1 << label
yield tuple(word)


def difference_bits(word):
"""For each difference, intersect the prefix set with its XOR translate."""
prefix_set = 1
parity = [0] * 5
for step in word[:-1]:
for axis in range(5):
parity[axis] ^= (step >> axis) & 1
prefix_set |= 1 << sum(bit << axis for axis, bit in enumerate(parity))
result = 0
for difference in range(32):
translated = prefix_set
for axis in range(5):
if (difference >> axis) & 1:
width = 1 << axis
low = sum(((1 << width) - 1) << start
for start in range(0, 32, 2 * width))
translated = ((translated & low) << width) | (
(translated & (low << width)) >> width)
if translated & prefix_set:
result |= 1 << difference
return result


def canonical_census(triple):
counts = tuple((4 if axis == 0 else 2) - ((triple >> axis) & 1)
for axis in range(5))
histogram = Counter()
for singles in position_words(counts):
histogram[difference_bits(singles + (triple,)).bit_count()] += 1
return histogram
Loading
Loading