diff --git a/research/one-triple-ten-step-obstruction/README.md b/research/one-triple-ten-step-obstruction/README.md new file mode 100644 index 0000000000..1f659aae55 --- /dev/null +++ b/research/one-triple-ten-step-obstruction/README.md @@ -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. diff --git a/research/one-triple-ten-step-obstruction/SOURCES.json b/research/one-triple-ten-step-obstruction/SOURCES.json new file mode 100644 index 0000000000..5856160a8e --- /dev/null +++ b/research/one-triple-ten-step-obstruction/SOURCES.json @@ -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" + } + ] +} diff --git a/research/one-triple-ten-step-obstruction/TASK.json b/research/one-triple-ten-step-obstruction/TASK.json new file mode 100644 index 0000000000..b5a011121a --- /dev/null +++ b/research/one-triple-ten-step-obstruction/TASK.json @@ -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." + } + ] +} diff --git a/research/one-triple-ten-step-obstruction/VERIFY.json b/research/one-triple-ten-step-obstruction/VERIFY.json new file mode 100644 index 0000000000..f31219eba5 --- /dev/null +++ b/research/one-triple-ten-step-obstruction/VERIFY.json @@ -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." + } + ] +} diff --git a/research/one-triple-ten-step-obstruction/oracle.py b/research/one-triple-ten-step-obstruction/oracle.py new file mode 100644 index 0000000000..ebe39c2b12 --- /dev/null +++ b/research/one-triple-ten-step-obstruction/oracle.py @@ -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 diff --git a/research/one-triple-ten-step-obstruction/verify.py b/research/one-triple-ten-step-obstruction/verify.py new file mode 100644 index 0000000000..09f0df4cf9 --- /dev/null +++ b/research/one-triple-ten-step-obstruction/verify.py @@ -0,0 +1,167 @@ +"""Exact finite obstruction for a single triple in ten source steps.""" +from collections import Counter +from hashlib import sha256 +from itertools import combinations +from math import factorial +from pathlib import Path +import json + +from oracle import canonical_census, difference_bits + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def next_word(word): + """Advance a nine-entry multiset permutation in lexicographic order.""" + pivot = -1 + for index in range(7, -1, -1): + if word[index] < word[index + 1]: + pivot = index + break + if pivot == -1: + return False + for other in range(8, pivot, -1): + if word[other] > word[pivot]: + word[pivot], word[other] = word[other], word[pivot] + word[pivot + 1:] = reversed(word[pivot + 1:]) + return True + raise ValueError("lexicographic successor is missing") + + +def prefixes(word): + values = [0] + for step in word: + values.append(values[-1] ^ step) + return values + + +def difference_set(word): + values = prefixes(word)[:-1] + return {left ^ right for left in values for right in values} + + +def validate(word): + require(len(word) == 10, "ten source steps required") + require(all(type(step) is int and 0 < step < 32 for step in word), + "nonzero five-bit steps required") + require(sum(step.bit_count() == 3 for step in word) == 1, + "exactly one triple required") + require(all(step.bit_count() in (1, 3) for step in word), + "remaining steps must be singletons") + counts = [sum((step >> axis) & 1 for step in word) for axis in range(5)] + require(sorted(counts) == [2, 2, 2, 2, 4], "incidence profile required") + require(prefixes(word)[-1] == 0, "restored connector required") + + +def census(triple): + counts = tuple((4 if axis == 0 else 2) - ((triple >> axis) & 1) + for axis in range(5)) + word = [1 << axis for axis, count in enumerate(counts) for _ in range(count)] + expected = factorial(9) + for count in counts: + expected //= factorial(count) + histogram = Counter() + best = None + # There are at most 9! multiset permutations. Exhaustion is checked below. + for _ in range(factorial(9)): + full = tuple(word) + (triple,) + validate(full) + size = len(difference_set(full)) + histogram[size] += 1 + if best is None or size > best[0]: + best = (size, full) + if not next_word(word): + break + require(sum(histogram.values()) == expected, "permutation census incomplete") + require(best is not None, "empty census") + return histogram, best + + +def rejected(word): + try: + validate(word) + except ValueError: + return True + return False + + +def controls(best): + word = best[1] + require(not rejected(word), "attaining word rejected") + mutations = (word[:-1], (0,) + word[1:], (True,) + word[1:], + (32,) + word[1:], word[:-1] + (3,), + word[:-1] + (11,), (7,) + word[1:]) + require(all(rejected(w) for w in mutations), "invalid word accepted") + masks = difference_set(word) + require(len(masks) == 30 and len(set(range(32)) - masks) == 2, + "sharp witness does not miss exactly two masks") + # Cyclic rotation changes prefixes by translation, preserving differences. + for cut in range(10): + rotated = word[cut:] + word[:cut] + validate(rotated) + require(difference_set(rotated) == masks, "rotation reduction failed") + # A planted full cover exercises the accepting branch, outside this alphabet. + gray = tuple(index ^ (index >> 1) for index in range(32)) + (0,) + gray_word = tuple(gray[i] ^ gray[i + 1] for i in range(32)) + require(difference_set(gray_word) == set(range(32)), "full cover rejected") + require(difference_bits(gray_word) == (1 << 32) - 1, "oracle full cover failed") + require(difference_set((1, 1, 1, 1)) == {0, 1}, "repeated-prefix test failed") + require(difference_bits((1, 1, 1, 1)) == 3, "oracle repeated-prefix test failed") + return len(mutations) + + +def source_hashes(): + package = Path(__file__).resolve().parent + paths = sorted(package.iterdir()) + require(len(paths) <= 16, "unexpected package contents") + return {path.name: sha256(path.read_bytes()).hexdigest() + for path in paths if path.is_file()} + + +def main(): + histograms = {} + best = None + for axes in combinations(range(5), 3): + triple = sum(1 << axis for axis in axes) + histogram, attaining = census(triple) + key = "contains_repeated" if triple & 1 else "avoids_repeated" + if key in histograms: + require(histograms[key] == histogram, "coordinate-symmetry mismatch") + histograms[key] = histogram + if best is None or attaining[0] > best[0]: + best = attaining + require(sum(histograms["contains_repeated"].values()) == 15120, + "wrong first domain size") + require(sum(histograms["avoids_repeated"].values()) == 7560, + "wrong second domain size") + require(histograms["contains_repeated"] == canonical_census(7), + "independent containing-triple census disagrees") + require(histograms["avoids_repeated"] == canonical_census(14), + "independent avoiding-triple census disagrees") + require(max(histograms["contains_repeated"]) == 30, "wrong sharp maximum") + require(max(histograms["avoids_repeated"]) == 26, "wrong second maximum") + require(best is not None, "no attaining word") + rejected_count = controls(best) + # Positive even incidences summing to 12 have one four and four twos. + prices = (1, 4, 10, 16, 28) + base_bill = 2 * sum(prices) + require(base_bill + 2 * min(prices) == 120, "old incidence tariff changed") + require(base_bill + 4 * min(prices) == 122, "new incidence floor changed") + receipt = {"status": "PASS_ONE_TRIPLE_TEN_STEP_OBSTRUCTION", + "primary_words": 6 * 15120 + 4 * 7560, + "independent_words": 15120 + 7560, + "covering_words": 0, "sharp_maximum_masks": best[0], + "attaining_word": best[1], + "attaining_prefixes": prefixes(best[1]), + "missing_masks": sorted(set(range(32)) - difference_set(best[1])), + "canonical_histograms": histograms, + "rejected_word_controls": rejected_count, + "package_sha256": source_hashes()} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()