From 4789d2cb28df9c1d6054f7945531d246e2b01bf5 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 03:57:06 -0400 Subject: [PATCH 1/3] Cap bounded-depth connector blocks: depth two holds log2 c + O(log log c) sources (no new kappa) A depth-d block on k sources at characteristic c satisfies 2^k - 1 <= k*min(k,c)*binom(kc+d-2,d-1), from the weight identity sum of read boundaries == |m| (mod c). Gray's 1/2 (PR6071) is the sharp leading constant for concatenations of depth<=2 blocks. Co-Authored-By: Claude Opus 5.5 --- .../connector-bounded-depth-cap/README.md | 203 +++++++++++ .../connector-bounded-depth-cap/SOURCES.json | 24 ++ .../connector-bounded-depth-cap/TASK.json | 74 ++++ .../connector-bounded-depth-cap/VERIFY.json | 36 ++ .../connector-bounded-depth-cap/verify.py | 332 ++++++++++++++++++ 5 files changed, 669 insertions(+) create mode 100644 research/connector-bounded-depth-cap/README.md create mode 100644 research/connector-bounded-depth-cap/SOURCES.json create mode 100644 research/connector-bounded-depth-cap/TASK.json create mode 100644 research/connector-bounded-depth-cap/VERIFY.json create mode 100644 research/connector-bounded-depth-cap/verify.py diff --git a/research/connector-bounded-depth-cap/README.md b/research/connector-bounded-depth-cap/README.md new file mode 100644 index 0000000000..f1a8ac505e --- /dev/null +++ b/research/connector-bounded-depth-cap/README.md @@ -0,0 +1,203 @@ +# Bounded-depth connector blocks: depth two caps at log₂ c + O(log log c) sources + +**Scoped upper bound for the unsigned dirty connector; no new κ.** +In the unchanged interface of PR4231/PR4248, a depth-d block on k sources in +characteristic c ≥ 2 satisfies + +```text +2^k − 1 ≤ k · min(k, c) · binom(kc + d − 2, d − 1). +``` + +For d = 2 this is `2^k − 1 ≤ k³c`, so every depth-two block has +`k ≤ 1 + log₂ c + 3 log₂ k` sources. Trivial pair counting allows about +2 log₂ c. Consequences: + +- The reflected-Gray blocks of [PR6071](https://github.com/CrocSwap/integer-mult-bounds/pull/6071) + (k = 1 + ⌊log₂ c⌋) are within O(log log c) of the largest possible + depth-two block. A depth-two block "near k ≈ 2 log₂ c", which PR6071's + open question 1 suggests looking for, does not exist once c is large. +- Every floor word built by concatenating blocks of depth at most two has + `n ≤ c · max(2, K₂(c)/2) = (1/2 + o(1)) c log₂ c` sources. PR6071's + `(1 + ⌊log₂ c⌋)⌊c/2⌋` lower bound attains this, so **1/2 is the sharp + leading constant for depth ≤ 2 block concatenations**. +- More generally, concatenations of blocks of depth at most D give at most + `(1 − 1/D + o(1)) c log₂ c` sources. A leading constant above 1/2 needs + blocks of depth at least three; reaching the counting constant 1 needs + depth that grows with c, or reads that are not organized in blocks. + +The general constant of N(c)/(c log₂ c) stays open in [1/2, 1]. This +package proves no new lower bound. + +```sh +python3.12 -I -W error -B research/connector-bounded-depth-cap/verify.py +``` + +Expected (about 2 s, standard library only): +`PASS_CONNECTOR_BOUNDED_DEPTH_CAP sources=1 census_cases=8 identity_checks=1031591 gray_blocks=21 gray_masks=741 cap_beats_trivial_from=2^6 controls=5 sha256=499b979ff5d691fd`. +Add `--table` to print the census and the capacity table below. + +## Interface and definitions (inherited) + +The interface is [PR4248](../connector-depth-blocks/README.md)'s unsigned +immutable-source, one-dirty-connector model, unchanged; no operation is added. +A floor word calls every source operator B_j exactly c times. Let q_t ∈ Z^k +be the integer count vector of the first t source calls of a word W, so +q_0 = 0 and q_{kc} = c·1. PR4248 says W has **depth d** on its k sources if +every nonzero binary mask m is congruent modulo c to a sum of at most d +prefixes q_t. Blocks of total depth at most c concatenate to a floor word, +and deleting a source keeps the depth (PR4248, PR6071). + +## Theorem (weight identity) + +**Lemma.** If `q_{a_1} + ... + q_{a_e} ≡ m (mod c)` for a binary mask m, then +`a_1 + ... + a_e ≡ |m| (mod c)`. + +*Proof.* Each source call increases one coordinate by one, so the coordinate +sum of q_t is t. Sum the congruence over all k coordinates. ∎ + +**Theorem.** A depth-d block on k sources at characteristic c ≥ 2, with +d ≥ 1, satisfies `2^k − 1 ≤ k · min(k, c) · binom(kc + d − 2, d − 1)`. + +*Proof.* Since q_{kc} ≡ 0 ≡ q_0, every read can use a boundary in +{0, ..., kc − 1}, and reads at boundary 0 pad any representation to exactly +d reads. So each nonzero mask m is represented by a multiset +{a_1 ≤ ... ≤ a_d} of these kc boundaries, and the multiset determines m. +Fix the sub-multiset {a_1, ..., a_{d−1}}: there are binom(kc + d − 2, d − 1) +choices. By the lemma, a_d ≡ |m| − (a_1 + ... + a_{d−1}) (mod c). The +weight |m| lies in {1, ..., k}, so it takes at most min(k, c) residues mod c. +Each residue has exactly k representatives in {0, ..., kc − 1}. So at most +k · min(k, c) values of a_d are possible, and each value determines m. ∎ + +Only additivity and the c-fold call count are used. The ring may be any +nonzero unital ring of characteristic c; the bound concerns schedules that are +correct for arbitrary compatible maps, as in PR4248. + +**Depth two.** `2^k − 1 ≤ k³c`. Since `2^(k−1) ≤ 2^k − 1` for k ≥ 1, +`k ≤ 1 + log₂ c + 3 log₂ k`. Write K₂(c) for the largest k that the +displayed inequality allows. By deletion, no block has more than K₂(c) +sources. + +**Fixed depth d ≥ 2.** `binom(kc + d − 2, d − 1) ≤ (kcd)^(d−1)`, so +`k ≤ 1 + 3 log₂ k + (d − 1)(log₂ c + log₂ k + log₂ d)`. Since k = O(d log c), +`k/d ≤ (1 − 1/d) log₂ c + O(log d + log log c)`. + +**Concatenation.** Let a floor word be a concatenation of blocks of depths +d_i ≤ D with Σ d_i ≤ c. Depth-one blocks carry at most two sources +(PR4248 Lemma C), so `n = Σ k_i ≤ c · max_{1 ≤ d ≤ D} K_d(c)/d`. For D = 2 +this is `n ≤ c · max(2, K₂(c)/2)`, which is `(1/2 + O(log log c / log c)) c log₂ c`. +PR6071 gives `n ≥ (1 + ⌊log₂ c⌋)⌊c/2⌋ + 2(c mod 2)`. Both ratios to +c log₂ c tend to 1/2. For D ≥ 3 the ceiling is `(1 − 1/D + o(1)) c log₂ c`; +no matching construction is supplied for D ≥ 3. + +The same lemma applied to a whole floor word (d = c, k = n) gives +`2^n − 1 ≤ n · min(n, c) · binom(cn + c − 2, c − 1)`. For n ≥ 2 this is +weaker than PR4248's counting bound `binom(cn + c − 1, c)`, because +`n · min(n, c) · c ≥ 2nc ≥ cn + c − 1`; the general constant 1 is untouched. The gain comes only when k is much smaller than c, +which is the regime of fixed-depth blocks. + +## Capacity table + +Exact evaluation of the largest k allowed (c = 2^e). "Trivial" is the +multiset count `2^k − 1 ≤ binom(kc + 1, 2)` for depth two. The ratios use +the D = 2 ceiling `c · max(2, K₂/2)` and PR6071's lower bound. + +| c | Gray k | K₂ (this) | trivial depth two | K₃ | K₄ | lower / (c log₂ c) | depth ≤ 2 upper / (c log₂ c) | +|---|---:|---:|---:|---:|---:|---:|---:| +| 2^8 | 9 | 21 | 24 | 35 | 49 | 0.5625 | 1.3125 | +| 2^16 | 17 | 30 | 41 | 54 | 76 | 0.5313 | 0.9375 | +| 2^32 | 33 | 48 | 75 | 88 | 128 | 0.5156 | 0.7500 | +| 2^64 | 65 | 83 | 141 | 156 | 228 | 0.5078 | 0.6484 | +| 2^128 | 129 | 149 | 271 | 287 | 425 | 0.5039 | 0.5820 | +| 2^1024 | 1025 | 1054 | 2069 | 2091 | 3127 | 0.5005 | 0.5146 | +| 2^4096 | 4097 | 4132 | 8217 | 8243 | 12353 | 0.5001 | 0.5044 | + +The new depth-two cap is stronger than pair counting from c = 2^6 on. +Convergence to 1/2 is only logarithmic in log c. **At practical c the cap is +loose**: at c = 2^8 it allows 21 sources, against 9 from Gray and 8 from +PR6061's largest finite template, and the upper ratio is above 1. The table is an evaluation of the +proved inequality, not a search for blocks. + +## Verification + +`verify.py` is standard library only and writes no files. + +- Source pin: the SHA256 of PR4248's README, the inherited definition. +- Exhaustive census of every floor word for (k, c) = (2, 2..5), (3, 2..4) and + (4, 2): 39,288 words. For each word and each depth d ∈ {1, 2} (and d = 3 + when kc ≤ 9), every multiset of boundaries that represents a binary mask is + checked against the weight identity, and for every fixed sub-multiset and + weight the number of admissible last reads is checked to be at most k. + 1,031,591 identity checks pass. The census confirms that no three-source + word has depth one (PR4248 Lemma C). +- Twenty-one reflected-Gray blocks (k = 1..7, three values of c each), built + separately from PR6071's README statement, have depth two on literal + words and satisfy the identity on every representing pair. +- The capacity table, the closed form `K₂ ≤ 1 + log₂ c + 3 log₂ K₂` at every + tabulated c, and exact (Fraction) ratio checks at c = 2^4096. +- Five controls are rejected: a word with a missing call, the identity with + the wrong modulus, a claimed block one source above K₂(1024), PR6071's + block with its downward suffix not reversed (loses depth two), and depth + one on three sources at c = 3. + +Finite checks support the written proof; they do not establish the +all-parameter theorem, which rests on the proof above. No AI or human +proof-kernel review is claimed beyond the review noted in the PR. + +## Scope, task and overlap + +Base `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. The +chooser drew `connector-alphabet-change` (seed +`9aa6e642b3ad1c5695053de603870c91`). **Scope changed**: the alphabet stays +fixed. This follows the general-family handoff in PR6071's open question 1 +(sharp leading constant of N(c)/(c log₂ c)) and settles its depth-two part. +It is a local interface side result. It does not pass a supplier budget gate, +add a native consumer or change the selected record. + +Nearest work, all crediting the retained connector lineage: + +- PR4231/PR4248 (Nick Petalas): interface, floor, prefix criterion, + concatenation/deletion, Lemma C (depth one carries at most two sources) + and the counting upper bound. This package is the depth-d analogue of + Lemma C. Pinned input: `research/connector-depth-blocks/README.md`. +- PR6035 (Nick Petalas, merged as `research/connector-five-halves-growth`), + PR6057 (zxv), PR6061 (JosieElliston): finite depth-two blocks on five to + eight sources. +- PR6071 (apoursh), head `a0f08278dd755e0bf228855e45c5efaa3b8ad97a`: the + Gray-walk depth-two blocks and N(c) = Θ(c log c). Its open question 1 is + the question addressed here. Pending; used for comparison and to rebuild + its block in the verifier, not as an executable dependency. + +The overlap search (`scripts/find_overlap.py --task connector-alphabet-change`, +live discussions and open PRs, searches for "leading constant" and Gray) found +no earlier upper bound on depth-two block size beyond pair counting. That is +not a novelty certificate. + +## Open next questions + +1. **Is there a depth-three block family with k ≈ 2 log₂ c?** It would raise + the lower constant to 2/3, the most the theorem allows for depth three. + *Why:* depth ≤ 2 blocks are now capped at 1/2, so this is the cheapest + possible improvement of the lower constant. *First step:* by the + theorem, almost every pair of first reads must extend to a mask, so search + small c (8 to 32) for depth-three blocks with k > 2 + 2 log₂ c and look + for structure. Informal remark, not checked by the verifier: a Gray pair + plus one extra read does not suffice, because the extra read's prefix must + lie in {−1, 0, 1}^k mod c, and a monotone prefix chain has at most 4k + 1 + such values. *Blocked by:* no construction known. +2. **The general constant in [1/2, 1].** Concatenations of depth ≤ D blocks + are capped at 1 − 1/D. Do words with unbounded block depth, or reads that + cross block boundaries, beat 1/2? *First step:* sharpen the global count + by also using the coordinate structure of each read, not only its weight. +3. **Exact depth-two capacity at small c.** The cap is loose at practical c + (21 against 9 at c = 2^8). *First step:* exact search at c = 8..16 to see + whether depth-two blocks beyond Gray plus O(log log c) exist; balanced + Gray codes (Bhat–Savage) suggest about log₂ c + log₂ log₂ c is reachable. + +## Credit + +Prepared by JosieElliston with substantial Anthropic Claude (Claude Code, +session 40) assistance. Nick Petalas supplies PR4231/4248/6035 and the retained +Ross Richardson PR934/943 and Riquelme Soares lineage; apoursh's PR6071 +supplies the Gray-walk construction and the open question; zxv's PR6057 and +PR6061 supply finite depth-two blocks. Reflected Gray codes and balanced Gray +codes are established combinatorics. Apache-2.0; no predecessor file changes. diff --git a/research/connector-bounded-depth-cap/SOURCES.json b/research/connector-bounded-depth-cap/SOURCES.json new file mode 100644 index 0000000000..739918f47a --- /dev/null +++ b/research/connector-bounded-depth-cap/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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-depth-blocks/README.md", + "usage": "input", + "git_blob": "5d5b4a5b96e05f3818ff454d4dfdc5dc2959f6b4", + "sha256": "0ce59767f249b24d65d7d14b466115858d82c0bbfaaa8eab46b7406f4e975331" + } + ] +} diff --git a/research/connector-bounded-depth-cap/TASK.json b/research/connector-bounded-depth-cap/TASK.json new file mode 100644 index 0000000000..f936bb2c5e --- /dev/null +++ b/research/connector-bounded-depth-cap/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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": "Upper bound on bounded-depth blocks of the unchanged unsigned dirty connector (PR4231/PR4248 interface): a depth-d block on k sources at characteristic c has 2^k-1 <= k*min(k,c)*binom(kc+d-2,d-1); depth-two blocks have at most log2 c + O(log log c) sources; concatenations of depth<=2 blocks have sharp leading constant 1/2 (matched by PR6071), and depth<=D concatenations are capped at (1-1/D+o(1)) c log2 c.", + "scope_change_reason": "The alphabet stays fixed. This follows the released general-family handoff, PR6071 open question 1 (sharp leading constant of N(c)/(c log2 c)), and settles its depth-two part: it shows that the suggested search for depth-two blocks near 2 log2 c cannot succeed for large c.", + "bottleneck_link": "Side result on recursive-interface capacity. It changes no supplier or kappa; it redirects further N(c) constructions from depth-two blocks to depth>=3 or non-block words.", + "budget_minutes": 60, + "stop_rule": "Stop at the proved cap plus a literal-word verifier; do not start a depth-three construction search in this session.", + "outcome": "completed", + "evidence": "README proof (weight identity); verify.py: exhaustive census of 39,288 small floor words with 1,031,591 identity checks, 21 rebuilt Gray blocks, exact capacity table to c=2^4096, five rejected controls. Standard library only.", + "author": "JosieElliston (Claude Code session 40)", + "ai_assistance": "Substantial: Anthropic Claude (Claude Code session 40) derived the proof, wrote the verifier and README; optional OpenAI Codex read-only review.", + "open_questions": [ + { + "question": "Is there a depth-three block family with k ~ 2 log2 c (lower constant 2/3)?", + "why_it_matters": "Depth<=2 concatenations are capped at constant 1/2; depth three is the cheapest route to a larger lower constant.", + "first_step": "Search small c (8..32) for depth-three blocks with k > 2 + 2 log2 c; by the theorem most first-read pairs must extend to a mask.", + "blocked_by": "No construction known." + }, + { + "question": "Is the general constant of N(c)/(c log2 c) above 1/2, and is it 1?", + "why_it_matters": "Fixed-depth block concatenations are capped at 1-1/D; the counting constant 1 needs unbounded depth or cross-block reads.", + "first_step": "Sharpen the global count using the coordinate structure of each read, not only its weight.", + "blocked_by": "Global counting gains nothing from the weight identity when n >= 2." + }, + { + "question": "What is the exact largest depth-two block at small c?", + "why_it_matters": "The cap is loose at practical c (21 against Gray 9 at c=2^8).", + "first_step": "Exact search at c=8..16; balanced Gray codes suggest about log2 c + log2 log2 c is reachable.", + "blocked_by": "Search size." + } + ] +} diff --git a/research/connector-bounded-depth-cap/VERIFY.json b/research/connector-bounded-depth-cap/VERIFY.json new file mode 100644 index 0000000000..e4e7cecb69 --- /dev/null +++ b/research/connector-bounded-depth-cap/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-depth-blocks/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source pin; exhaustive census of 39,288 floor words (k,c) in {(2,2..5),(3,2..4),(4,2)} with weight-identity and per-weight last-read checks at depths 1,2 (3 when kc<=9); 21 rebuilt reflected-Gray depth-two blocks; exact capacity table to c=2^4096; five rejected controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat every check under optimized Python; checks use explicit exceptions, not assert." + } + ] +} diff --git a/research/connector-bounded-depth-cap/verify.py b/research/connector-bounded-depth-cap/verify.py new file mode 100644 index 0000000000..692542565a --- /dev/null +++ b/research/connector-bounded-depth-cap/verify.py @@ -0,0 +1,332 @@ +#!/usr/bin/env python3 +"""Verify the bounded-depth block capacity bound for the unsigned connector. + +Claim (README): a depth-d block on k sources in characteristic c >= 2, i.e. a +word using each source exactly c times in which every nonzero binary mask is a +sum of at most d prefix-count vectors modulo c, satisfies + + 2^k - 1 <= k * min(k, c) * binom(k*c + d - 2, d - 1). + +The proof is the weight identity: boundary t has coordinate sum t, so the read +boundaries of a mask m sum to |m| modulo c. This script checks the identity +and the per-weight candidate count on literal words (an exhaustive census of +small words and independently rebuilt reflected-Gray blocks), evaluates the +explicit capacity tables, and rejects mutation controls. Finite checks support +the written proof; they do not replace it. Standard library only. + +JosieElliston (Claude Code session 40, Anthropic Claude assistance). Apache-2.0. +""" + +from __future__ import annotations + +import hashlib +import itertools +import json +import math +from fractions import Fraction +import pathlib +import sys + +HERE = pathlib.Path(__file__).resolve().parent +ROOT = HERE.parent.parent + + +class Fail(Exception): + pass + + +def need(cond: bool, msg: str) -> None: + if not cond: + raise Fail(msg) + + +# ---------------------------------------------------------------- sources + +def check_sources() -> int: + data = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + n = 0 + for row in data["files"]: + if row["usage"] != "input": + continue + raw = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row["sha256"], + f"source hash mismatch: {row['path']}") + n += 1 + return n + + +# ---------------------------------------------------------------- words + +def validate_word(word, k, c): + need(len(word) == k * c, "word length must be k*c") + counts = [0] * k + for s in word: + need(0 <= s < k, "source label out of range") + counts[s] += 1 + need(all(x == c for x in counts), "every source must occur exactly c times") + + +def prefixes(word, k): + """Integer prefix-count vectors q_0..q_{kc} as tuples.""" + q = [0] * k + out = [tuple(q)] + for s in word: + q[s] += 1 + out.append(tuple(q)) + return out + + +def mask_of(vec, c): + """Return the binary mask (as int) if vec is binary mod c, else None.""" + m = 0 + for j, x in enumerate(vec): + r = x % c + if r == 1: + m |= 1 << j + elif r != 0: + return None + return m + + +def cover(word, k, c, d, audit=True): + """Nonzero masks represented by multisets of <= d boundaries in [0, kc-1]. + + Boundary kc has prefix c*1 == 0 = q_0 mod c, so it is never needed. + With audit=True, every representing multiset is checked against the + weight identity sum(a_i) == |m| (mod c), and for every (d'-1)-prefix + multiset and weight w the number of admissible last boundaries is <= k. + Returns (set_of_masks, number_of_identity_checks). + """ + validate_word(word, k, c) + q = prefixes(word, k) + T = k * c + masks = set() + checks = 0 + for e in range(1, d + 1): + for head in itertools.combinations_with_replacement(range(T), e - 1): + base = [0] * k + for a in head: + for j in range(k): + base[j] += q[a][j] + lo = head[-1] if head else 0 + per_weight = {} + for a in range(lo, T): + vec = [base[j] + q[a][j] for j in range(k)] + m = mask_of(vec, c) + if m is None or m == 0: + continue + masks.add(m) + if audit: + w = bin(m).count("1") + need((sum(head) + a - w) % c == 0, + f"weight identity fails: word={word} reads={head + (a,)}") + per_weight[w] = per_weight.get(w, 0) + 1 + checks += 1 + for w, cnt in per_weight.items(): + need(cnt <= k, "more than k last-read candidates for one weight") + return masks, checks + + +def multiset_words(k, c): + """All words with each of k labels exactly c times (lexicographic).""" + counts = [c] * k + word = [] + + def rec(): + if len(word) == k * c: + yield tuple(word) + return + for s in range(k): + if counts[s]: + counts[s] -= 1 + word.append(s) + yield from rec() + word.pop() + counts[s] += 1 + + yield from rec() + + +# ---------------------------------------------------------------- bounds + +def cap_rhs(k, c, d): + return k * min(k, c) * math.comb(k * c + d - 2, d - 1) + + +def trivial_rhs(k, c, d): + # multisets of exactly d boundaries among the kc residue-distinct ones + return math.comb(k * c + d - 1, d) + + +def first_fail(c, d, rhs): + k = 1 + while (1 << k) - 1 <= rhs(k, c, d): + k += 1 + return k + + +def gray_lower(c): + b = 1 + (c.bit_length() - 1) + return b * (c // 2) + 2 * (c % 2) + + +# ---------------------------------------------------------------- Gray blocks +# Independent rebuild of the PR6071 construction from its README statement: +# upward labels A, nonnegative middle fill, reversed downward labels B. + +def gray_block(k, c): + labels = [] + g = 0 + up = [] + down = [] + for i in range(1, 1 << k): + j = (i & -i).bit_length() - 1 + labels.append(j) + if (g >> j) & 1: + down.append(j) + else: + up.append(j) + g ^= 1 << j + flips = [labels.count(j) for j in range(k)] + need(max(flips) <= c, "Gray block needs c >= 2^(k-1)") + middle = [j for j in range(k) for _ in range(c - flips[j])] + return tuple(up + middle + list(reversed(down))) + + +# ---------------------------------------------------------------- controls + +def run_controls(): + rejected = 0 + # 1. word with one source short + try: + validate_word((0, 0, 1), 2, 2) + except Fail: + rejected += 1 + # 2. weight identity with the wrong modulus is not an invariant + w = gray_block(3, 4) + q = prefixes(w, 3) + bad = False + for a in range(12): + for s in range(a, 12): + vec = [q[a][j] + q[s][j] for j in range(3)] + m = mask_of(vec, 4) + if m and (a + s - bin(m).count("1")) % 5 != 0: + bad = True + if bad: + rejected += 1 + # 3. a claimed depth-two block above the cap at c=1024 (k=K_2+1) is excluded + c = 1024 + k = first_fail(c, 2, cap_rhs) + if (1 << k) - 1 > cap_rhs(k, c, 2): + rejected += 1 + # 4. the Gray block with its downward suffix not reversed loses depth two + k, c = 4, 8 + up, down, g = [], [], 0 + for i in range(1, 1 << k): + j = (i & -i).bit_length() - 1 + (down if (g >> j) & 1 else up).append(j) + g ^= 1 << j + flips = [up.count(j) + down.count(j) for j in range(k)] + mid = [j for j in range(k) for _ in range(c - flips[j])] + wrong = tuple(up + mid + down) + got, _ = cover(wrong, k, c, 2, audit=True) + if len(got) < (1 << k) - 1: + rejected += 1 + # 5. depth one cannot cover three sources (PR4248 Lemma C) at c=3 + best = max(len(cover(wd, 3, 3, 1, audit=True)[0]) for wd in multiset_words(3, 3)) + if best < 7: + rejected += 1 + return rejected + + +# ---------------------------------------------------------------- main + +def main() -> int: + n_src = check_sources() + + # Exhaustive census of small words: identity + per-weight candidate count + census = {} + total_checks = 0 + for (k, c) in [(2, 2), (2, 3), (2, 4), (2, 5), (3, 2), (3, 3), (3, 4), (4, 2)]: + words = 0 + best = {1: 0, 2: 0, 3: 0} + for wd in multiset_words(k, c): + words += 1 + for d in (1, 2, 3): + if d == 3 and k * c > 9: + continue + got, chk = cover(wd, k, c, d) + total_checks += chk + need(len(got) <= cap_rhs(k, c, d), "cap violated on a literal word") + best[d] = max(best[d], len(got)) + census[f"k={k},c={c}"] = {"words": words, "max_cover_d1": best[1], + "max_cover_d2": best[2], + "max_cover_d3": best[3] if k * c <= 9 else None} + expected_words = {"k=2,c=2": 6, "k=2,c=3": 20, "k=2,c=4": 70, "k=2,c=5": 252, + "k=3,c=2": 90, "k=3,c=3": 1680, "k=3,c=4": 34650, + "k=4,c=2": 2520} + for key, n in expected_words.items(): + need(census[key]["words"] == n, f"census size {key}") + # depth one carries at most two sources (PR4248 Lemma C): no k=3 word has depth one + for key in ("k=3,c=2", "k=3,c=3", "k=3,c=4"): + need(census[key]["max_cover_d1"] < 7, "unexpected depth-one three-source word") + + # Gray blocks: depth two on literal words, identity audited + gray = 0 + gray_masks = 0 + for k in range(1, 8): + base = max(2, 1 << (k - 1)) + for c in (base, base + 1, base + 3): + got, chk = cover(gray_block(k, c), k, c, 2) + need(len(got) == (1 << k) - 1, f"Gray block k={k} c={c} not depth two") + need((1 << k) - 1 <= cap_rhs(k, c, 2), "Gray block above cap") + total_checks += chk + gray += 1 + gray_masks += len(got) + + # Capacity tables + table = [] + for e in list(range(1, 21)) + [24, 32, 40, 48, 64, 96, 128, 256, 1024, 4096]: + c = 1 << e + k2 = first_fail(c, 2, cap_rhs) - 1 + t2 = first_fail(c, 2, trivial_rhs) - 1 + k3 = first_fail(c, 3, cap_rhs) - 1 + k4 = first_fail(c, 4, cap_rhs) - 1 + g = 1 + e # Gray block size at c = 2^e + # explicit closed form: 2^(k-1) <= k^3 c => k <= 1 + log2 c + 3 log2 k + need(k2 <= 1 + e + 3 * math.log2(k2) + 1e-9, "closed form fails") + need(g <= k2, "Gray block exceeds the cap (impossible)") + # n <= c * max(2, K_2/2) for depth<=2 concatenations; ratios exact + upper_ratio = Fraction(max(4, k2), 2 * e) + lower_ratio = Fraction(gray_lower(c), c * e) + table.append({"c": f"2^{e}", "gray_k": g, "cap_k_d2": k2, + "trivial_k_d2": t2, "cap_k_d3": k3, "cap_k_d4": k4, + "N_le2_lower_over_clog2c": str(round(lower_ratio, 6)), + "N_le2_upper_over_clog2c": str(round(upper_ratio, 6))}) + # sanity of the asymptotic message at the largest entry + last = table[-1] + need(Fraction(last["N_le2_upper_over_clog2c"]) < Fraction(506, 1000), "depth<=2 upper ratio not near 1/2") + need(Fraction(last["N_le2_lower_over_clog2c"]) > Fraction(49, 100), "Gray ratio not near 1/2") + need(last["trivial_k_d2"] > 1.99 * 4096, "trivial depth-two count should be ~2 log2 c") + # the cap is strictly better than trivial pair counting from c = 2^7 on + crossover = min(int(r["c"][2:]) for r in table if r["cap_k_d2"] < r["trivial_k_d2"]) + + controls = run_controls() + need(controls == 5, f"only {controls}/5 controls rejected") + + digest = hashlib.sha256(json.dumps({"census": census, "table": table}, + sort_keys=True).encode()).hexdigest() + if "--table" in sys.argv: + print(json.dumps({"census": census, "table": table}, indent=1)) + print(f"PASS_CONNECTOR_BOUNDED_DEPTH_CAP sources={n_src} census_cases={len(census)} " + f"identity_checks={total_checks} gray_blocks={gray} gray_masks={gray_masks} " + f"cap_beats_trivial_from=2^{crossover} controls={controls} sha256={digest[:16]}") + return 0 + + +if __name__ == "__main__": + try: + sys.exit(main()) + except Fail as exc: + print(f"FAIL {exc}") + sys.exit(1) From 2055b98c0b7946a7f0a3008fe56112583b0c2bbb Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 03:58:41 -0400 Subject: [PATCH 2/3] Clarify concatenation family and note the general constant interval Co-Authored-By: Claude Opus 5.5 --- research/connector-bounded-depth-cap/README.md | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/research/connector-bounded-depth-cap/README.md b/research/connector-bounded-depth-cap/README.md index f1a8ac505e..0443f6bf18 100644 --- a/research/connector-bounded-depth-cap/README.md +++ b/research/connector-bounded-depth-cap/README.md @@ -16,11 +16,13 @@ For d = 2 this is `2^k − 1 ≤ k³c`, so every depth-two block has (k = 1 + ⌊log₂ c⌋) are within O(log log c) of the largest possible depth-two block. A depth-two block "near k ≈ 2 log₂ c", which PR6071's open question 1 suggests looking for, does not exist once c is large. -- Every floor word built by concatenating blocks of depth at most two has +- Every floor word built by PR4248's concatenation (blocks with depths + summing to at most c, each mask read inside each block) using blocks of + depth at most two has `n ≤ c · max(2, K₂(c)/2) = (1/2 + o(1)) c log₂ c` sources. PR6071's `(1 + ⌊log₂ c⌋)⌊c/2⌋` lower bound attains this, so **1/2 is the sharp leading constant for depth ≤ 2 block concatenations**. -- More generally, concatenations of blocks of depth at most D give at most +- More generally, such concatenations of blocks of depth at most D give at most `(1 − 1/D + o(1)) c log₂ c` sources. A leading constant above 1/2 needs blocks of depth at least three; reaching the counting constant 1 needs depth that grows with c, or reads that are not organized in blocks. @@ -89,6 +91,13 @@ PR6071 gives `n ≥ (1 + ⌊log₂ c⌋)⌊c/2⌋ + 2(c mod 2)`. Both ratios to c log₂ c tend to 1/2. For D ≥ 3 the ceiling is `(1 − 1/D + o(1)) c log₂ c`; no matching construction is supplied for D ≥ 3. +**The general constant is at most 1.** PR4248's count `2^n − 1 ≤ binom(cn + c − 1, c)` +and `binom(N, c) ≤ (eN/c)^c` give `2^n − 1 ≤ (e(n + 1))^c`, so +`n ≤ 1 + c log₂(e(n + 1))`. With PR6071's `n < 4c(⌈log₂ c⌉ + 1)` this is +`n ≤ (1 + O(log log c / log c)) c log₂ c`. So N(c)/(c log₂ c) has liminf at +least 1/2 (PR6071) and limsup at most 1. This sharpening of the counting +asymptotic is routine and is stated only to fix the interval. + The same lemma applied to a whole floor word (d = c, k = n) gives `2^n − 1 ≤ n · min(n, c) · binom(cn + c − 2, c − 1)`. For n ≥ 2 this is weaker than PR4248's counting bound `binom(cn + c − 1, c)`, because From e4528e2c43cc4284208744fe163baae8d5da6490 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 04:00:33 -0400 Subject: [PATCH 3/3] Address review: exact depth-two inequality, K_d definition, exact ratio checks, drop circular control Co-Authored-By: Claude Opus 5.5 --- .../connector-bounded-depth-cap/README.md | 29 ++++++++++--------- .../connector-bounded-depth-cap/TASK.json | 2 +- .../connector-bounded-depth-cap/VERIFY.json | 2 +- .../connector-bounded-depth-cap/verify.py | 17 +++++------ 4 files changed, 25 insertions(+), 25 deletions(-) diff --git a/research/connector-bounded-depth-cap/README.md b/research/connector-bounded-depth-cap/README.md index 0443f6bf18..0127ee2009 100644 --- a/research/connector-bounded-depth-cap/README.md +++ b/research/connector-bounded-depth-cap/README.md @@ -8,7 +8,7 @@ characteristic c ≥ 2 satisfies 2^k − 1 ≤ k · min(k, c) · binom(kc + d − 2, d − 1). ``` -For d = 2 this is `2^k − 1 ≤ k³c`, so every depth-two block has +For d = 2 this is `2^k − 1 ≤ k² c · min(k, c) ≤ k³c`, so every depth-two block has `k ≤ 1 + log₂ c + 3 log₂ k` sources. Trivial pair counting allows about 2 log₂ c. Consequences: @@ -35,7 +35,7 @@ python3.12 -I -W error -B research/connector-bounded-depth-cap/verify.py ``` Expected (about 2 s, standard library only): -`PASS_CONNECTOR_BOUNDED_DEPTH_CAP sources=1 census_cases=8 identity_checks=1031591 gray_blocks=21 gray_masks=741 cap_beats_trivial_from=2^6 controls=5 sha256=499b979ff5d691fd`. +`PASS_CONNECTOR_BOUNDED_DEPTH_CAP sources=1 census_cases=8 identity_checks=1031591 gray_blocks=21 gray_masks=741 cap_beats_trivial_from=2^6 controls=4 sha256=499b979ff5d691fd`. Add `--table` to print the census and the capacity table below. ## Interface and definitions (inherited) @@ -74,9 +74,11 @@ Only additivity and the c-fold call count are used. The ring may be any nonzero unital ring of characteristic c; the bound concerns schedules that are correct for arbitrary compatible maps, as in PR4248. -**Depth two.** `2^k − 1 ≤ k³c`. Since `2^(k−1) ≤ 2^k − 1` for k ≥ 1, -`k ≤ 1 + log₂ c + 3 log₂ k`. Write K₂(c) for the largest k that the -displayed inequality allows. By deletion, no block has more than K₂(c) +**Depth two.** `2^k − 1 ≤ k² c · min(k, c) ≤ k³c`. Since `2^(k−1) ≤ 2^k − 1` for k ≥ 1, +`k ≤ 1 + log₂ c + 3 log₂ k`. For d ≥ 2 write K_d(c) for the largest k that the exact theorem inequality +`2^k − 1 ≤ k · min(k, c) · binom(kc + d − 2, d − 1)` allows (the verifier and +table use this exact form, not the k³c relaxation); set K₁ = 2 by PR4248 +Lemma C. By deletion, no block has more than K₂(c) sources. **Fixed depth d ≥ 2.** `binom(kc + d − 2, d − 1) ≤ (kcd)^(d−1)`, so @@ -142,11 +144,13 @@ proved inequality, not a search for blocks. separately from PR6071's README statement, have depth two on literal words and satisfy the identity on every representing pair. - The capacity table, the closed form `K₂ ≤ 1 + log₂ c + 3 log₂ K₂` at every - tabulated c, and exact (Fraction) ratio checks at c = 2^4096. -- Five controls are rejected: a word with a missing call, the identity with - the wrong modulus, a claimed block one source above K₂(1024), PR6071's - block with its downward suffix not reversed (loses depth two), and depth - one on three sources at c = 3. + tabulated c, and exact Fraction comparisons of both ratios at c = 2^4096 + (the printed table rounds them to six decimals). +- Four controls are rejected: a word with a missing call, the identity with + the wrong modulus, PR6071's block with its downward suffix not reversed + (loses depth two), and depth one on three sources at c = 3. The table + itself is arithmetic on the proved inequality, not an independent check of + the theorem. Finite checks support the written proof; they do not establish the all-parameter theorem, which rests on the proof above. No AI or human @@ -186,10 +190,9 @@ not a novelty certificate. 1. **Is there a depth-three block family with k ≈ 2 log₂ c?** It would raise the lower constant to 2/3, the most the theorem allows for depth three. *Why:* depth ≤ 2 blocks are now capped at 1/2, so this is the cheapest - possible improvement of the lower constant. *First step:* by the - theorem, almost every pair of first reads must extend to a mask, so search + possible improvement of the lower constant. *First step:* search small c (8 to 32) for depth-three blocks with k > 2 + 2 log₂ c and look - for structure. Informal remark, not checked by the verifier: a Gray pair + for structure among the first-read pairs that extend to a mask. Informal remark, not checked by the verifier: a Gray pair plus one extra read does not suffice, because the extra read's prefix must lie in {−1, 0, 1}^k mod c, and a monotone prefix chain has at most 4k + 1 such values. *Blocked by:* no construction known. diff --git a/research/connector-bounded-depth-cap/TASK.json b/research/connector-bounded-depth-cap/TASK.json index f936bb2c5e..8bd9ab8d37 100644 --- a/research/connector-bounded-depth-cap/TASK.json +++ b/research/connector-bounded-depth-cap/TASK.json @@ -48,7 +48,7 @@ "budget_minutes": 60, "stop_rule": "Stop at the proved cap plus a literal-word verifier; do not start a depth-three construction search in this session.", "outcome": "completed", - "evidence": "README proof (weight identity); verify.py: exhaustive census of 39,288 small floor words with 1,031,591 identity checks, 21 rebuilt Gray blocks, exact capacity table to c=2^4096, five rejected controls. Standard library only.", + "evidence": "README proof (weight identity); verify.py: exhaustive census of 39,288 small floor words with 1,031,591 identity checks, 21 rebuilt Gray blocks, exact capacity table to c=2^4096, four rejected controls. Standard library only.", "author": "JosieElliston (Claude Code session 40)", "ai_assistance": "Substantial: Anthropic Claude (Claude Code session 40) derived the proof, wrote the verifier and README; optional OpenAI Codex read-only review.", "open_questions": [ diff --git a/research/connector-bounded-depth-cap/VERIFY.json b/research/connector-bounded-depth-cap/VERIFY.json index e4e7cecb69..5b549003c6 100644 --- a/research/connector-bounded-depth-cap/VERIFY.json +++ b/research/connector-bounded-depth-cap/VERIFY.json @@ -17,7 +17,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Source pin; exhaustive census of 39,288 floor words (k,c) in {(2,2..5),(3,2..4),(4,2)} with weight-identity and per-weight last-read checks at depths 1,2 (3 when kc<=9); 21 rebuilt reflected-Gray depth-two blocks; exact capacity table to c=2^4096; five rejected controls." + "checks": "Source pin; exhaustive census of 39,288 floor words (k,c) in {(2,2..5),(3,2..4),(4,2)} with weight-identity and per-weight last-read checks at depths 1,2 (3 when kc<=9); 21 rebuilt reflected-Gray depth-two blocks; exact capacity table to c=2^4096; four rejected controls." }, { "argv": [ diff --git a/research/connector-bounded-depth-cap/verify.py b/research/connector-bounded-depth-cap/verify.py index 692542565a..7d377771a1 100644 --- a/research/connector-bounded-depth-cap/verify.py +++ b/research/connector-bounded-depth-cap/verify.py @@ -214,12 +214,7 @@ def run_controls(): bad = True if bad: rejected += 1 - # 3. a claimed depth-two block above the cap at c=1024 (k=K_2+1) is excluded - c = 1024 - k = first_fail(c, 2, cap_rhs) - if (1 << k) - 1 > cap_rhs(k, c, 2): - rejected += 1 - # 4. the Gray block with its downward suffix not reversed loses depth two + # 3. the Gray block with its downward suffix not reversed loses depth two k, c = 4, 8 up, down, g = [], [], 0 for i in range(1, 1 << k): @@ -232,7 +227,7 @@ def run_controls(): got, _ = cover(wrong, k, c, 2, audit=True) if len(got) < (1 << k) - 1: rejected += 1 - # 5. depth one cannot cover three sources (PR4248 Lemma C) at c=3 + # 4. depth one cannot cover three sources (PR4248 Lemma C) at c=3 best = max(len(cover(wd, 3, 3, 1, audit=True)[0]) for wd in multiset_words(3, 3)) if best < 7: rejected += 1 @@ -286,6 +281,7 @@ def main() -> int: # Capacity tables table = [] + exact_ratios = [] for e in list(range(1, 21)) + [24, 32, 40, 48, 64, 96, 128, 256, 1024, 4096]: c = 1 << e k2 = first_fail(c, 2, cap_rhs) - 1 @@ -299,20 +295,21 @@ def main() -> int: # n <= c * max(2, K_2/2) for depth<=2 concatenations; ratios exact upper_ratio = Fraction(max(4, k2), 2 * e) lower_ratio = Fraction(gray_lower(c), c * e) + exact_ratios.append((lower_ratio, upper_ratio)) table.append({"c": f"2^{e}", "gray_k": g, "cap_k_d2": k2, "trivial_k_d2": t2, "cap_k_d3": k3, "cap_k_d4": k4, "N_le2_lower_over_clog2c": str(round(lower_ratio, 6)), "N_le2_upper_over_clog2c": str(round(upper_ratio, 6))}) # sanity of the asymptotic message at the largest entry last = table[-1] - need(Fraction(last["N_le2_upper_over_clog2c"]) < Fraction(506, 1000), "depth<=2 upper ratio not near 1/2") - need(Fraction(last["N_le2_lower_over_clog2c"]) > Fraction(49, 100), "Gray ratio not near 1/2") + need(exact_ratios[-1][1] < Fraction(506, 1000), "depth<=2 upper ratio not near 1/2") + need(exact_ratios[-1][0] > Fraction(49, 100), "Gray ratio not near 1/2") need(last["trivial_k_d2"] > 1.99 * 4096, "trivial depth-two count should be ~2 log2 c") # the cap is strictly better than trivial pair counting from c = 2^7 on crossover = min(int(r["c"][2:]) for r in table if r["cap_k_d2"] < r["trivial_k_d2"]) controls = run_controls() - need(controls == 5, f"only {controls}/5 controls rejected") + need(controls == 4, f"only {controls}/4 controls rejected") digest = hashlib.sha256(json.dumps({"census": census, "table": table}, sort_keys=True).encode()).hexdigest()