Prove exact dirty endpoint tests with bounded sign lifetimes

research/sign-frontier-identity/PROOF.md

@@ -0,0 +1,158 @@
+# Complete dirty endpoints with bounded live signs
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement and scope
+
+Consider a chronological word of L instructions on r independent roles.
+The permitted instructions are rational ADD, signed QUERY, signed unary
+APPLY and SWAP. An ADD is x_d <- x_d + c x_s. A QUERY is
+x_d <- x_d + c z_j x_s. An APPLY is x_d <- z_j x_d. A SWAP exchanges
+two roles. Here d != s, c is rational and each z_j independently belongs
+to {+1,-1}. Repeated occurrences of a label use the same sign. All roles
+have arbitrary initial values, and equality concerns their complete endpoint.
+
+After instruction t, let B_t consist of labels whose first occurrence is
+at most t and whose last occurrence is greater than t. Set
+
+    k = max_(0 <= t <= L) |B_t|,       D = r^2+1.
+
+An instruction containing a sign only once does not put it in either
+adjacent frontier. Such an instruction still branches over both signs.
+
+**Theorem.** Identity of the complete word at every sign assignment is
+decidable deterministically using at most
+
+    L * 2^(k+1) * D
+
+candidate prefix updates and O(L * 2^(k+1) * D^3) rational arithmetic
+operations. At each cut it retains at most 2^k * D actual prefix matrices.
+If the word is not the identity, it returns an actual sign assignment
+and hence a complete-endpoint counterexample. Rational bit complexity
+is 2^k times a polynomial in the ordinary input size. In particular,
+fixed r and bounded k give a polynomial-time exact test independently
+of the total number n of sign labels.
+
+The same test compares two words by appending the inverse of the second
+to the first. The parameter k is measured on that concatenation, not
+separately on each word. This qualification can matter substantially.
+
+## Homogeneous prefix invariant
+
+Let P be a complete r-by-r prefix matrix and define
+
+    h(P) = (vec(P),1) in Q^D.
+
+For every live assignment a on B_t, retain a set S_(t,a) of actual
+prefix matrices together with their actual sign histories. Its invariant is
+
+    span { h(P) : P in S_(t,a) }
+      = span { h(P_t(e)) : e is any prefix assignment restricting to a }.
+
+The right-hand set ranges over assignments to every label already seen,
+including forgotten labels. At t=0 there is only h(I), so the invariant
+holds. A basis needs at most D representatives; selection by exact
+incremental Gaussian elimination can keep actual members of the set.
+The normalized elimination rows are auxiliary data, never fake executions.
+
+For a fixed next sign, left multiplication by the instruction matrix A
+induces a linear map on homogeneous vectors,
+
+    (vec(P),u) -> (vec(AP),u).
+
+If the next sign is new, branch each representative with both choices.
+If its label is live, its value is already specified by a. Constant
+instructions do not branch. Apply the linear map to every representative.
+Then restrict the sign key to B_(t+1), merging keys for labels that have
+just reached their last occurrence. Taking the span of this union and
+selecting a basis preserves exactly the displayed invariant. Forgotten
+signs have no future occurrence, so this merger loses no future correlation.
+No bound on the number of their possible histories is assumed.
+
+At the last cut the frontier is empty. Define the linear map
+
+    F(vec(P),u) = vec(P) - u vec(I).
+
+Every complete endpoint equals I exactly when F vanishes on the final
+span. It suffices to check its retained basis. Each retained vector is
+h(P) for an actual assignment, so any failing basis member supplies an
+actual counterexample. A differing column supplies a dirty input on which
+the endpoints differ. This proves both decision and witness correctness.
+
+The homogeneous coordinate is necessary for this implementation. Ordinary
+linear span cannot distinguish the set {I} from {I,-I}. For example,
+applying the same sign once to each of the five roles has endpoint zI.
+Keeping only a nonhomogeneous basis can discard the negative endpoint.
+The supplied semantic control requires the negative assignment to survive.
+
+## Cost and exact arithmetic
+
+There are at most 2^k keys before an instruction, and each has at most D
+representatives. Each representative has at most two successors. Thus
+there are at most 2^(k+1)D candidate updates per instruction, including
+a sign occurring only once. Left multiplication costs O(r^3) operations
+even for a general dense instruction matrix. The supplied elementary
+updates cost only O(r). Incremental echelon reduction of a D-vector
+against at most D stored rows costs O(D^2). These bounds give the theorem.
+Only the previous and next layers, their elimination rows and their
+actual witnesses need remain live. Besides input and schedule storage,
+the space is O(2^k D^2) rationals and O(2^k D n) witness bits.
+
+For completeness, this is also a bit-complexity claim, not just a unit-cost
+field count. Let b bound the bit length of any input numerator or
+denominator. Clear each instruction's denominators first. The product
+of these denominators has O(Lb) bits, and products of r-by-r integer
+matrices have entry length O(L(b+log(r+1))). Hence every actual prefix
+has a polynomial-size rational representation. The homogeneous coordinate
+has the same bound after clearing row denominators. Elimination entries
+are ratios of minors of at most D such rows. The determinant expansion
+bounds their bit lengths by a polynomial in D,L,b. Exact rational
+arithmetic and independence tests therefore have polynomial bit cost.
+Witnesses are n-bit assignments. Label indices themselves remain part
+of the input encoding; sparse large indices can be renamed in order of
+first occurrence before this mathematical algorithm.
+
+## Native interpretation and comparison
+
+This is the commuting-sign subclass specified in PR #5716, Section 1.
+For the diagonal generator Z_j e_x=(-1)^(x_j)e_x, its f-fold tensor power
+acts on an address tuple by the scalar
+
+    z_j = (-1)^(x_j^(1)+...+x_j^(f)).
+
+Every sign assignment is realized at f=1. It is also realized for every
+positive f by using its binary address in the first tensor factor and
+zero addresses in the remaining factors. Instructions preserve addresses,
+so their complete endpoint is block diagonal with the scalar endpoints
+just tested. The theorem therefore decides equality at every positive
+tensor width in this exact subclass. This application uses the stated
+sign semantics; it does not check another contributor's compiler.
+
+ADD and QUERY are inverted by negating c; APPLY and SWAP are involutions.
+Reverse the instruction order to invert a word. If P and Q are the two
+endpoints, first executing the first word and then the inverse second word
+has endpoint Q^(-1)P. It is I if and only if P=Q, on every sign assignment.
+No zero role, erased output, independent resampling of repeated signs or
+unpaid physical operation is introduced by this mathematical reduction.
+
+## What is new here
+
+PR #5716 explicitly asks for a useful restricted class with a tractable
+complete-endpoint identity test. The contribution is the live-sign
+restriction, the displayed source-grammar bound and the executable
+counterexample-preserving test. It is a scoped answer to that question,
+not a new general weighted-automaton equivalence principle or a claim
+of priority for parameterized dynamic programming.
+
+Reachable-span bases and retaining concrete witnesses are classical.
+See Stefan Kiefer, [Notes on Equivalence and Minimization of Weighted
+Automata](https://arxiv.org/abs/2009.01217), Section 2, especially
+Propositions 2.1 and 2.2, and the Schutzenberger/Tzeng lineage cited there.
+The adaptation here conditions the span on currently live signs, forgets
+them only after their final occurrence and homogenizes complete matrices
+to test an affine equality. The proof above is self-contained.
+
+No small k is proved for the selected P104 caller, the CNF hardness
+construction or general native affine/quadratic operators. Noncommuting
+address maps and rounded arithmetic are excluded. There is no new kappa,
+physical tariff, supplier admission or complete multiplication theorem.

research/sign-frontier-identity/README.md

@@ -0,0 +1,163 @@
+# Exact dirty-endpoint tests with bounded live signs
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Result
+
+Scoped written mathematical proof with exact finite corroboration. For a word
+of L rational ADD, signed QUERY, signed APPLY and SWAP instructions on r
+arbitrary dirty roles, let k be the maximum number of signs that have appeared
+but will appear again. Complete identity at every assignment is decidable in
+
+    O(L * 2^(k+1) * (r^2+1)^3)
+
+rational operations, with at most 2^k(r^2+1) retained actual prefix matrices.
+Bit complexity is 2^k times a polynomial in the ordinary input size. A failed
+identity returns an actual sign assignment. Repeated signs remain correlated,
+and every input and returned role participates in the endpoint.
+
+In the commuting diagonal-sign native subclass, this decides equality at every
+positive tensor width. Two words can be compared by appending the inverse of
+the second to the first; k is measured on the concatenation. No small k is
+asserted for the selected caller or the general hardness construction.
+
+[PROOF.md](PROOF.md) gives the theorem, homogeneous span invariant, field and
+bit bounds, native interpretation and exact limitations. The algorithm is
+
+```text
+for each instruction
+  branch new signs; preserve every live sign
+  transform actual prefix matrices within each live-sign assignment
+  forget signs at their last use; retain a homogeneous span basis
+check every final representative against the complete identity
+```
+
+The extra homogeneous coordinate distinguishes I from -I. A basis consists
+of genuine prefixes with genuine assignments, so a failing representative
+is a concrete counterexample rather than a formal linear combination.
+
+## Source and novelty boundary
+
+Hiroki KUMAZAKI's [PR #5716](https://github.com/CrocSwap/integer-mult-bounds/pull/5716),
+head `946acb3a36953216dd9a39f0c5222a40a9e90cd3`, explicitly asks for a useful
+restricted class with a tractable complete-endpoint identity test. This
+package answers that open question with the bounded live-sign hypothesis.
+Its CNF audit and Ali Romman's [PR #5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369)
+reduction are cited, not rechecked as this contribution. Barrington retains
+the classical five-role branching-program method.
+
+Reachable-span reduction and concrete witness retention are classical; see
+Stefan Kiefer's [weighted-automata notes](https://arxiv.org/abs/2009.01217),
+Section 2 and its Schutzenberger/Tzeng references. The new contribution is
+the live-sign-conditioned complete-endpoint application and explicit bound,
+not a new general equivalence algorithm or a literature-priority claim.
+zxv's [PR #5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235)
+handles independent formal operators, and
+[PR #5441](https://github.com/CrocSwap/integer-mult-bounds/pull/5441) handles
+already supplied fixed transfer tables across tensor columns. Neither is
+the repeated-sign lifetime bound proved here. Their methods retain credit.
+
+Canonical base is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
+[SOURCES.json](SOURCES.json) pins the question and grammar documents; the direct
+verifier checks their hashes without executing predecessor code. Selected
+metadata and the task card are provenance only. This explicitly changes the
+`formal-interface-lemma` card to an informal algorithmic side result; no proof
+assistant build or selected assumption discharge is claimed.
+
+The initial overlap cache covered 470 open PRs and 5,432 Discussion records
+with complete reported pagination. Its local filesystem search was sparse,
+so separate main-tree README searches and merged-PR searches were also used.
+These searches do not cover unpublished work or every historical code diff.
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217826).
+
+## Reproduction and evidence
+
+From the repository root, with CPython 3.12 and its standard library only:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sign-frontier-identity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sign-frontier-identity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sign-frontier-identity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sign-frontier-identity --check-source-history
+```
+
+Elsewhere substitute a CPython 3.12 executable. Expected direct status is
+`PASS_SIGN_FRONTIER_IDENTITY`; registered replay ends with
+`PASS_REGISTERED_RESEARCH_PACKAGE`. Each registered command has a 120-second
+timeout. The direct checker writes a generated JSON receipt to stdout, binding
+every package file by SHA256; redirect it outside the checkout if desired.
+It neither reads a saved expected receipt nor writes files into the package.
+
+The finite checks include:
+
+- All 1,555 words of length zero through four over the declared six-gate
+  alphabet, with 4,097 exhaustive sign assignments.
+- 216 structured words on two, three and five roles, with 9,216 exhaustive
+  assignments. A separate column-vector interpreter checks every input column,
+  complete endpoint verdict and returned counterexample.
+- Two 128-sign families. The width-zero negative family retains two matrices
+  and returns a literal witness although its all-positive assignment is the
+  identity. The width-one positive family preserves repeated-sign cancellation.
+  Each processes exactly 512 candidates. These families are not exhaustively
+  enumerated over their sign assignments.
+- An eight-live-sign identity visiting all 256 live keys, with 1,020 candidate
+  updates, plus five capacity/inverse fixtures. These cover the 4,096-gate
+  limit, label 4,095, 64-bit coefficients, the empty one-role word and a mixed
+  ADD/QUERY/APPLY/SWAP inverse.
+- Eighteen invalid-input/capacity rejections and three semantic controls for
+  homogeneous scalar phases, correlated repeated signs and independent signs.
+
+The infinite statement rests on the written invariant and bit argument;
+finite comparisons corroborate the implementation. Local normal/optimized
+registered replay, source metadata and committed-byte/source-history checks
+are separate from hosted CI and independent scientific acceptance.
+
+## Limitations
+
+The executable accepts 1..5 roles, at most 4,096 gates, frontier limit at most
+eight, sign labels 0..4,095 and exact fractions with numerator/denominator
+length at most 64 bits. It rejects larger inputs rather than narrowing its
+verdict silently. The written theorem does not require these implementation
+caps. It is an exact code API, not a native-source parser or general compiler.
+
+Only commuting diagonal signs are covered. Arbitrary affine address changes,
+quadratic phases, nonlinear leaves, rounding, ownership, physical routing,
+precision/tapes and paid supplier costs need separate contracts. The test
+does not supply a faster physical word or a new multiplication theorem.
+No new kappa or selected-frontier change. Independent human and formal
+proof-kernel review are unclaimed. No predecessor scientific suite, selected
+cold replay, Lean or Docker run was performed.
+
+## Implementation inspection
+
+The bounded executable uses no recursion. All loops range over validated
+inputs, finite sign branches, at most 256 live assignments and at most 26
+representatives per assignment. An input check precedes frontier allocation.
+State and witnesses are local to one decision. Scientific checks use explicit
+exceptions and remain enabled under optimization. Functions stay below 60
+physical lines. Warning-strict normal/optimized execution and AST compilation
+provide the available standard-library diagnostics; no external static
+analyzer is required or claimed.
+
+Power-of-Ten rule 3 deviation: CPython and Fraction allocate managed objects
+during elimination. This is confined to the validated solver domain above,
+with two adjacent layers, at most 26 elimination rows per key and the
+polynomial rational-size bound in PROOF.md. Capacity rejection and maximum
+frontier/gate/label/coefficient fixtures verify the bounds. A fixed-allocation
+implementation would be a separate lower-level port; no constant-RSS claim
+is made. Rule 8/9 deviation: the verifier loads the single package-local
+solver via a fixed importlib path, and rejection controls use bounded local
+callbacks. No external path or callback is accepted. Normal and optimized
+replay exercise every such target.
+
+## Open next questions
+
+1. Does a useful emitted caller in this subclass have small k after legal
+   reordering? Extract labels and their first/last occurrences from one exact
+   word before attempting reordering. A source-bound extraction contract and
+   preservation of every dirty return are still needed.
+2. Can one correlated family avoid explicit enumeration of its live signs?
+   Begin with a precise replacement invariant. Large k remains exponential
+   here; generic hardness is not contradicted.
+
+[TASK.json](TASK.json) records the relevance, first step and blockers for both.

research/sign-frontier-identity/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/reversible-cnf-independent-audit/PROOF.md",
+      "usage": "input",
+      "git_blob": "5d4ba20edc00381c72de756fd2fbd7fa33dfbeba",
+      "sha256": "5e35ffc14e07fa87d7e1fd467ca0aabe8a3922dd31a9bfd5a73a20d48b6df68c"
+    },
+    {
+      "path": "research/reversible-cnf-independent-audit/README.md",
+      "usage": "input",
+      "git_blob": "5ae1ef6558a2218d8c54530fd131d1fdc49e87e8",
+      "sha256": "dce8411944f39a1bfdcbf7eacc40e0e55612e65b145dda0f674606f68a7e3c71"
+    }
+  ]
+}