diff --git a/research/connector-gray-growth/README.md b/research/connector-gray-growth/README.md new file mode 100644 index 0000000000..0c9041011c --- /dev/null +++ b/research/connector-gray-growth/README.md @@ -0,0 +1,305 @@ +# Unsigned connectors attain their call floor on Θ(c log c) sources + +In the unchanged unsigned dirty-connector interface of +[PR4231](https://github.com/CrocSwap/integer-mult-bounds/pull/4231), let N(c) +be the largest source count attaining the complete-call floor in characteristic +c ≥ 2. This package proves the explicit lower bound + +```text +b(c) = 1 + floor(log₂ c), +N(c) ≥ b(c) floor(c/2) + 2(c mod 2). +``` + +Together with the counting upper bound of +[PR4248](https://github.com/CrocSwap/integer-mult-bounds/pull/4248), this gives +**N(c) = Θ(c log c)**. In particular N(c)/c is unbounded. The new ingredient +is a constructive depth-two block for every k ≥ 1 and c ≥ max(2, 2^(k−1)), +obtained from a binary reflected Gray path. The proof below covers all these +parameters; finite replay supports its implementation. + +This answers [PR6035](https://github.com/CrocSwap/integer-mult-bounds/pull/6035) +open question 3 and the general-family handoff in +[PR6061](https://github.com/CrocSwap/integer-mult-bounds/pull/6061) open question 2. +It is a scoped connector theorem, with no new κ or selected-frontier change. + +## Exact interface and floor + +Let R be any nonzero unital ring of characteristic c ≥ 2. There are n immutable +source rows x_j, one arbitrary borrowed dirty row z, and arbitrary dirty output +rows y_m for every nonempty binary mask m on the sources. Compatible R-linear +maps B_j and A_m are arbitrary. The permitted complete calls are only + +```text +B_j: z += B_j x_j +A_m: y_m += A_m z. +``` + +Each call restores its private scratch and heads, preserves all other rows, +and acts independently of its old target. Coefficients remain immutable and +outputs are unobserved until completion. The required action is +`y_m += sum_(j in m) A_m B_j x_j`, with x_j and z unchanged. No signed calls, +scalings, extra connectors, direct products, free copies or source updates are +introduced. In particular the downward flips used to DESIGN the walk below +are not downward or inverse executable calls. + +Identity specialization, as in PR4231, forces each B_j and A_m to appear a +positive multiple of c times. Thus every universal word costs at least +`c(n + 2^n − 1)` complete calls. A floor word calls every operator exactly c +times. Project such a word onto its cn source calls and let q_t be their integer +prefix-count vector, including q_0 = 0. Calling A_m at c boundaries is correct +exactly when the sum of their q_t vectors is m modulo c. Repeated boundaries +are allowed; boundary zero supplies padding. This criterion uses additivity, +not invertibility of the maps, commutativity between A and B, or primality of c. + +A depth-d block uses each of its sources c times and represents every binary +mask as a sum of at most d source prefixes modulo c. Concatenating disjoint +blocks adds their depths because each completed block has prefix zero modulo c. +These are PR4248's prefix and concatenation lemmas; their proofs also follow +immediately from the displayed criterion. + +## A covering-walk construction + +**Lemma.** Suppose g_0,...,g_L is a finite walk in {0,1}^k, starts at zero, +visits every mask, and changes exactly one coordinate at each step. Repeated +vertices are allowed. Let f_j be the total flips of coordinate j. If c ≥ 2 and +f_j ≤ c for every j, there is an explicit depth-two block on these k sources. + +**Proof.** Let A be the subsequence of upward-flip labels, and B the subsequence +of downward-flip labels, both in their original order. For time t, let U_j(t) +and D_j(t) count upward and downward flips of coordinate j so far. Then +`U(t) − D(t) = g_t`. Write u(t) = sum_j U_j(t) and d(t) = sum_j D_j(t). +Form the unsigned source word + +```text +W = A · (0^(c−f_0) 1^(c−f_1) ... (k−1)^(c−f_(k−1))) · reverse(B). +``` + +Every exponent is nonnegative and every source occurs exactly c times. Let M +be the middle word. Two actual source boundaries are + +```text +a(t) = u(t), s(t) = kc − d(t). +``` + +They obey `0 ≤ a(t) ≤ |A| ≤ |A|+|M| ≤ s(t) ≤ kc`. The prefix at a(t) has +count vector U(t). At s(t), the unexecuted suffix consists of the reversal of +the first d(t) downward labels in B, so its count vector is D(t). Consequently + +```text +q_a(t) = U(t), q_s(t) = c·1 − D(t), +q_a(t) + q_s(t) = c·1 + g_t ≡ g_t (mod c). +``` + +This proves the claim for every visited mask. Use its first visit if it occurs +repeatedly. The zero mask can instead use the empty list of reads. Both +boundaries are chronological, even if they coincide. All executable events +are positive source calls. ∎ + +**Gray specialization.** For integers 0 ≤ i < 2^k set `g_i = i xor (i >> 1)`. +This lists every mask once: the map on k-bit vectors is triangular with unit +diagonal, hence invertible. Transition i−1 to i flips coordinate v₂(i), so +coordinate j flips exactly `2^(k−1−j)` times. The largest flip count is +`2^(k−1)`. The lemma therefore gives a depth-two block whenever +`c ≥ max(2, 2^(k−1))`. This is the classical reflected Gray path; Gray codes +themselves are not claimed new. + +For example, at k=3 and c=4 the Gray labels are `0,1,0,2,0,1,0`, giving +`A=0,1,2,0`, `B=0,1,0` and +`W=0,1,2,0,1,1,2,2,2,0,1,0`. Its twelve events contain each source four times, +and the lemma gives all seven nonzero masks using two prefixes each. + +## Growth theorem and complete words + +Set b = b(c). Concatenate floor(c/2) disjoint b-source Gray blocks. For odd c, +append PR4248's depth-one two-source block +`a b a^(c−1) b^(c−1)`: prefixes at boundaries 1, 2 and c+1 represent a, a+b +and b respectively. The total depth is at most c. For each nonzero global mask, +select the reads for its nonzero block masks, then pad to exactly c reads at +boundary zero. Sort reads chronologically and interleave the corresponding A_m +calls with the source word. Different output calls preserve z and can share a +boundary. The resulting word has exactly + +```text +n = b floor(c/2) + 2(c mod 2) sources, +cn source calls and c(2^n − 1) output calls. +``` + +The connector returns to z_0 since each B_j appears c times. Each output gains +`c A_m z_0 + sum_j m_j A_m B_j x_j`, with the first term zero. Arbitrary initial +y_m is preserved additively. This proves the floor bound for arbitrary compatible +maps over R, including composite characteristic and singular noncommuting maps. +The argument is constructive, but constructing all 2^n−1 output schedules is +exponential in n. Large examples below are evaluations of a proved formula, +not full-word simulations. + +Deleting source events and retaining only masks on the surviving sources +preserves the prefix identities and exactly c calls per remaining operator. +Thus attainable source counts form an initial segment, as in PR4248. + +For completeness, the inherited counting argument gives an explicit finite +upper bound. A floor word has at most cn distinct prefix vectors modulo c +(the initial and final boundaries coincide). There are at most +`binom(cn+c−1,c)` multisets of c such vectors, so floor attainment requires + +```text +2^n − 1 ≤ binom(cn+c−1,c). +``` + +Put m=ceil(log₂ c) and n₀=4c(m+1). The elementary inequality +`c! ≥ (c/3)^c` follows by induction from `(1+1/c)^c < 3` (bound its binomial +expansion by `sum_(j≥0) 1/j! < 3`). Hence + +```text +binom(cn₀+c−1,c) < [3(n₀+1)]^c, +3(n₀+1) = 12c(m+1)+3 ≤ 16c(m+1) + ≤ 16·2^m·2^m = 2^(2m+4) ≤ 2^(4m+3) = 2^(n₀/c−1). +``` + +Here m≥1 and m+1≤2^m. Therefore the count is less than +`2^(n₀−c) < 2^n₀−1`, excluding n₀; deletion excludes all larger n too. +Consequently + +```text +b(c) floor(c/2) + 2(c mod 2) ≤ N(c) < 4c(ceil(log₂ c)+1). +``` + +This proves Θ(c log c) and `liminf N(c)/(c log₂ c) ≥ 1/2`, without asserting +an optimal leading constant. + +The finite templates in PR6035 and PR6061 remain stronger at small c. In +particular PR6061 reaches six, seven and eight sources at c≥8, 12 and 27, +whereas the corresponding reflected-Gray thresholds are 32, 64 and 128. +Retain the maximum of established bounds when comparing pointwise values: + +| c | PR6061 eight-source lower bound | This construction | +|---:|---:|---:| +| 256 | 1,024 | 1,152 | +| 257 | 1,026 | 1,154 | +| 512 | 2,048 | 2,560 | +| 1,024 | 4,096 | 5,632 | + +## Cost and outstanding supplier obligations + +With positive fixed complete-call prices p_Bj and p_Am, the map-call bill is +exactly `c(sum_j p_Bj + sum_m p_Am)`, attaining PR4231's lower bound in that +pricing model. A conditional full caller bill remains + +```text +I + sum_F P_F + D_W + c(sum_j p_Bj(L) + sum_m p_Am(L)). +``` + +I pays input admission and layout; P_F pays reusable coefficient preparation; +D_W pays schedule construction/storage, instruction reads and dispatch. +Every p_F must include source/coefficient access, arithmetic, target update, +private scratch restoration, head returns and frames. These costs are not set +to zero. The required n source rows, 2^n−1 output rows and one dirty connector +also need a concrete admitted layout. No physical prices, native consumer, +transfer schedule, supplier recurrence or favorable complete multiplication +invoice are supplied. The local algebra and call counts are proved; those +integration obligations remain open. The selected κ stays 0.003125804. + +## Task, provenance and overlap + +Base: `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. +The original `connector-alphabet-change` card is retained in [TASK.json](TASK.json). +Scope is **changed**: the alphabet stays fixed. This follows the released +all-size-family handoff rather than another fixed-k search, and resolves the +asymptotic capacity gap between linear constructions and the counting bound. +It is a local interface side result, not passage of the family-level supplier +budget gate. The card's orientation control passed unchanged: +`PASS_UNIVERSAL_CONNECTOR_BOUNDARY pairings=945 max_coverage=31 queries=74 leaves=182`. +The selected baseline's binding check passed; its full cold replay was not run +because this package changes no selected construction or shared code. + +Canonical coordination: +[claim and result](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19233477). +Live handoffs, recent PRs and all-state Gray/connector and N(c)/log searches +were checked. The offline helper searched only 11 of 8,348 HEAD notes, with no +usable remote cache; that incomplete coverage is not evidence of novelty. +The live comparison found: + +- PR4231 and PR4248: exact interface, floor, prefix/deletion/concatenation and + counting lemmas; pinned canonical READMEs in [SOURCES.json](SOURCES.json). +- PR6035, head `119de1d7fca5124fa8d01ea49d258560aca618e6`: five-source lifted + template and the unbounded-ratio question; canonical README pinned. +- PR6061, head `babc5e99421403284fa530e9f135b618f31805bb`: stronger finite-size + thresholds and the explicit all-k handoff; motivation/comparison only. +- [PR6057](https://github.com/CrocSwap/integer-mult-bounds/pull/6057), head + `f92bd41f60564175bd68f944e9d6450da8965734`: parallel six-source construction; + motivation/comparison only. +- [PR5372](https://github.com/CrocSwap/integer-mult-bounds/pull/5372) uses a + clean helper row and Gray ordering; [PR1185](https://github.com/CrocSwap/integer-mult-bounds/pull/1185) + treats characteristic-two one-root connector optima and general Gray upper + bounds, with source multiplicities not constrained to c each. Their contracts + and results differ from this characteristic-dependent growth theorem. + +No pending-PR bytes or predecessor executable code are required. The direct +verifier checks the exact SHA256 of the three declared canonical README inputs; +the registered metadata check additionally validates historical Git provenance. + +## Reproduction and evidence + +From the repository root with Python 3.12 (standard library only): + +```sh +python3.12 -I -W error -B research/connector-gray-growth/verify.py +python3.12 -I -O -W error -B research/connector-gray-growth/verify.py +python3.12 -B scripts/research_package.py --package research/connector-gray-growth +python3.12 -B scripts/check_research_commit.py --package research/connector-gray-growth --check-source-history --check-modes +``` + +`construct.py` provides the covering-walk and reflected-Gray constructors, +block composition and literal complete-call iterator. `independent.py` uses a +separate recursive Gray construction and literal 2×2 matrix execution over Z/c. +`verify.py` binds sources and audits the production implementation, including +all target masks in the small composed examples. All local modules are loaded +from source bytes; verification writes no files and needs no Git or network. +Finite replay does not prove the all-parameter theorem; that proof is above. + +On CPython 3.12.14 / macOS arm64, normal and optimized direct runs agree +(about 0.9 seconds each). The production audit covers 36 blocks with k=1..12 +at c=max(2,2^(k−1)), that threshold plus 1, and plus 7: 24,534 nonzero masks +and 135,798 source events. It also checks 14 repeated/backtracking covering +walks, five complete compositions for c=2..6 (847 outputs, 4,778 literal calls), +and the first counting failure for every c=2..128 (92,001 comparisons). +The separate implementation covers 27 blocks and five compositions with +52,682 literal calls. Its recursion gives a second Gray-path implementation; +its grouped-boundary interpreter differs from execution of the production +call iterator. + +All 27 combined controls are rejected: they include malformed/under-capacity +walks, incorrect prefix witnesses, an unreversed downward suffix, source-count +corruption, dropped source/output calls, padding moved to a nonzero prefix, +and an over-depth composition. Guards and semantic controls are distinguished +in the verifier; every check stays active under `-O`. The counting transcript +SHA256 is `35d273c15d655535a3016e226a4c8295dd2db44cca3ae5e47acfbfc00e9e3e76`. +These counts describe bounded tests, not exhaustive coverage of all c or maps. +Independent Codex proof/code checks are AI-assisted reviews, not independent +human or proof-kernel verification. No native multiplication replay is claimed. + +## Open next questions + +Structured versions are in [TASK.json](TASK.json). + +1. What is the sharp leading constant of N(c)/(c log₂ c)? This construction + gives at least 1/2. First sharpen the counting asymptotic and look for + depth-two blocks near its `k ≈ 2 log₂ c` capacity. The present Gray split + only certifies `k ≈ log₂ c`; no matching construction or upper constant + is proved here. +2. Can a concrete characteristic-c consumer use these larger batches at a + favorable complete invoice? First specify its immutable-source interface + and price I, P_F, D_W and every complete primitive, including output layout. + No such consumer or price schedule is currently supplied; source capacity + alone cannot settle this question. + +## Credit + +Prepared by **apoursh** with substantial OpenAI Codex assistance, including +separate construction, literal-execution and mathematical-audit agents. +Nick Petalas supplies PR4231/4248/6035 and their retained Ross Richardson +PR934/943 and Riquelme Soares lineage. JosieElliston's PR6061 supplies the +finite-block progress and explicit general-family handoff; zxv's PR6057 is +parallel finite-block work. Classical reflected Gray codes are established +combinatorics. This package adds their upward/reversed-downward realization +in the unchanged unsigned connector contract and the resulting growth theorem. +Predecessor attribution and frozen bytes are preserved. Apache-2.0. diff --git a/research/connector-gray-growth/SOURCES.json b/research/connector-gray-growth/SOURCES.json new file mode 100644 index 0000000000..dfd36ec9e3 --- /dev/null +++ b/research/connector-gray-growth/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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" + }, + { + "path": "research/connector-five-halves-growth/README.md", + "usage": "input", + "git_blob": "ede2725b4b49c8fe587f077d731432437a3fdb3d", + "sha256": "623f08f27f74ed050d19d5fb518c842512ac6eb54c07701aa94d018eda01cb6f" + }, + { + "path": "research/unsigned-connector-characteristic/README.md", + "usage": "input", + "git_blob": "f5756613cc92a15bb5a1d2865dfb0ac469eff92f", + "sha256": "260ae8ca19cfd8add386666e823725065eb137bcaedf7577785d6eda4ee0200b" + } + ] +} diff --git a/research/connector-gray-growth/TASK.json b/research/connector-gray-growth/TASK.json new file mode 100644 index 0000000000..21478f695b --- /dev/null +++ b/research/connector-gray-growth/TASK.json @@ -0,0 +1,69 @@ +{ + "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": "Prove an all-size depth-two family in the unchanged unsigned immutable-source/one-dirty-connector interface: k sources at c >= max(2,2^(k-1)); derive N(c) >= (1+floor(log2 c))*floor(c/2)+2*(c mod 2) and N(c)=Theta(c log c).", + "scope_change_reason": "Follow the explicitly released general-family question in PR6061 OQ2 and PR6035 OQ3. The card asks for an alphabet extension; this retains that alphabet and resolves its asymptotic floor-attainment capacity, rather than extending a fixed-size census. No predecessor exclusion or disputed pruning is used.", + "bottleneck_link": "Scoped interface side result: resolves the gap between linear constructive floor capacity and the O(c log c) counting upper bound. No native consumer, complete price schedule or supplier recurrence is supplied, so this is not a selected-bound improvement or passage of the family-level budget gate.", + "budget_minutes": 60, + "stop_rule": "Stop after the all-parameter construction, independent proof/execution audit and bounded replay; do not continue to larger fixed-k searches or claim a supplier saving without a concrete complete invoice.", + "outcome": "completed", + "evidence": "README proof; normal/optimized source-bound production verification (36 blocks, 14 repeated walks, 5 compositions, 127 counting thresholds, 18 controls); independent implementation (27 blocks, 5 compositions, 9 controls).", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance, including separate construction, literal-execution and mathematical-audit agents. No independent human or proof-kernel verification claimed.", + "open_questions": [ + { + "question": "What is the sharp leading constant of N(c)/(c log2 c)?", + "why_it_matters": "The new construction proves a liminf of at least 1/2 and settles the order, leaving a gap to the counting bound.", + "first_step": "Sharpen the counting asymptotic and seek depth-two blocks near k=2 log2 c, comparing their complete unsigned word with the prefix criterion.", + "blocked_by": "The reflected-Gray split certifies only k about log2 c; no matching leading constant is proved." + }, + { + "question": "Can a concrete characteristic-c consumer use these larger batches at a favorable complete invoice?", + "why_it_matters": "Connector source capacity alone does not imply a multiplication bound improvement.", + "first_step": "Specify an immutable-source, unobserved-output consumer and price admission, layout, coefficient preparation, schedule/dispatch and every complete primitive.", + "blocked_by": "No native consumer, physical primitive prices, transfer schedule or supplier recurrence is supplied." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19233477" +} diff --git a/research/connector-gray-growth/VERIFY.json b/research/connector-gray-growth/VERIFY.json new file mode 100644 index 0000000000..29c11f6501 --- /dev/null +++ b/research/connector-gray-growth/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-depth-blocks/README.md", + "research/connector-five-halves-growth/README.md", + "research/unsigned-connector-characteristic/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate three canonical source READMEs; explicit prefix identities, recursive independent construction, production literal calls on all source/dirty input columns over Z/c, block composition, counting thresholds and semantic failure controls; no selected-frontier replay." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate three canonical source READMEs; explicit prefix identities, recursive independent construction, production literal calls on all source/dirty input columns over Z/c, block composition, counting thresholds and semantic failure controls; no selected-frontier replay." + } + ] +} diff --git a/research/connector-gray-growth/construct.py b/research/connector-gray-growth/construct.py new file mode 100644 index 0000000000..808ffc71e2 --- /dev/null +++ b/research/connector-gray-growth/construct.py @@ -0,0 +1,131 @@ +"""Explicit unsigned connector walks from binary covering walks. + +The interface, prefix criterion, block composition and depth-one pair are +Nick Petalas's PR4248/6035, following Ross Richardson's connector lineage. +The upward/downward Gray-walk construction is new in this package. +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +""" + +from collections import Counter + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def covering_block(k, c, states): + """Return a source word and explicit two-prefix witnesses for every mask. + + ``states`` is a zero-start covering walk in the k-dimensional binary + cube. Each step flips one bit; repeats are allowed. The characteristic + must be at least the largest total flip count of a coordinate. + Readout keys include zero, whose witness is the empty tuple. + """ + require(type(k) is int and k >= 1, "positive integer source count required") + require(type(c) is int and c >= 2, "characteristic must be an integer >= 2") + states = iter(states) + old = next(states, None) + require(type(old) is int and old == 0, "covering walk must start at zero") + up, down = [], [] + first = {0: (0, 0)} + for new in states: + require(type(new) is int and 0 <= new < 1 << k, "mask outside cube") + difference = old ^ new + require(difference != 0 and difference & (difference - 1) == 0, + "each covering-walk step must flip exactly one bit") + bit = difference.bit_length() - 1 + (up if new & difference else down).append(bit) + first.setdefault(new, (len(up), len(down))) + old = new + require(len(first) == 1 << k, "covering walk does not visit every mask") + flips = Counter(up + down) + require(all(flips[j] <= c for j in range(k)), + "characteristic smaller than a coordinate's flip count") + middle = [j for j in range(k) for _ in range(c - flips[j])] + word = up + middle + down[::-1] + # The reversed downward suffix has exactly d original downward events + # still to run at boundary kc-d. Its count vector is c*1-D(t). + readouts = {mask: (u, k * c - d) for mask, (u, d) in first.items()} + readouts[0] = () + return word, readouts + + +def gray_block(k, c): + """A depth-at-most-two block for c >= 2**(k-1), c >= 2. + + Reflected Gray transition i flips bit v_2(i), so bit j changes exactly + 2**(k-1-j) times. The returned witnesses are chronological boundaries. + """ + require(type(k) is int and k >= 1, "positive integer source count required") + require(type(c) is int and c >= max(2, 1 << (k - 1)), + "Gray block requires c >= max(2, 2**(k-1))") + return covering_block(k, c, (i ^ (i >> 1) for i in range(1 << k))) + + +def pair_block(c): + """PR4248's two-source depth-one word and prefix witnesses.""" + require(type(c) is int and c >= 2, "characteristic must be an integer >= 2") + return [0, 1] + [0] * (c - 1) + [1] * (c - 1), { + 0: (), 1: (1,), 2: (c + 1,), 3: (2,)} + + +def compose_blocks(c, blocks): + """Concatenate certified disjoint blocks and pad every output to c reads. + + Each block is ``(width, word, readouts)`` with local labels 0..width-1, + all mask keys including zero, and boundary tuples. The caller must check + each block's prefix identity; this routine validates shape, counts and + the sufficient sum-of-depths budget. Its output has nonzero mask keys. + """ + require(type(c) is int and c >= 2, "characteristic must be an integer >= 2") + blocks = list(blocks) + require(bool(blocks), "at least one block required") + word, shifted, width, depth = [], [], 0, 0 + for k, path, hits in blocks: + require(type(k) is int and k >= 1, "positive block width required") + require(all(type(j) is int and 0 <= j < k for j in path), + "source label outside block") + require(Counter(path) == {j: c for j in range(k)}, + "each block source must occur exactly c times") + require(set(hits) == set(range(1 << k)), "block mask coverage is incomplete") + require(hits[0] == (), "zero block mask must use no readouts") + for times in hits.values(): + require(all(type(t) is int and 0 <= t <= len(path) for t in times), + "readout boundary outside source word") + require(tuple(sorted(times)) == tuple(times), "readouts must be chronological") + depth += max(map(len, hits.values())) + shifted.append((k, width, len(word), hits)) + word.extend(width + j for j in path) + width += k + require(depth <= c, "sum of block depths exceeds the c-readout budget") + readouts = {} + for mask in range(1, 1 << width): + times = [] + for k, shift, offset, hits in shifted: + local_mask = (mask >> shift) & ((1 << k) - 1) + times.extend(offset + t for t in hits[local_mask]) + times.extend([0] * (c - len(times))) + readouts[mask] = tuple(sorted(times)) + return word, readouts + + +def literal_calls(word, readouts): + """Yield ('B', source) and ('A', mask) calls in chronological order.""" + at = {} + for mask, times in readouts.items(): + for time in times: + require(type(time) is int and 0 <= time <= len(word), + "readout boundary outside source word") + at.setdefault(time, []).append(mask) + for time in range(len(word) + 1): + for mask in sorted(at.get(time, [])): + yield "A", mask + if time < len(word): + yield "B", word[time] + + +def source_bound(c): + """The theorem's attainable global source count, without building its word.""" + require(type(c) is int and c >= 2, "characteristic must be an integer >= 2") + return c.bit_length() * (c // 2) + 2 * (c % 2) diff --git a/research/connector-gray-growth/independent.py b/research/connector-gray-growth/independent.py new file mode 100644 index 0000000000..6e83f995da --- /dev/null +++ b/research/connector-gray-growth/independent.py @@ -0,0 +1,185 @@ +"""Independent audit of the upward/reversed-downward connector construction. + +Stdlib; a separate reflected recursion and literal 2x2 matrix execution over +Z/c, including singular noncommuting maps and arbitrary dirty input columns. +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +The interface and depth-one pair are credited to Nick Petalas (PR4248/6035), +following Ross Richardson and the retained unsigned connector lineage. +No claim of an independent human or formal-kernel review. +""" +from collections import Counter, defaultdict + + +def require(value, message): + if not value: + raise ValueError(message) + + +def gray(k): + if k == 0: + return [0] + previous = gray(k - 1) + return previous + [x | (1 << (k - 1)) for x in reversed(previous)] + + +def block(path, k, c): + require(path[0] == 0, 'start') + up, down = [], [] + locations = {0: (0, 0)} + for old, new in zip(path, path[1:]): + delta = old ^ new + require(delta > 0 and not delta & (delta - 1), 'one bit') + j = delta.bit_length() - 1 + require(j < k, 'coordinate') + (up if new & delta else down).append(j) + locations.setdefault(new, (len(up), len(down))) + require(set(locations) == set(range(1 << k)), 'cover') + counts = Counter(up + down) + require(max(counts.values(), default=0) <= c, 'capacity') + middle = [j for j in range(k) for _ in range(c - counts[j])] + word = up + middle + list(reversed(down)) + pairs = {m: [a, len(word) - d] for m, (a, d) in locations.items() if m} + return word, pairs + + +def check_prefix(word, reads, k, c, *, depth=None): + require(Counter(word) == Counter({j: c for j in range(k)}), 'source counts') + pref = [[0] * k] + for j in word: + q = pref[-1].copy() + q[j] += 1 + pref.append(q) + require(set(reads) == set(range(1, 1 << k)), 'output set') + for mask, times in reads.items(): + require(depth is None or len(times) <= depth, 'depth') + require(all(0 <= t <= len(word) for t in times), 'boundary') + require(all(sum(pref[t][j] for t in times) % c == (mask >> j & 1) + for j in range(k)), 'wrong mask') + + +def compose(parts, c): + word, total_k, all_parts = [], 0, [] + for subword, subreads, k in parts: + all_parts.append((len(word), total_k, subreads, k)) + word.extend(j + total_k for j in subword) + total_k += k + reads = {} + for mask in range(1, 1 << total_k): + times = [] + for offset, shift, subreads, k in all_parts: + submask = mask >> shift & ((1 << k) - 1) + if submask: + times.extend(t + offset for t in subreads[submask]) + require(len(times) <= c, 'read budget') + reads[mask] = sorted([0] * (c - len(times)) + times) + return word, reads, total_k + + +ZERO = (0, 0, 0, 0) +I = (1, 0, 0, 1) + + +def add(a, b, c): + return tuple((x + y) % c for x, y in zip(a, b)) + + +def mul(a, b, c): + return ((a[0]*b[0]+a[1]*b[2]) % c, (a[0]*b[1]+a[1]*b[3]) % c, + (a[2]*b[0]+a[3]*b[2]) % c, (a[2]*b[1]+a[3]*b[3]) % c) + + +def literal(word, reads, k, c): + """Apply every call to exact block matrices for all arbitrary input columns.""" + check_prefix(word, reads, k, c) + require(all(len(ts) == c for ts in reads.values()), 'complete A count') + maps = [(0, 1, 0, 0), (0, 0, 1, 0), (1, 1, 0, 1), (1, 0, 1, 1)] + B = [maps[j % 4] for j in range(k)] + A = {m: maps[(m + 1) % 4] for m in reads} + # Input block k is the arbitrary initial dirty connector, the others sources. + z = [ZERO] * k + [I] + y = {m: [ZERO] * (k + 1) for m in reads} + at = defaultdict(list) + for m, ts in reads.items(): + for t in ts: + at[t].append(m) + for t in range(len(word) + 1): + for m in at[t]: + y[m] = [add(old, mul(A[m], q, c), c) for old, q in zip(y[m], z)] + if t < len(word): + j = word[t] + z[j] = add(z[j], B[j], c) + require(z == [ZERO] * k + [I], 'dirty restoration') + for m in reads: + expected = [mul(A[m], B[j], c) if m >> j & 1 else ZERO for j in range(k)] + [ZERO] + require(y[m] == expected, 'literal operator') + require(mul(maps[0], maps[1], c) != mul(maps[1], maps[0], c), 'noncommuting control') + return len(word) + sum(map(len, reads.values())) + + +def rejected(fn): + try: + fn() + except ValueError: + return 1 + raise ValueError('mutation accepted') + + +def run(): + blocks = calls = 0 + # Independent reflected recursion, both simple paths and repeated-label + # paths with an inserted closed excursion before the complete Gray path. + for k in range(1, 8): + path = gray(k) + flip = Counter((a ^ b).bit_length()-1 for a,b in zip(path,path[1:])) + require([flip[j] for j in range(k)] == [1 << (k - 1 - j) for j in range(k)], 'flip law') + for c in [max(flip.values()), max(flip.values()) + 1, max(flip.values()) + 3]: + if c < 2: + continue + w, r = block(path, k, c) + check_prefix(w, r, k, c, depth=2) + full = {m: [0] * (c-2) + ts for m, ts in r.items()} + calls += literal(w, full, k, c) + require(len(w) + c * len(r) == c * (k + (1 << k)-1), 'floor') + blocks += 1 + repeated = [0, 1, 0] + path[1:] + counts = Counter((a ^ b).bit_length()-1 for a,b in zip(repeated,repeated[1:])) + c = max(counts.values()) + w,r = block(repeated,k,c) + calls += literal(w,{m:[0]*(c-2)+ts for m,ts in r.items()},k,c) + blocks += 1 + composed = 0 + for c in range(2,7): + k = min(3,c.bit_length()) + w,r = block(gray(k),k,c) + parts = [(w,r,k)] * (c//2) + if c % 2: + # Independent depth-one two-source fixture from predecessor. + tail = [0,1]+[0]*(c-1)+[1]*(c-1) + parts.append((tail,{1:[1],3:[2],2:[c+1]},2)) + joined, reads, n = compose(parts,c) + require(n == k*(c//2)+2*(c%2), 'source count formula') + calls += literal(joined,reads,n,c) + composed += 1 + w,r = block(gray(3),3,4) + controls = 0 + controls += rejected(lambda: block(gray(3),3,3)) + controls += rejected(lambda: block([1,0],1,2)) + controls += rejected(lambda: block([0,3],2,2)) + controls += rejected(lambda: block([0,1],2,2)) + controls += rejected(lambda: check_prefix(w[:-1],r,3,4)) + altered={m:ts.copy() for m,ts in r.items()} + altered[1]=[0,0] + controls += rejected(lambda: check_prefix(w,altered,3,4)) + bad_middle=w.copy();bad_middle[0]=1 + controls += rejected(lambda: check_prefix(bad_middle,r,3,4)) + # Reverse-down order is essential: its first nontrivial counterexample. + longer,lr=block(gray(4),4,8) + up=[(a^b).bit_length()-1 for a,b in zip(gray(4),gray(4)[1:]) if b&(a^b)] + down=[(a^b).bit_length()-1 for a,b in zip(gray(4),gray(4)[1:]) if not b&(a^b)] + bad=longer[:-len(down)]+down + controls += rejected(lambda: check_prefix(bad,lr,4,8)) + controls += rejected(lambda: compose([(w,r,3)]*3,4)) + print(f'PASS_GRAY_CONNECTOR_INDEPENDENT blocks={blocks} composed={composed} literal_calls={calls} controls={controls}') + +if __name__=='__main__': + run() diff --git a/research/connector-gray-growth/verify.py b/research/connector-gray-growth/verify.py new file mode 100644 index 0000000000..a34ca252a3 --- /dev/null +++ b/research/connector-gray-growth/verify.py @@ -0,0 +1,229 @@ +"""Source-bound checks of the explicit Gray connector construction. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Predecessor interface, prefix criterion and counting: Nick Petalas's +PR4231/4248/6035, following Ross Richardson and the retained lineage. +All finite checks support the written proof; no supplier or new kappa. +""" +from collections import Counter +from hashlib import sha256 +import json +from math import comb +from pathlib import Path +from types import ModuleType + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load(name): + path = PACKAGE / (name + '.py') + module = ModuleType(name) + module.__file__ = str(path) + exec(compile(path.read_bytes(), str(path), 'exec'), module.__dict__) + return module + + +def source_checks(): + manifest = json.loads((PACKAGE / 'SOURCES.json').read_bytes()) + inputs = [row for row in manifest['files'] if row['usage'] == 'input'] + wanted = { + 'research/connector-depth-blocks/README.md', + 'research/connector-five-halves-growth/README.md', + 'research/unsigned-connector-characteristic/README.md', + } + require(len(inputs) == 3 and {row['path'] for row in inputs} == wanted, + 'source input coverage changed') + for row in inputs: + require(sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], + 'source bytes changed: ' + row['path']) + return len(inputs) + + +def block_checks(prod, independent): + cases = masks = events = repeated = 0 + for k in range(1, 13): + threshold = max(2, 1 << (k - 1)) + for c in (threshold, threshold + 1, threshold + 7): + word, hits = prod.gray_block(k, c) + reference_word, reference_hits = independent.block(independent.gray(k), k, c) + require(word == reference_word, 'independent source word differs') + require(hits[0] == (), 'zero mask should consume no depth') + require({m: list(ts) for m, ts in hits.items() if m} == reference_hits, + 'independent readout boundaries differ') + independent.check_prefix(word, reference_hits, k, c, depth=2) + require(all(len(ts) == 2 and ts[0] <= ts[1] for m, ts in hits.items() if m), + 'two chronological reads missing') + events += len(word) + masks += len(reference_hits) + cases += 1 + for k in range(1, 8): + reflected = independent.gray(k) + # First a backtrack before coverage, then a closed covering walk. + walks = ([0, 1, 0] + reflected[1:], reflected + reflected[-2::-1]) + for states in walks: + counts = Counter((a ^ b).bit_length() - 1 for a, b in zip(states, states[1:])) + c = max(2, max(counts.values())) + word, hits = prod.covering_block(k, c, states) + reference_word, reference_hits = independent.block(states, k, c) + require(word == reference_word, 'repeated walk source mismatch') + require({m: list(ts) for m, ts in hits.items() if m} == reference_hits, + 'repeated walk readout mismatch') + independent.check_prefix(word, reference_hits, k, c, depth=2) + repeated += 1 + return cases, masks, events, repeated + + +def execute(calls, k, c, independent): + """Execute the actual yielded call sequence on all source/dirty columns. + + Every entry is a 2x2 matrix over Z/c; no A/B commutation is imposed. + Each old output has its unchanged identity contribution because outputs + are only destinations. All source and dirty columns are computed. + """ + zero, ident = independent.ZERO, independent.I + mul, add = independent.mul, independent.add + maps = [(0, 1, 0, 0), (0, 0, 1, 0), (1, 1, 0, 1), (1, 0, 1, 1)] + require(mul(maps[0], maps[1], c) != mul(maps[1], maps[0], c), 'commuting fixture') + B = [maps[j % len(maps)] for j in range(k)] + masks = range(1, 1 << k) + A = {m: maps[(m + 1) % len(maps)] for m in masks} + z = [zero] * k + [ident] + outputs = {m: [zero] * (k + 1) for m in masks} + count = Counter() + total = 0 + for kind, index in calls: + count[kind, index] += 1 + total += 1 + if kind == 'B': + require(type(index) is int and 0 <= index < k, 'invalid source event') + z[index] = add(z[index], B[index], c) + elif kind == 'A': + require(index in outputs, 'invalid output event') + outputs[index] = [add(y, mul(A[index], a, c), c) + for y, a in zip(outputs[index], z)] + else: + raise ValueError('unknown call type') + require(z == [zero] * k + [ident], 'dirty connector not restored') + for mask in masks: + expected = [mul(A[mask], B[j], c) if mask >> j & 1 else zero for j in range(k)] + [zero] + require(outputs[mask] == expected, 'wrong full operator, including dirty dependence') + expected_counts = Counter({('B', j): c for j in range(k)}) + expected_counts.update({('A', mask): c for mask in masks}) + require(count == expected_counts, 'complete-call multiplicities changed') + require(total == c * (k + (1 << k) - 1), 'complete-call floor differs') + return total + + +def composition_checks(prod, independent): + words = outputs = calls = 0 + for c in range(2, 7): + k = c.bit_length() + word, hits = prod.gray_block(k, c) + parts = [(k, word, hits)] * (c // 2) + if c % 2: + pair_word, pair_hits = prod.pair_block(c) + independent.check_prefix(pair_word, {m: ts for m, ts in pair_hits.items() if m}, + 2, c, depth=1) + parts.append((2, pair_word, pair_hits)) + n = sum(width for width, _, _ in parts) + require(n == prod.source_bound(c), 'attained source formula differs') + joined, readouts = prod.compose_blocks(c, parts) + oracle_word, oracle_reads, oracle_n = independent.compose( + [(w, {m: list(ts) for m, ts in h.items() if m}, width) for width, w, h in parts], c) + require(oracle_n == n and oracle_word == joined, 'concatenation mismatch') + require({m: list(ts) for m, ts in readouts.items()} == oracle_reads, + 'concatenated readouts mismatch') + independent.check_prefix(joined, readouts, n, c, depth=c) + calls += execute(prod.literal_calls(joined, readouts), n, c, independent) + outputs += len(readouts) + words += 1 + return words, outputs, calls + + +def counting_checks(prod): + require({c: prod.source_bound(c) for c in (256, 257, 512, 1024)} == + {256: 1152, 257: 1154, 512: 2560, 1024: 5632}, 'large source bounds') + thresholds = [] + comparisons = 0 + for c in range(2, 129): + n = 1 + # This is a finite arithmetic corroboration of the inherited bound, + # not the proof that its first failure excludes all later n. + while True: + available = comb(c * n + c - 1, c) + required = (1 << n) - 1 + comparisons += 1 + if available < required: + break + n += 1 + require(n <= 4 * c * (2*c).bit_length(), 'counting scan exceeded explicit cap') + require(prod.source_bound(c) < n, 'construction contradicts counting bound') + thresholds.append([c, n]) + require(thresholds[:8] == [[2, 7], [3, 14], [4, 22], [5, 30], [6, 38], + [7, 47], [8, 56], [9, 65]], 'predecessor threshold control') + digest = sha256(json.dumps(thresholds, separators=(',', ':')).encode()).hexdigest() + return len(thresholds), comparisons, digest + + +def mutation_checks(prod, independent): + controls = 0 + reject = independent.rejected + for args in ((0, 2), (2, 1), (3, 3), (True, 2)): + controls += reject(lambda args=args: prod.gray_block(*args)) + for states in ([1, 0], [0, 3], [0, 1], [0, 1, 1, 0], [0, 4]): + controls += reject(lambda states=states: prod.covering_block(2, 4, states)) + word, hits = prod.gray_block(3, 4) + invalid = dict(hits) + invalid[1] = (0, 0) + controls += reject(lambda: independent.check_prefix(word, {m: ts for m, ts in invalid.items() if m}, + 3, 4, depth=2)) + controls += reject(lambda: prod.compose_blocks(4, [(3, word, hits)] * 3)) + controls += reject(lambda: prod.compose_blocks(4, [(3, word[:-1], hits)])) + controls += reject(lambda: list(prod.literal_calls(word, {1: (-1,)}))) + # Test physical failures against the actual yielded schedule. + full_word, readouts = prod.compose_blocks(4, [(3, word, hits)]) + calls = list(prod.literal_calls(full_word, readouts)) + first_a = next(i for i, x in enumerate(calls) if x[0] == 'A') + controls += reject(lambda: execute(calls[:first_a] + calls[first_a+1:], 3, 4, independent)) + first_b = next(i for i, x in enumerate(calls) if x[0] == 'B') + controls += reject(lambda: execute(calls[:first_b] + calls[first_b+1:], 3, 4, independent)) + bad_padding = {m: tuple(ts) for m, ts in readouts.items()} + # Keep all c reads, but move a zero-state padding read to a nonzero prefix. + times = list(bad_padding[1]); require(times[0] == 0, 'padding fixture') + times[0] = 1; bad_padding[1] = tuple(sorted(times)) + controls += reject(lambda: independent.check_prefix(full_word, bad_padding, 3, 4, depth=4)) + controls += reject(lambda: execute(prod.literal_calls(full_word, bad_padding), 3, 4, independent)) + # The reversed-down order is part of the construction, not optional. + word4, hits4 = prod.gray_block(4, 8) + states4 = independent.gray(4) + down = [(a ^ b).bit_length()-1 for a,b in zip(states4, states4[1:]) if not b & (a ^ b)] + wrong_reverse = word4[:-len(down)] + down + controls += reject(lambda: independent.check_prefix(wrong_reverse, + {m: ts for m, ts in hits4.items() if m}, 4, 8, depth=2)) + return controls + + +def main(): + sources = source_checks() + independent = load('independent') + prod = load('construct') + independent.run() + blocks, masks, events, repeated = block_checks(prod, independent) + compositions, outputs, literal = composition_checks(prod, independent) + characteristics, comparisons, digest = counting_checks(prod) + controls = mutation_checks(prod, independent) + print(f'PASS_CONNECTOR_GRAY_GROWTH sources={sources} blocks={blocks} masks={masks} ' + f'source_events={events} repeated_walks={repeated} compositions={compositions} ' + f'outputs={outputs} literal_calls={literal} counting_characteristics={characteristics} ' + f'counting_comparisons={comparisons} controls={controls} no_new_kappa') + print('COUNTING_THRESHOLDS_SHA256=' + digest) + + +if __name__ == '__main__': + main()