From 00798d2af754c4123a80666e513b8f7585d5b617 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 14:10:26 +0000 Subject: [PATCH] feat(research): prove sharp boundary-rank endpoint horizon --- research/boundary-rank-horizon/PROOF.md | 124 +++++++++++ research/boundary-rank-horizon/README.md | 147 +++++++++++++ research/boundary-rank-horizon/RESULT.json | 87 ++++++++ research/boundary-rank-horizon/SOURCES.json | 30 +++ research/boundary-rank-horizon/TASK.json | 110 ++++++++++ research/boundary-rank-horizon/VERIFY.json | 34 +++ research/boundary-rank-horizon/verify.py | 216 ++++++++++++++++++++ 7 files changed, 748 insertions(+) create mode 100644 research/boundary-rank-horizon/PROOF.md create mode 100644 research/boundary-rank-horizon/README.md create mode 100644 research/boundary-rank-horizon/RESULT.json create mode 100644 research/boundary-rank-horizon/SOURCES.json create mode 100644 research/boundary-rank-horizon/TASK.json create mode 100644 research/boundary-rank-horizon/VERIFY.json create mode 100644 research/boundary-rank-horizon/verify.py diff --git a/research/boundary-rank-horizon/PROOF.md b/research/boundary-rank-horizon/PROOF.md new file mode 100644 index 0000000000..ad673208a0 --- /dev/null +++ b/research/boundary-rank-horizon/PROOF.md @@ -0,0 +1,124 @@ +# Sharp positive-width horizon from the right-boundary kernel + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let K be any field, let Sigma be a finite alphabet, and fix finite matrices + +``` +F in K^(p x D), B in K^(D x q), T_s in K^(D x D) for s in Sigma. +``` + +The complete residual at word w=s_1...s_f is F T_w B, with the matrices +multiplied in the displayed order. Every input/output role is retained. +The empty word is outside the tested domain. The physical-column model of +zxv's PR5441 uses s=(output column,input column). + +Define V_k as the row span of all F T_w with 1<=|w|<=k. Put + +``` +r = dim V_1, b = rank B. +``` + +If r=0 or b=0, every positive-width residual is zero. Otherwise set + +``` +H = max(1, D-r-b+2). +``` + +Then the residual is zero at every positive width if and only if it is +zero for every word of lengths 1,...,H. Equivalently, any nonzero complete +residual has a literal nonzero entry at a positive width at most H. + +For every integer D>=1 and every 1<=r,b<=D, this bound is attained by a +one-symbol example with exactly those ranks. The examples use only zeros +and ones and work over every field. + +## Upper bound + +If r=0, every word starts with F T_s=0. If b=0, B=0. These cases give the +first assertion, including D=0 and an empty alphabet. + +Assume r,b>0. Let W be the left kernel of B, so dim W=D-b. The spaces V_k +satisfy + +``` +V_(k+1) = V_k + sum_s V_k T_s. +``` + +If consecutive spaces agree, that space is invariant under every T_s. +It then contains every later positive reachable row. + +Suppose the residual vanishes through width H. Thus V_H is contained in W. +If r+b>D, already dim V_1=r>D-b, a contradiction. In this case H=1 and +width one must have a nonzero entry. + +It remains to consider r+b<=D. Here H=D-r-b+2>=2. If every inclusion from +V_1 to V_H were strict, then + +``` +dim V_H >= r+(H-1) = D-b+1, +``` + +contradicting V_H contained in W. Some consecutive spaces therefore agree +before width H. Their invariance and containment in W prove that every +later residual also vanishes. The reverse implication is immediate. + +This proof stops dimension growth at the kernel of the actual right +boundary. PR5441's bound D-r+1 instead budgets growth in the entire +D-dimensional transfer space. The improvement is b-1 widths until the +mandatory minimum positive width one is reached. At b=1 the bounds agree. + +No minimum realization, genericity, commutativity, invertibility of the +transitions, numerical separation or characteristic assumption is used. + +## Sharpness for every rank triple + +First suppose r+b<=D+1, and put L=D-r-b+2>=1. Partition a basis into + +``` +r-1 dead basis vectors; +L cycle basis vectors c_0,...,c_(L-1); +b-1 unreachable accepting basis vectors. +``` + +The counts sum to D. The single transition T fixes every dead and +unreachable vector and acts on row vectors by the cyclic shift +c_j T=c_((j+1) mod L). Let the rows of F be the dead vectors followed by +c_(L-1). Let the columns of B be the transpose of c_(L-1), followed by +the transposes of the unreachable accepting vectors. + +Then rank B=b. The rows of F T are the r-1 dead vectors and c_0, so r is +the positive seed rank. At positive widths 1,...,L-1 no reachable row +pairs nontrivially with a column of B. At width L the cycle row returns +to c_(L-1), and its accepting entry is one. The first discrepancy is +exactly L=H. The empty-word entry is one too; including width zero would +change the statement and destroy this sharp positive-width example. + +If r+b>D+1, take T=I, let the rows of F be the first r coordinate vectors, +and let the columns of B be the last b coordinate vectors. The coordinate +sets overlap, giving a nonzero entry at width one. The ranks are r,b, +and H=1. This completes every admissible triple. + +For example D=8,r=2,b=3 gives first discrepancy five. It passes every +width below five, so replacing the final +2 by +1 is false. The earlier +seed-rank-only horizon is seven for this example. + +## Scope and credit + +The proof is a rank-nullity refinement of classical weighted-automata +reachability. It is not a claim of a new general equivalence algorithm or +general literature priority. Credit zxv's PR5441 for the fixed physical +table, positive-width, full-role and complete-return contract and its +earlier D-r+1 bound. Its proof credits Kiefer and coauthors, Tzeng, +Crosswhite and Bacon, and the repository's independent/inverse register +certificates PR5235 and PR5262. Those results are premises and context, +not scientific replay or audit targets here. + +This is an exact finite-representation statement. It does not certify a +width-dependent table, tolerance test, omitted return, actual source-table +extraction, native realization, physical cost, supplier or multiplication +theorem. The cutoff changes neither the transition dimension nor the +cost of testing all physical words below that cutoff. All five selected +framework assumptions remain. diff --git a/research/boundary-rank-horizon/README.md b/research/boundary-rank-horizon/README.md new file mode 100644 index 0000000000..60c42bc4be --- /dev/null +++ b/research/boundary-rank-horizon/README.md @@ -0,0 +1,147 @@ +# Sharp boundary-rank horizon for complete finite-memory endpoints + +This contribution was produced by Nick Petalas. Apache-2.0. + +A complete fixed transfer representation needs positive-width tests only through + +``` +H = max(1, D-r-b+2), +r = rank of the positive seed rows {F T_s}, b = rank B. +``` + +Here every endpoint is `F T_w B`, D is the transfer dimension, and r,b are +nonzero. If either rank is zero, every positive-width endpoint is zero. +The bound is sharp for every admissible triple D,r,b over every field. +For D=8,r=2,b=3, a one-symbol cyclic example first fails at width five; +the earlier seed-rank-only horizon is seven. + +Claim type: scoped written mathematical proof with exact finite corroboration. +No new kappa, selected-frontier change or complete multiplication theorem is +claimed. The new step observes that all passing reachable rows lie in the +actual right-boundary kernel of dimension D-b, rather than the whole transfer +space. [PROOF.md](PROOF.md) gives the quantified argument and sharp examples. + +## Interface and predecessor + +This is an independently posed refinement of the complete physical-column +interface in [zxv's PR5441](https://github.com/CrocSwap/integer-mult-bounds/pull/5441), +head `11fedb46fa199283f78282187c10aea432d8b0bb`. Its retained +[proof](../finite-memory-lifting/PROOF.md) supplies the earlier D-r+1 horizon, +fixed-table semantics, positive-width convention and complete dirty returns. +Those results are credited premises, not audit or replay targets. No predecessor +checker is imported or executed, and no existing package is changed. + +The alphabet may contain every physical input/output column pair. Every word +must be tested, rather than only repeated identical columns. Every original +and returned role must remain in the residual. A reference can be subtracted +by direct sum as in the predecessor; ranks belong to that complete residual. +The matrices and boundaries must stay fixed across widths. + +The exact horizon improves by b-1 widths until it reaches one. This is an +interface reduction, not a measured runtime speedup. It does not reduce table +extraction cost, transition dimension or the number of words at a given width. +No actual selected provider/consumer table is extracted here. Numerical +tolerance, physical realization, paid/native/tape/stock/precision costs, +compiler and analytic recovery remain separate. All five selected framework +assumptions remain. Independent human and formal proof-kernel review are +unclaimed. The selected cold replay, Lean, Docker and predecessor suites were +not run. + +## Exact finite evidence + +The standalone checker enumerates every binary one-symbol transition table +in dimensions 1,2,3 and every ordered two-symbol table in dimensions 1,2. +For each table it uses every row subspace for F and every column subspace +for B. Choosing canonical bases retains all zero/nonzero endpoint questions +and the two ranks, including arbitrary rectangular or dependent boundaries. +These are 137,896 normalized contracts, not a count of all literal boundary +matrices. The oracle visits 288,662 endpoint blocks, retaining duplicate word +paths and stopping at the first nonzero block. When no discrepancy appears, +it checks every word through D+1; histogram key zero means only this finite +observation, rather than a separate classification of zero-family root causes. +The continuum and arbitrary-field conclusions come from the written proof. + +Seed ranks use row-XOR elimination. The literal endpoint oracle instead uses +column dot products and enumerates the word tree without reachability pruning. +The five census domains contain respectively 8, 400, 131,072, 16 and 6,400 +contracts. All 650 triples with 1<=D<=12 and 1<=r,b<=D attain the predicted +first width. Their zero/one cyclic construction also has the all-field proof. + +Nine invalid rank/dimension inputs reject. Five semantic controls cover a +one-too-small horizon, a mixed-word discrepancy missed by repeated-symbol +testing, a discrepancy in a returned-role block, the false pass after dropping +that block, and zero transfer dimension. Explicit exceptions retain all checks +under optimization. No predecessor scientific numbers are recounted. + +The generated [RESULT.json](RESULT.json) binds all six scientific/package +source files by SHA256. Default execution compares the complete typed receipt +and writes nothing. `--emit /absolute/new/path.json` exclusively creates a new +generated receipt. The result file is excluded from its own source-hash list. + +## Reproduce + +From the repository root with CPython 3.12 and only its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/boundary-rank-horizon/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/boundary-rank-horizon/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/boundary-rank-horizon +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/boundary-rank-horizon --check-source-history +``` + +Another CPython 3.12 path may replace the displayed local interpreter. +Expected markers are `PASS_BOUNDARY_RANK_HORIZON`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +The shared runner also authenticates the historical catalogue and source +provenance in [SOURCES.json](SOURCES.json). The direct scientific verifier +needs only this package, with no Git, network or predecessor runtime input. +Each registered command has a 120-second limit. + +## Open next questions + +Can one actual complete provider/consumer residual exhibit b>1 and a useful +horizon reduction after every return is included? Extract its fixed table, +compute the positive seed and right-boundary ranks, and compare the horizons. +Physical table extraction and complete supplier costs remain blockers. This +question is unclaimed; no further construction search follows from this result. + +## Scope, credit and engineering + +The `formal-interface-lemma` card changes to a written exact-interface proof, +rather than a selected-caller formalization. Canonical base is +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected PR6030. +The current selected-baseline command passed its binding-only orientation. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375593) +records the independently posed question and live overlap limits. Source +sharing is limited to the credited physical model, not the separately claimed +uniform-approximation question. Main and live searches did not find this +rank-sensitive horizon; unpublished work and arbitrary historical diffs remain +unknown. Discovery stopped at the first proved step. + +Credit zxv / PR5441 for the physical table and earlier positive seed-rank +criterion, with its retained independent/inverse-register, native, compiler +and source-adapter lineage. Weighted-automata reachability and rank-nullity are +classical. Kiefer and coauthors, Tzeng, Crosswhite and Bacon retain the +foundational credit recorded in that proof. No general literature-priority +claim is made. + +Build the Lever shaped the standalone checker. Prove It Works and Test Behavior, +Not Implementation shaped the literal first-discrepancy oracle and returned-role +control. Foundational Thinking led to binary row/column subspaces as the finite +contract representation. The Investigation playbook kept predecessor results as +premises and separated the all-field proof from finite observations. + +Power-of-Ten inspection found no recursion, dynamic code generation or mutable +shared state. All functions fit below sixty physical lines. The census fixes +D<=3, at most two symbols, at most sixteen subspaces and 512 individual matrices. +The two-symbol census has D<=2. Its word trees and the mixed-word control have +at most sixteen paths at one level. Sharpness fixtures fix D<=12 and one symbol. +All scientific loops are bounded by those finite domains. The CLI accepts no +external matrix and only an optional output path. + +Rule 3 has a managed-runtime deviation. CPython allocates collections and +integers during replay; the fixed dimensions and binary coefficients bound live +data. The largest transition list has 512 matrices, and the receipt contains +only bounded aggregates. Extending the fixed census domains requires reviewing +those capacities. Warning-strict normal and optimized execution supplies the +available interpreter diagnostics. No external static analyzer is required. diff --git a/research/boundary-rank-horizon/RESULT.json b/research/boundary-rank-horizon/RESULT.json new file mode 100644 index 0000000000..0388236315 --- /dev/null +++ b/research/boundary-rank-horizon/RESULT.json @@ -0,0 +1,87 @@ +{ + "cases": 137896, + "censuses": [ + { + "alphabet_size": 1, + "cases": 8, + "dimension": 1, + "endpoint_blocks": 15, + "first_discrepancy_histogram": { + "0": 7, + "1": 1 + }, + "strictly_shorter_horizons": 0, + "subspaces": 2 + }, + { + "alphabet_size": 1, + "cases": 400, + "dimension": 2, + "endpoint_blocks": 870, + "first_discrepancy_histogram": { + "0": 229, + "1": 159, + "2": 12 + }, + "strictly_shorter_horizons": 45, + "subspaces": 5 + }, + { + "alphabet_size": 1, + "cases": 131072, + "dimension": 3, + "endpoint_blocks": 243875, + "first_discrepancy_histogram": { + "0": 34297, + "1": 87535, + "2": 8568, + "3": 672 + }, + "strictly_shorter_horizons": 56056, + "subspaces": 16 + }, + { + "alphabet_size": 2, + "cases": 16, + "dimension": 1, + "endpoint_blocks": 82, + "first_discrepancy_histogram": { + "0": 13, + "1": 3 + }, + "strictly_shorter_horizons": 0, + "subspaces": 2 + }, + { + "alphabet_size": 2, + "cases": 6400, + "dimension": 2, + "endpoint_blocks": 43820, + "first_discrepancy_histogram": { + "0": 2761, + "1": 3423, + "2": 216 + }, + "strictly_shorter_horizons": 477, + "subspaces": 5 + } + ], + "controls": { + "invalid_domains_rejected": 9, + "semantic_controls": 5 + }, + "endpoint_blocks": 288662, + "sharpness": { + "cases": 650, + "transcript_sha256": "b33b45759fec1a55d9b5f3d04dabbb9cb3e27237dee4f519783cd1f418a6b1f1" + }, + "source_sha256": { + "PROOF.md": "6222f2d0c54fb6bbcc638b4893a432d76bc9752b2e0bcc69260ff9ebe206938d", + "README.md": "349d2af70aa024e80bb52c52e7df41adeac1a7c7dce40674b57b8e840e7527c5", + "SOURCES.json": "fc91606eb796ef959aa01d7d2db6cf9cf1223eb2bef9d4567f644485c10a16e1", + "TASK.json": "35c6435501151490795cde5dd767abd2c74c3527f8e4f08babe74c8bb967623b", + "VERIFY.json": "abe91efdbf146837cf9c9438b1e0a56a7b724bce86f4183cf1c1e6cc03cc8422", + "verify.py": "b513149562989da1df96c2b620e182a73716cb959f7670f970ac7546f16ac2f6" + }, + "status": "PASS_BOUNDARY_RANK_HORIZON" +} diff --git a/research/boundary-rank-horizon/SOURCES.json b/research/boundary-rank-horizon/SOURCES.json new file mode 100644 index 0000000000..70eb9e513a --- /dev/null +++ b/research/boundary-rank-horizon/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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/finite-memory-lifting/PROOF.md", + "usage": "provenance", + "git_blob": "36152f9e31555a88ce3636ae59abf07a8058d78d", + "sha256": "de4a6b79d480d7718b3d157d2be73b4f45723ccac6719160dd815f8cef40356b" + }, + { + "path": "research/finite-memory-lifting/README.md", + "usage": "provenance", + "git_blob": "5ce4fa86af1d5487f9a639acdc9fa0177c76c192", + "sha256": "ca0be421d5cb1835a8814685907db78a7a3ea24b7e1e474f3038c87b0e46498e" + } + ] +} diff --git a/research/boundary-rank-horizon/TASK.json b/research/boundary-rank-horizon/TASK.json new file mode 100644 index 0000000000..4851dc4950 --- /dev/null +++ b/research/boundary-rank-horizon/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp positive-width equivalence horizon max(1,D-r-b+2), with positive seed rank r and right-boundary rank b, and attaining examples for every admissible triple over every field.", + "scope_change_reason": "An independently posed rank-nullity refinement of the fixed physical transfer-table interface replaces a selected-caller formalization. This is a written exact-interface proof with bounded corroboration, not a Lean proof or predecessor audit.", + "bottleneck_link": "A smaller exact finite horizon can reduce the largest physical width needed to reject or certify a supplied complete transfer representation. Actual table extraction and physical supplier admission remain separate.", + "budget_minutes": 60, + "stop_rule": "Discovery stops at the first proved horizon refinement and its sharpness family; no further mathematical extension.", + "outcome": "completed", + "evidence": "Written all-field proof; 137896 normalized binary contracts, 288662 literal endpoint-block observations, 650 sharp rank-triple fixtures, nine invalid-domain rejections and five semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual complete provider/consumer residual exhibit b>1 and a useful horizon reduction after all returns are included?", + "why_it_matters": "The abstract rank saving does not supply an extracted physical table or reduce its representation size.", + "first_step": "Extract one complete residual and compute its positive seed rank and exact right-boundary rank, then compare the two horizons.", + "blocked_by": "Actual source-table extraction and its complete native, ownership and physical costs are outside this package." + } + ], + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375593", + "question_source": "original", + "predecessor_author": "zxv", + "playbook": "Investigation", + "first_working_example": { + "command": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_selected_baseline.py", + "output": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY" + }, + "freshness": { + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "selected_record_sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "checked_at_utc": "2026-11-03T14:07:38Z", + "coverage": "Live open PR bodies, account recent PRs, active Discussions, recent handoffs, main README formula/object searches and merged/all-state searches. Arbitrary historical diffs and unpublished work are unknown." + } +} diff --git a/research/boundary-rank-horizon/VERIFY.json b/research/boundary-rank-horizon/VERIFY.json new file mode 100644 index 0000000000..4538aa8d8e --- /dev/null +++ b/research/boundary-rank-horizon/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact binary horizon census, all-triple sharpness fixtures, domain and semantic controls; full source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete checks with assertions disabled; checks use explicit exceptions." + } + ] +} diff --git a/research/boundary-rank-horizon/verify.py b/research/boundary-rank-horizon/verify.py new file mode 100644 index 0000000000..05e92b55a0 --- /dev/null +++ b/research/boundary-rank-horizon/verify.py @@ -0,0 +1,216 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the positive-width boundary-rank horizon.""" + +import argparse +from collections import Counter +import hashlib +from itertools import combinations, product +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def horizon(dimension, seed_rank, boundary_rank): + need(type(dimension) is int and 0 <= dimension <= 32, 'dimension') + need(type(seed_rank) is int and 0 <= seed_rank <= dimension, 'seed rank') + need(type(boundary_rank) is int and 0 <= boundary_rank <= dimension, + 'boundary rank') + if seed_rank == 0 or boundary_rank == 0: + return 0 + return max(1, dimension - seed_rank - boundary_rank + 2) + + +def basis(rows, dimension): + """Canonical binary RREF, using row XORs rather than the endpoint oracle.""" + pivots = [0] * dimension + for original in rows: + value = original + for pivot in range(dimension - 1, -1, -1): + if (value >> pivot) & 1: + if pivots[pivot]: + value ^= pivots[pivot] + else: + pivots[pivot] = value + break + for pivot in range(dimension): + for other in range(pivot + 1, dimension): + if (pivots[other] >> pivot) & 1: + pivots[other] ^= pivots[pivot] + return tuple(row for row in pivots if row) + + +def row_action(row, transition): + value = 0 + for index, matrix_row in enumerate(transition): + if (row >> index) & 1: + value ^= matrix_row + return value + + +def positive_rank(left, transitions, dimension): + rows = [row_action(row, transition) + for transition in transitions for row in left] + return len(basis(rows, dimension)) + + +def all_subspaces(dimension): + spaces = {()} + for size in range(1, dimension + 1): + for rows in combinations(range(1, 1 << dimension), size): + reduced = basis(rows, dimension) + if len(reduced) == size: + spaces.add(reduced) + return tuple(sorted(spaces)) + + +def matrix_columns(transition): + dimension = len(transition) + return tuple(sum(((transition[i] >> j) & 1) << i + for i in range(dimension)) for j in range(dimension)) + + +def first_discrepancy(left, transitions, right, depth): + """Literal word tree, retaining duplicate paths and using column dot products.""" + columns = tuple(matrix_columns(matrix) for matrix in transitions) + frontier = [(left, ())] + blocks = 0 + for width in range(1, depth + 1): + following = [] + for rows, word in frontier: + for symbol, matrix in enumerate(columns): + advanced = tuple(sum(((row & column).bit_count() & 1) << j + for j, column in enumerate(matrix)) + for row in rows) + blocks += 1 + for output_role, row in enumerate(advanced): + for input_role, column in enumerate(right): + if (row & column).bit_count() & 1: + return width, blocks, word + (symbol,), output_role, input_role + following.append((advanced, word + (symbol,))) + frontier = following + return 0, blocks, (), -1, -1 + + +def census(dimension, alphabet_size): + spaces = all_subspaces(dimension) + matrices = tuple(product(range(1 << dimension), repeat=dimension)) + histogram = Counter() + cases = blocks = shortened = 0 + for transitions in product(matrices, repeat=alphabet_size): + for left in spaces: + seed = positive_rank(left, transitions, dimension) + for right in spaces: + bound = horizon(dimension, seed, len(right)) + first, work, _, _, _ = first_discrepancy( + left, transitions, right, dimension + 1) + need(first == 0 or (bound > 0 and first <= bound), 'horizon violation') + need(bound != 0 or first == 0, 'zero-boundary violation') + cases += 1 + blocks += work + shortened += int(bound > 0 and bound < dimension - seed + 1) + histogram[str(first)] += 1 + return dict(dimension=dimension, alphabet_size=alphabet_size, + subspaces=len(spaces), cases=cases, endpoint_blocks=blocks, + strictly_shorter_horizons=shortened, + first_discrepancy_histogram=dict(sorted(histogram.items()))) + + +def sharp_instance(dimension, seed, boundary): + length = horizon(dimension, seed, boundary) + transition = [1 << i for i in range(dimension)] + if seed + boundary <= dimension + 1: + start = seed - 1 + stop = start + length - 1 + for index in range(start, stop + 1): + transition[index] = 1 << (start if index == stop else index + 1) + left = tuple(1 << i for i in range(seed - 1)) + (1 << stop,) + right = (1 << stop,) + tuple(1 << i for i in range(stop + 1, dimension)) + else: + left = tuple(1 << i for i in range(seed)) + right = tuple(1 << i for i in range(dimension - boundary, dimension)) + need(len(left) == seed and len(right) == boundary, 'sharp boundary shapes') + return left, (tuple(transition),), right + + +def sharp_cases(): + count = 0 + transcript = hashlib.sha256() + for dimension in range(1, 13): + for seed in range(1, dimension + 1): + for boundary in range(1, dimension + 1): + left, transitions, right = sharp_instance(dimension, seed, boundary) + need(positive_rank(left, transitions, dimension) == seed, 'sharp seed rank') + need(len(basis(right, dimension)) == boundary, 'sharp right rank') + first, _, _, _, _ = first_discrepancy(left, transitions, right, dimension) + need(first == horizon(dimension, seed, boundary), 'sharp first width') + transcript.update(f'{dimension},{seed},{boundary},{first}\n'.encode()) + count += 1 + return dict(cases=count, transcript_sha256=transcript.hexdigest()) + + +def controls(): + bad = ((-1, 0, 0), (33, 0, 0), (3, -1, 1), (3, 4, 1), + (3, 1, -1), (3, 1, 4), (True, 1, 1), (3, True, 1), (3, 1, False)) + rejected = 0 + for arguments in bad: + try: + horizon(*arguments) + except ValueError: + rejected += 1 + else: + raise ValueError('invalid domain accepted') + left, transitions, right = sharp_instance(8, 2, 3) + first, _, _, _, _ = first_discrepancy(left, transitions, right, 8) + need(first == 5 and first > 8 - 2 - 3 + 1, 'off-by-one control') + # Only the mixed word (0,1) is nonzero. Repeated-symbol testing misses it. + mixed = ((2, 0, 0), (0, 4, 0)) + hit = first_discrepancy((1,), mixed, (4,), 4) + need(hit[0] == 2 and hit[2] == (0, 1), 'mixed physical word') + for matrix in mixed: + need(first_discrepancy((1,), (matrix,), (4,), 4)[0] == 0, + 'constant-word trap') + # The only discrepancy can occur in a required returned-role block. + need(first_discrepancy((0, 1), ((1,),), (0, 1), 1)[3:] == (1, 1), + 'complete-role control') + need(first_discrepancy((0,), ((1,),), (0,), 3)[0] == 0, + 'dropped-role control') + need(horizon(0, 0, 0) == 0, 'zero dimension') + return dict(invalid_domains_rejected=rejected, semantic_controls=5) + + +def report(): + censuses = [census(dimension, 1) for dimension in range(1, 4)] + censuses += [census(dimension, 2) for dimension in range(1, 3)] + result = dict(status='PASS_BOUNDARY_RANK_HORIZON', censuses=censuses, + sharpness=sharp_cases(), controls=controls()) + result['cases'] = sum(row['cases'] for row in censuses) + result['endpoint_blocks'] = sum(row['endpoint_blocks'] for row in censuses) + package = Path(__file__).resolve().parent + names = ('README.md', 'PROOF.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + result['source_sha256'] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', type=Path, help='exclusively create a generated receipt') + arguments = parser.parse_args() + result = report() + encoded = json.dumps(result, sort_keys=True, indent=2) + '\n' + if arguments.emit is not None: + with arguments.emit.open('x', encoding='utf-8') as stream: + stream.write(encoded) + else: + expected = json.loads((Path(__file__).resolve().parent / 'RESULT.json').read_text()) + need(encoded == json.dumps(expected, sort_keys=True, indent=2) + '\n', + 'complete typed receipt mismatch') + print(encoded, end='') + + +if __name__ == '__main__': + main()