Research: seven-source singleton universal path — length 18 excluded, f(7) >= 20 (no new kappa)

research/universal-f7-singleton-seedb859517b/CERTIFICATE-PROGRESS.json

@@ -0,0 +1 @@
+{"done": {"000": {"nodes": 2, "leaves": 0, "hits": 0, "words": []}, "001": {"nodes": 2, "leaves": 0, "hits": 0, "words": []}, "010": {"nodes": 1973843, "leaves": 33211, "hits": 0, "words": []}, "011": {"nodes": 3, "leaves": 0, "hits": 0, "words": []}, "012": {"nodes": 13802142, "leaves": 278853, "hits": 0, "words": []}}, "accum": {"nodes": 15775992, "leaves": 312064, "hits": 0, "words": []}}

research/universal-f7-singleton-seedb859517b/CERTIFICATE.json

@@ -0,0 +1,113 @@
+{
+  "conclusion": "f(7) >= 20 (length 18 excluded)",
+  "seconds": 117.0,
+  "tier1_reproduction": {
+    "n5": {
+      "counting_least_even_L": 10,
+      "gray_length": 12
+    },
+    "n5_L10": {
+      "matches_pinned": true,
+      "max_coverage": 31,
+      "records_sha256": "3dcc5689a4a34baec6424389a07dd917c0b681d6a894cba3e909f5a81efdc86e",
+      "words": 945
+    },
+    "n6": {
+      "counting_least_even_L": 14,
+      "gray_length": 16
+    },
+    "n6_L12": {
+      "matches_pinned": true,
+      "max_coverage": 49,
+      "records_sha256": "491b295f12cfa34a010dc23392b02d725dedcd0ba84111b31aa939a013d4958a",
+      "words": 10395
+    },
+    "n6_L14": {
+      "matches_pinned": true,
+      "max_coverage": 59,
+      "records_sha256": "3d711ffa192093103cc034bb5ab00c680d96667c9f6d1a509981b444663bc838",
+      "words": 945945
+    },
+    "n7": {
+      "counting_least_even_L": 18,
+      "gray_length": 24
+    }
+  },
+  "tier2_controls": {
+    "lemma_rows_8_8": {
+      "feasible": false,
+      "rows": 1
+    },
+    "lemma_rows_8_9": {
+      "feasible": false,
+      "rows": 3
+    },
+    "lemma_rows_9_8": {
+      "feasible": false,
+      "rows": 3
+    },
+    "lemma_rows_9_9": {
+      "feasible": true,
+      "rows": 55
+    },
+    "n5_nine_point": {
+      "covers": 0,
+      "max_coverage": 29,
+      "sets": 7888725
+    },
+    "n5_ten_point": {
+      "brute_covers": 99200,
+      "brute_sets": 20160075,
+      "cycle_realisable_covers": 0,
+      "joint_covers": 99200,
+      "joint_splits": [
+        [
+          2,
+          8
+        ],
+        [
+          3,
+          7
+        ],
+        [
+          4,
+          6
+        ],
+        [
+          5,
+          5
+        ],
+        [
+          6,
+          4
+        ],
+        [
+          7,
+          3
+        ],
+        [
+          8,
+          2
+        ]
+      ]
+    }
+  },
+  "tier3_f7": {
+    "admissible_splits_L18": [
+      [
+        9,
+        9
+      ]
+    ],
+    "census_nodes": 15775992,
+    "covers_found": null,
+    "joint_nodes": null,
+    "shards": 5,
+    "simple_18_cycles": 312064,
+    "size17_splits": {
+      "8_9": false,
+      "9_8": false
+    },
+    "universal_words": []
+  }
+}

research/universal-f7-singleton-seedb859517b/CLAIM.md

@@ -0,0 +1,75 @@
+# CLAIM — kappa-blocker KB3: the sharp singleton f(7) gap
+
+Agent: **Aaron Wang**, with help from opencode (substantial AI assistance; no
+independent human review claimed). Base main
+`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`; priority revision 4; catalogue
+SHA-256 `d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7`;
+selected-record SHA-256
+`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. Posted
+claim: https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18947532
+
+## Object and scope change
+
+In the PR943 prefix-walk model (`research/universal-connector-boundary`), a
+restored source word `w` over `n` singleton labels is universal when paired
+readouts realize every mask, `D(w) = {q_s xor q_t} = F2^n`; `f(n)` is the
+minimum word length. The pinned record is `f(5) = 12`, `f(6) = 16`,
+`18 <= f(7) <= 24` (`research/universal-connector-six-source/README.md`: "The
+exact value of `f(7)` is open"). This package decides or narrows that gap in
+the singleton alphabet only.
+
+**Scope status: changed** (authorized explicit-open-request scope change to the
+assigned kappa-blocker KB3; drawn track `adversarial-audit`, chooser seed
+`b859517b2b08394033ce4a4ab231ece8`). The drawn cards
+(`selected-stock-envelope`, `uniform-transfer-audit`,
+`supplier-boundary-audit`) are saturated or incremental at this base — the last
+two were completed within hours (discussion 1166 comments 18939154/18939459 and
+18939803/18940382). The distinct scopes of the DUO pair-source alphabet
+(https://github.com/CrocSwap/integer-mult-bounds/pull/2396,
+https://github.com/CrocSwap/integer-mult-bounds/pull/2128,
+https://github.com/CrocSwap/integer-mult-bounds/pull/2156) and the 63-mask
+weight-1/2/3 sparse family
+(https://github.com/CrocSwap/integer-mult-bounds/pull/2229,
+https://github.com/CrocSwap/integer-mult-bounds/pull/2236,
+https://github.com/CrocSwap/integer-mult-bounds/pull/2397) are recorded as
+concurrent scopes in `SOURCES.json`, not collisions.
+
+## Method
+
+Smallest falsifying instance first: the engine must reproduce the pinned
+five-source length-10 census (945 words, max 31/32) and six-source
+length-12/14 censuses (10,395 words, max 49/64; 945,945 words, max 59/64)
+byte-for-byte, including records SHA-256, before any new number is trusted.
+
+Then the length-18 census at `n = 7`, via the prefix vertex set `P = E union O`
+(`E` even-weight prefixes, `O` odd-weight prefixes; universality is exactly
+`P + P = F2^7`):
+
+1. Position parity gives `|E|, |O| <= 9`; counting gives `|E||O| >= 64` and
+   `C(|E|,2) + C(|O|,2) >= 63`.
+2. **Lemma A (pair-representation identity).** Every surviving 17-point split
+   `(9,8)` and `(8,9)` is contradictory: full odd coverage with 72 pairs forces
+   `sum_x A_x B_x >= 4`, while full even coverage forces at most one shared
+   nonzero pair-sum value, bounding the same sum by 1. Machine-checked rows are
+   in `CERTIFICATE.json`; an independent multiset enumeration re-derives them.
+   (The same lemma explains the community census fact that no nine-point set of
+   `F2^5` covers, max 29.)
+3. So a universal 18-word would walk a simple 18-cycle through an 18-point
+   cover with the `(9,9)` split. The joint `(E,O)` search enumerates every such
+   cover (increasing-order generation, exact 64-bit bitmasks, collision-budget
+   and coverage-capacity pruning — each prune a proved necessary condition),
+   and every cover found is tested for a Hamiltonian 18-cycle in the induced
+   hypercube.
+
+Controls and non-vacuity: the same joint search is validated at `n = 5` against
+a brute-force census of all C(31,9) ten-point sets (exact agreement on the
+number of covers) and reproduces the community nine-point result; `f(5) = 12`
+is re-confirmed by showing no ten-point cover is cycle-realisable.
+
+## Deliverable
+
+Either an exact length-18 exclusion (`f(7) >= 20`) or a universal word of
+length below 24 (`f(7) <= 22` or `20`), with exact coverage verification either
+way. No kappa, supplier or selected-frontier claim. One bounded pivot maximum
+(a length-20/22 construction screen on the same set engine) if the length-18
+census completes negative inside the priced budget.

research/universal-f7-singleton-seedb859517b/EXPECTED.json

@@ -0,0 +1,6 @@
+{
+  "conclusion": "f(7) >= 20 (length 18 excluded)",
+  "census_nodes": 15775992,
+  "simple_18_cycles": 312064,
+  "universal_words": 0
+}

research/universal-f7-singleton-seedb859517b/INDEPENDENT.json

@@ -0,0 +1,12 @@
+{
+  "control_sets": "ok",
+  "lemma_rows": {
+    "n5_5_4": "best_sum_AB=1 need=2",
+    "n5_5_5": "best_sum_AB=9 need=5",
+    "n7_8_8": "counting",
+    "n7_8_9": "best_sum_AB=1 need=4",
+    "n7_9_8": "best_sum_AB=1 need=4",
+    "n7_9_9": "best_sum_AB=25 need=9"
+  },
+  "witnesses_replayed": 0
+}

research/universal-f7-singleton-seedb859517b/NOTICE.md

@@ -0,0 +1,30 @@
+# Attribution and license
+
+Contribution by **Aaron Wang**, with help from opencode (substantial AI
+assistance in scoping, implementation, verification and writing; no independent
+human review claimed). New work is Apache-2.0, under the repository LICENSE.
+
+The model and the prefix-difference reduction are **Ross Richardson's PR943**
+(`research/universal-connector-boundary`). The pinned five- and six-source
+censuses, the values `f(5) = 12`, `f(6) = 16` and the recorded `f(7)` gap
+`18 <= f(7) <= 24` are **Douglas Colkitt's**
+(`research/universal-connector-six-source`, https://github.com/CrocSwap/integer-mult-bounds/pull/1185),
+which extends PR943. Both are read and reproduced here, never imported: no
+predecessor executable is vendored or called. Exact pins are in `SOURCES.json`.
+
+The community five-bit nine-point census fact (all 7,888,725 normalized
+nine-point sets of `F2^5`, maximum pair coverage 29, no cover) was published in
+the DUO-line coordination thread
+(https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18931315);
+this package re-derives it independently as a control and credits that source.
+
+The DUO pair-source alphabet work
+(https://github.com/CrocSwap/integer-mult-bounds/pull/2396,
+https://github.com/CrocSwap/integer-mult-bounds/pull/2128,
+https://github.com/CrocSwap/integer-mult-bounds/pull/2156) and the sparse
+weight-1/2/3 mask family
+(https://github.com/CrocSwap/integer-mult-bounds/pull/2229,
+https://github.com/CrocSwap/integer-mult-bounds/pull/2236,
+https://github.com/CrocSwap/integer-mult-bounds/pull/2397) are distinct scopes,
+recorded in `SOURCES.json`. Nothing here changes the selected frontier, any
+supplier or kappa.