Prove sharp boundary-rank endpoint horizon (no κ)

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.

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.

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"
+}

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"
+    }
+  ]
+}