diff --git a/research/six-source-c7-witness-other-weights/README.md b/research/six-source-c7-witness-other-weights/README.md new file mode 100644 index 0000000000..413a6c9612 --- /dev/null +++ b/research/six-source-c7-witness-other-weights/README.md @@ -0,0 +1,136 @@ +# Non-weight-3 masks missed by the recorded c=7 witness + +**Exhaustive finite census of one word. No new κ.** On the length-42 floor +word recorded in PR #7016, + +```text +023514103524310254054123145203452034213150 +``` + +the pairs `0 ≤ s ≤ t ≤ 41` realize 41 of the 43 nonzero binary masks of +weight other than 3. The two missing masks are `(3, 5)` and `(0, 1, 3, 5)`. +The same census misses the weight-3 mask `(1, 3, 5)`, which is the gap that +PR #7016 already records for this word. This word is therefore not a +depth-two block. + +The selected conditional κ remains `781451/250000000` in +`certificates/selected-result.json`. + +## Interface + +A floor word on six sources in characteristic 7 has length 42 and calls each +source seven times. `q_t` counts the first `t` letters, so `q_0 = 0` and +`q_42 = (7, 7, 7, 7, 7, 7)`. This is the unsigned dirty-connector interface +of PR #4231 / PR #4248, as used by PR #6141 and by the c=7 diagonal note: +the word meets a nonzero binary mask when `q_s + q_t` is congruent to that +mask modulo 7 for some `0 ≤ s ≤ t ≤ 41`. Boundary 42 is omitted because +`q_42 = 7·1 ≡ q_0`. + +Each coordinate of `q_s + q_t` lies in `{0, ..., 14}`. The residues 0 and 1 +in that range are exactly `{0, 1, 7, 8, 14}`, and the mask bit is 1 on +`{1, 8}`. The weight is the number of mask bits. The coordinate sum of +`q_t` is `t`, so a realizing pair satisfies `s + t ≡ weight (mod 7)`. + +## Census + +There are `42·43/2 = 903` pairs. The checker visits each pair once, compares +the allowed-set reading with the modulo-7 reading, and classifies all 63 +nonzero masks. + +| weight | masks | realized | missing on this word | +|---:|---:|---:|---| +| 1 | 6 | 6 | none | +| 2 | 15 | 14 | `(3, 5)` | +| 3 | 20 | 19 | `(1, 3, 5)`, the recorded #7016 gap | +| 4 | 15 | 14 | `(0, 1, 3, 5)` | +| 5 | 6 | 6 | none | +| 6 | 1 | 1 | none | + +The non-weight-3 misses are exactly `(3, 5)` and `(0, 1, 3, 5)`. Realizing +pairs of the nonzero masks number 16, 19, 19, 19, 15 and 8 at weights 1 +through 6. Eight further pairs realize the zero vector. The zero vector is +not a depth-two obligation. + +The first six letters are `023514`, one copy of each source. A reviewer can +check three pairs by hand: `(0, 1)` realizes `(0)`, `(0, 3)` realizes +`(0, 2, 3)`, and `(0, 6)` realizes every source. The checker requires those +three sums. + +Of the 16 masks that contain both sources 3 and 5, the census realizes 13. +The three unrealized masks are the whole missing list above. In particular +`(0, 3, 5)` and `(1, 2, 3, 5)` are realized, so the census does not say that +every mask containing `{3, 5}` is missed. + +Including `t = 42` adds no nonzero mask beyond this list. + +## What the census establishes + +Under the interface above, this one word misses exactly two nonzero masks +of weight other than 3, namely `(3, 5)` and `(0, 1, 3, 5)`. A depth-two +block needs every nonzero mask. This word does not provide one. + +The evidence is an exhaustive finite census. The domain, the 903 pairs with +`0 ≤ s ≤ t ≤ 41`, is finite. The enumeration is the double loop over that +triangle, and the program checks that the loop visits 903 pairs. The +modulo-7 reading and the allowed-set reading agree on every pair. Every +realizing pair satisfies the weight identity. The separate `t = 42` pass +finds no extra nonzero mask. + +This does not prove that every six-source floor word at characteristic 7 +misses these masks, and it does not prove that no depth-two block exists. +It does not re-prove the one-pair weight-3 cover bound of PR #7016. The +weight-3 line of the table is a control that this is the recorded witness. +No supplier, consumer, or selected frontier changes. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -W error -B research/six-source-c7-witness-other-weights/verify.py +python3.12 -I -O -W error -B research/six-source-c7-witness-other-weights/verify.py +python3.12 -B scripts/research_package.py --package research/six-source-c7-witness-other-weights --check-only +``` + +The marker is + +```text +PASS_SIX_SOURCE_C7_WITNESS_OTHER_WEIGHTS pairs=903 nonzero_hit=60/63 other_hit=41/43 missing_other=(3,5);(0,1,3,5) weight3_missing=(1,3,5) zero_pairs=8 boundary42_new=0 superset_realized=13/16 controls=7 +``` + +The seven controls are the floor-word shape of the recorded literal, the +agreement of the two mask readings, the weight identity on every nonzero +hit, the three hand-checked prefix pairs together with the recorded +weight-3 gap `(1, 3, 5)`, the empty boundary-42 increment, the thirteen +realized masks among the sixteen that contain `{3, 5}`, and the two +negative words: the adjacent transposition of positions 1 and 2 is still a +floor word and has a different non-weight-3 missing set, while changing the +first letter from 0 to 1 is rejected. Failures raise `SystemExit`. +Optimized mode cannot silence them. No SAT solver, Lean, or Docker replay +is used. + +## Open next questions + +1. Can one explicit six-source length-42 floor word, other than this + witness, realize both `(3, 5)` and `(0, 1, 3, 5)`? *Why:* a depth-two + block needs both masks. This census shows that the recorded witness + misses both. One other word that realizes both would separate that miss + from the floor-word hypotheses. An exhaustive census of every floor word + would be a different claim. *First step:* evaluate the same 903-pair + predicate on one other concrete length-42 floor word and record, for + these two masks only, whether each is realized. *Blocked by:* only the + recorded witness is enumerated here, and no second characteristic-7 + floor word is certified in this package. The two-pair weight-3 exchange + remains open question 1 of PR #7016. + +## Credit + +The depth-two interface and the weight identity are Nick Petalas's +(PR #4231, PR #4248, PR #6107), with the Ross Richardson PR #934 / PR #943 +lineage. JosieElliston's PR #6141 leaves characteristic 7 open. The diagonal +equality case is upstream PR #6941. The witness word, its weight-3 gap +`(1, 3, 5)`, and the request to evaluate the other weights are open +question 2 of upstream PR #7016 (fork PR 179). This package evaluates that +word and does not repeat the one-pair cover argument. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/six-source-c7-witness-other-weights/SOURCES.json b/research/six-source-c7-witness-other-weights/SOURCES.json new file mode 100644 index 0000000000..1fac568194 --- /dev/null +++ b/research/six-source-c7-witness-other-weights/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "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/connector-six-source-small-char/verify.py", + "usage": "provenance", + "git_blob": "3f50c05759e37bd226a0af35b151fa99b0a12113", + "sha256": "569194e1577692f6049dedc13aeecdeb321152b3a77a143990a8c8fcba53f87f" + }, + { + "path": "research/six-source-c7-diagonal-obstruction/README.md", + "usage": "provenance", + "git_blob": "7761f90e2e4205747a8e2592c6e1ad71435245b3", + "sha256": "23f9cff3b843519a41c20e6ab9fc19c0294425c1f80f275a476da8f57cf12e99" + } + ] +} diff --git a/research/six-source-c7-witness-other-weights/TASK.json b/research/six-source-c7-witness-other-weights/TASK.json new file mode 100644 index 0000000000..bf5ba9bde6 --- /dev/null +++ b/research/six-source-c7-witness-other-weights/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "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": "On the single length-42 floor word recorded in PR #7016, classify every pair 0 <= s <= t <= 41 and list the nonzero binary masks of weight other than 3 that q_s + q_t does not realize. The weight-3 gap of that same word is a control, not a new exchange bound.", + "scope_change_reason": "The catalogue card asks for one new connector operation. This package keeps the unsigned dirty connector alphabet fixed and answers open question 2 of PR #7016: which non-weight-3 masks the recorded witness misses. A new operation is not the missing step.", + "bottleneck_link": "Side result on the recursive-interface schedule. A depth-two block needs every nonzero mask, so the weight-3 count on this word cannot by itself be a block. No supplier, consumer, or selected kappa changes.", + "budget_minutes": 60, + "stop_rule": "Stop once all 903 pairs on this word are classified and the non-weight-3 missing set is listed. Stop without a substitute if the word's weight-3 missing set is not exactly (1, 3, 5).", + "outcome": "completed", + "evidence": "Exhaustive finite census of the 903 pairs 0 <= s <= t <= 41 on the recorded word. The allowed-set reading and the mod-7 reading agree on every pair. The word realizes 41 of 43 nonzero masks of weight other than 3. The missing masks are (3, 5) and (0, 1, 3, 5). The same census misses the recorded weight-3 mask (1, 3, 5). Eight pairs realize the zero vector. Boundary 42 adds no nonzero mask. Seven controls cover the floor word, the two readings, the weight identity, three hand-checked prefixes, the {3, 5} superset corollary, one adjacent transposition, and one rejected call-count edit. This is not an unrestricted nonexistence claim.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance: the census, the checker, and the package text.", + "open_questions": [ + { + "question": "Can one explicit six-source length-42 floor word, other than the recorded #7016 witness, realize both non-weight-3 masks (3, 5) and (0, 1, 3, 5)?", + "why_it_matters": "A depth-two block needs both masks. This census shows the recorded witness misses both. One other word that realizes both would separate that miss from the floor-word hypotheses. An exhaustive census of every floor word would be a different claim.", + "first_step": "Evaluate the same 903-pair predicate on one other concrete length-42 floor word and record, for these two masks only, whether each is realized.", + "blocked_by": "Only the recorded witness is enumerated here, and no second characteristic-7 floor word is certified in this package. The two-pair weight-3 exchange remains open question 1 of PR #7016." + } + ] +} diff --git a/research/six-source-c7-witness-other-weights/VERIFY.json b/research/six-source-c7-witness-other-weights/VERIFY.json new file mode 100644 index 0000000000..4708b47a1f --- /dev/null +++ b/research/six-source-c7-witness-other-weights/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exhaustive census of all 903 pairs on the recorded length-42 word. Allowed-set and mod-7 readings agree. Non-weight-3 misses are exactly (3,5) and (0,1,3,5). Weight-3 miss (1,3,5) is the recorded control. Zero vector has 8 pairs. Boundary 42 adds no nonzero mask. Seven controls: floor word, two readings, weight identity, three hand-checked prefixes, 13 of 16 masks containing {3,5}, one adjacent transposition with a different missing set, and one rejected call-count edit." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same census and controls under optimized Python. Failures are SystemExit, not assertions." + } + ] +} diff --git a/research/six-source-c7-witness-other-weights/verify.py b/research/six-source-c7-witness-other-weights/verify.py new file mode 100644 index 0000000000..c1aab4fb88 --- /dev/null +++ b/research/six-source-c7-witness-other-weights/verify.py @@ -0,0 +1,284 @@ +#!/usr/bin/env python3 +"""Exhaustive mask census of the recorded six-source c=7 witness. + +The word is the length-42 floor word recorded in PR #7016. A pair +0 <= s <= t <= 41 realizes a binary mask when q_s + q_t is congruent to +that mask modulo 7. This program classifies all 903 such pairs. + +Evidence class: exhaustive finite census of this one word. The domain is +finite, every pair is visited, and the visit count is checked against +42*43/2. This is not a depth-two block, not an unrestricted nonexistence +claim at c=7, and not a change of the selected conditional kappa. +""" + +import itertools +import math + +K = 6 +C = 7 +LENGTH = 42 +WITNESS = "023514103524310254054123145203452034213150" +# Nonzero masks with no realizing pair. (1, 3, 5) is the weight-3 gap +# already recorded for this word. The other two are the census result. +MISSING = {(1, 3, 5), (3, 5), (0, 1, 3, 5)} +OTHER_MISSING = ((3, 5), (0, 1, 3, 5)) +ALLOWED = {0, 1, 7, 8, 14} +MASK_BIT = {0: 0, 1: 1, 7: 0, 8: 1, 14: 0} +# Realizing pairs of each nonzero weight, from the same 903-pair census. +HIT_PAIRS = {1: 16, 2: 19, 3: 19, 4: 19, 5: 15, 6: 8} +ZERO_PAIRS = 8 +PAIR_COUNT = LENGTH * (LENGTH + 1) // 2 + + +def fail(message): + raise SystemExit("FAIL: " + message) + + +def support(mask): + return tuple(index for index, bit in enumerate(mask) if bit) + + +def fmt(groups): + return ";".join("(" + ",".join(str(index) for index in group) + ")" for group in groups) + + +def prefixes(letters): + """Prefix counts q_0, ..., q_42. Reject a word that is not a floor word.""" + if len(letters) != LENGTH or any(letter not in range(K) for letter in letters): + fail("not a length-42 word on sources 0..5") + if any(letters.count(source) != C for source in range(K)): + fail("not a floor word: a source is not called seven times") + running = [0] * K + table = [tuple(running)] + for letter in letters: + running[letter] += 1 + table.append(tuple(running)) + if len(table) != LENGTH + 1 or table[-1] != (C,) * K: + fail("final count is not seven calls of each source") + return table + + +def readings(total): + """Binary mask of one sum, or None if any coordinate fails. + + The allowed values {0, 1, 7, 8, 14} are exactly the integers in + {0, ..., 14} whose residue modulo 7 is 0 or 1. Both readings are + computed, and a disagreement is a failed control. + """ + allowed_bits = [] + modular_bits = [] + allowed_ok = True + modular_ok = True + for value in total: + if value not in ALLOWED: + allowed_ok = False + else: + allowed_bits.append(MASK_BIT[value]) + residue = value % C + if residue not in (0, 1): + modular_ok = False + else: + modular_bits.append(residue) + allowed_mask = tuple(allowed_bits) if allowed_ok else None + modular_mask = tuple(modular_bits) if modular_ok else None + if allowed_mask != modular_mask: + fail("allowed-set and mod-7 readings disagree on " + str(total)) + return allowed_mask + + +def census(letters): + """Classify every pair 0 <= s <= t <= 41. Return hits, zero count, visits.""" + table = prefixes(letters) + bounds = table[:LENGTH] + hits = {} + zero = 0 + examined = 0 + for left in range(LENGTH): + for right in range(left, LENGTH): + examined += 1 + total = tuple( + bounds[left][source] + bounds[right][source] for source in range(K) + ) + mask = readings(total) + if mask is None: + continue + if not any(mask): + zero += 1 + continue + weight = sum(mask) + if (left + right - weight) % C: + fail( + "weight identity failed at s=%s t=%s mask=%s" + % (left, right, mask) + ) + hits.setdefault(mask, []).append((left, right)) + if examined != PAIR_COUNT: + fail("pair enumeration visited %s pairs, expected %s" % (examined, PAIR_COUNT)) + return table, hits, zero + + +def classify(hits): + """Split all 63 nonzero masks into hits and misses.""" + missing = [] + hit_masks = {weight: 0 for weight in range(1, 7)} + pair_counts = {weight: 0 for weight in range(1, 7)} + universe = 0 + for mask in itertools.product((0, 1), repeat=K): + if not any(mask): + continue + universe += 1 + weight = sum(mask) + found = hits.get(mask, ()) + if found: + hit_masks[weight] += 1 + pair_counts[weight] += len(found) + else: + missing.append(support(mask)) + if universe != (1 << K) - 1: + fail("nonzero mask count is %s" % universe) + return missing, hit_masks, pair_counts + + +def hand_examples(table): + """Pairs a reviewer can check from the first six letters 023514.""" + if table[1] != (1, 0, 0, 0, 0, 0): + fail("q_1 is not e_0") + if table[3] != (1, 0, 1, 1, 0, 0): + fail("q_3 is not e_0 + e_2 + e_3") + if table[6] != (1, 1, 1, 1, 1, 1): + fail("q_6 is not the all-ones vector") + examples = ( + (table[1], (0,)), + (table[3], (0, 2, 3)), + (table[6], (0, 1, 2, 3, 4, 5)), + ) + for total, expect in examples: + mask = readings(total) + if mask is None or support(mask) != expect: + fail("hand example %s classified as %s" % (expect, mask)) + + +def boundary_adds_nothing(table, hits): + """q_42 = 7*1 is outside the depth-two range. It adds no new mask.""" + fresh = 0 + for left in range(LENGTH): + total = tuple(table[left][source] + table[LENGTH][source] for source in range(K)) + mask = readings(total) + if mask is not None and any(mask) and mask not in hits: + fresh += 1 + if fresh: + fail("boundary 42 realized %s new nonzero masks" % fresh) + return fresh + + +def superset_corollary(hits): + """Masks containing {3, 5}, other than the three misses, are realized. + + This is a restatement of the missing set. It blocks reading the census + as 'every mask that contains sources 3 and 5 is missed.' + """ + family = 0 + realized = 0 + for mask in itertools.product((0, 1), repeat=K): + if mask[3] != 1 or mask[5] != 1: + continue + family += 1 + if support(mask) in MISSING: + if mask in hits: + fail("listed miss %s was realized" % (support(mask),)) + else: + if mask not in hits: + fail("mask %s contains {3, 5} and was not realized" % (support(mask),)) + realized += 1 + if family != 16 or realized != 13: + fail("superset family %s realized %s" % (family, realized)) + return realized + + +def transposition_differs(witness_other): + """One adjacent swap stays a floor word and changes the missing set.""" + letters = [int(character) for character in WITNESS] + if letters[1] == letters[2]: + fail("positions 1 and 2 are the same source") + letters[1], letters[2] = letters[2], letters[1] + _, hits, _ = census(letters) + missing, _, _ = classify(hits) + other = tuple(sorted( + (mask for mask in missing if len(mask) != 3), + key=lambda mask: (len(mask), mask), + )) + if other == witness_other: + fail("transposed word has the same non-weight-3 missing set") + + +def reject_call_count_change(): + """The recorded one-letter edit is not a floor word.""" + letters = [int(character) for character in WITNESS] + if letters[0] != 0: + fail("witness does not start with source 0") + letters[0] = 1 + try: + prefixes(letters) + except SystemExit as error: + if str(error).startswith("FAIL: not a floor word"): + return + raise + fail("a word that calls source 0 six times was accepted") + + +def main(): + if WITNESS != "023514103524310254054123145203452034213150": + fail("witness literal changed") + if PAIR_COUNT != 903: + fail("complete pair count is not 903") + letters = [int(character) for character in WITNESS] + table, hits, zero = census(letters) + if zero != ZERO_PAIRS: + fail("zero-mask pair count %s" % zero) + hand_examples(table) + fresh = boundary_adds_nothing(table, hits) + missing, hit_masks, pair_counts = classify(hits) + if set(missing) != MISSING: + fail("missing masks changed: " + str(missing)) + if pair_counts != HIT_PAIRS: + fail("realizing-pair counts changed: " + str(pair_counts)) + for weight in range(1, 7): + expect = math.comb(K, weight) - (1 if weight in (2, 3, 4) else 0) + if hit_masks[weight] != expect: + fail("weight %s hit %s masks, expected %s" % (weight, hit_masks[weight], expect)) + other = tuple(sorted( + (mask for mask in missing if len(mask) != 3), + key=lambda mask: (len(mask), mask), + )) + weight3 = tuple(sorted(mask for mask in missing if len(mask) == 3)) + if other != OTHER_MISSING: + fail("non-weight-3 missing set changed: " + str(other)) + if weight3 != ((1, 3, 5),): + fail("weight-3 missing set changed: " + str(weight3)) + realized_superset = superset_corollary(hits) + transposition_differs(other) + reject_call_count_change() + nonzero_hit = sum(hit_masks.values()) + other_hit = nonzero_hit - hit_masks[3] + other_total = ((1 << K) - 1) - math.comb(K, 3) + print( + "PASS_SIX_SOURCE_C7_WITNESS_OTHER_WEIGHTS" + " pairs=%s nonzero_hit=%s/63 other_hit=%s/%s" + " missing_other=%s weight3_missing=%s" + " zero_pairs=%s boundary42_new=%s superset_realized=%s/16 controls=7" + % ( + PAIR_COUNT, + nonzero_hit, + other_hit, + other_total, + fmt(other), + fmt(weight3), + zero, + fresh, + realized_superset, + ) + ) + + +if __name__ == "__main__": + main()