Certify rectangular dirty circuits with k+1-coordinate witnesses (no κ)

research/rectangular-dirty-certificates/DECISIONS.md

@@ -0,0 +1,39 @@
+# Implementation limits
+
+Investigation playbook. Build the Lever shaped the choice to retain a runnable
+certificate producer/checker. Prove It Works shaped the explicit-word and
+literal rectangular matrix oracles. The Power of Ten inspections are scoped
+to the three new Python files; predecessor files are read-only provenance.
+
+All control flow is structured and nonrecursive. Public inputs limit roles
+to 16, types to 8, arrows to 16 and each program to 128 instructions. The
+combined state dimension is at most 288. The basis accepts at most D rows;
+there are at most 16D arrow successor candidates. Each path has fewer than D
+letters. Echelon and coordinate loops have at most D rows or entries. The
+finite test loops have explicit bounds. No solver, subprocess or unbounded
+queue is used. All functions are shorter than sixty lines.
+
+Rule 3, fixed allocation, requires a managed-runtime deviation in these three
+files. Python lists, dictionaries and Fraction allocate during elimination.
+Live rational-cell storage is polynomial in the enforced finite input sizes;
+exact rational bit growth can still be large. Certificate encodings are capped
+and refused explicitly. The implementation makes no practical space or runtime
+promise for every capped problem. No fixed-size real-time allocator is supplied.
+The bounded small fixtures and registered 120-second timeout cover this replay.
+A deployment requiring a hard memory budget must use an external process
+memory limit or a bounded exact-arithmetic backend before accepting untrusted
+workloads. The tool is intended for local research input, not a service.
+
+Rule 9, indirect calls, has a narrow test-only deviation: must_reject receives
+one of the locally defined validation/checker lambdas. There are fourteen
+enumerated controls. Production compilation and certificate checking call
+named functions directly. No runtime registration or generated executable code
+is used. File resources use context managers; CLI writes are exclusive-create.
+
+Externally supplied arguments use ordinary rejecting checks. Internal compiler
+state-count and basis-dimension invariants use assertions; every scientific
+acceptance condition uses require and remains active under Python -O. Both
+registered commands enable warning errors. No external linter or type checker
+is installed in the declared standard-library environment. Repository metadata,
+publication-byte/source-history checks and literal CLI examples supplement the
+normal/optimized scientific replay. No repository-wide diagnostics are changed.

research/rectangular-dirty-certificates/PROOF.md

@@ -0,0 +1,164 @@
+# Compact certificates with rectangular payload types
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement and credit
+
+Let K be a field. A finite set of types t has independently chosen
+finite-dimensional spaces V_t, which may have dimension zero. Each arrow a
+has a declared source s(a) and target t(a), and denotes an arbitrary linear
+map X_a:V_s(a)->V_t(a). Different arrows are independent, including arrows
+with identical endpoints. A register has one fixed type and an arbitrary
+independent initial value. Scalar ADD and SWAP require equal register types;
+SCALE acts within one register; QUERY adds c X_a v_src to v_dst with matching
+types. APPLY is permitted only for an endomorphism of the register's type.
+Every register is retained in the complete endpoint. Scalars are central.
+
+**Typed bridge.** A program with r registers and q unary occurrences has
+r+q dependency states. For two programs on the same registers, let
+D=2r+q_left+q_right. Equality for every choice of the V_t and X_a is
+equivalent to a reachable-row closure certificate with at most D rows.
+Exact arithmetic finds either such a certificate or a shortest nonzero
+typed coefficient path w of length k. In the latter case a literal
+rectangular substitution with zero/one entries distinguishes the endpoints,
+using dimension
+
+    d_t = number of visits to type t along w,
+    sum_t d_t = k+1.
+
+Here k is at most the larger unary dependency depth of the two programs,
+and at most D-1. Types not visited by w have dimension zero. If all type
+spaces must be nonzero, add one unused coordinate to each unvisited type.
+This is a constructive upper bound, not a minimum-dimension theorem for
+arbitrary counterexamples.
+
+The equal-space dependency compiler and closure method are zxv's
+[PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), whose
+proof is pinned in SOURCES.json. Its classical weighted-automata and
+noncommutative PIT credit remains with Kiefer and Raz–Shpilka. Expanded
+typed block-polynomial identities already occur in Philipp / mightyOil's
+[PR1294](https://github.com/CrocSwap/integer-mult-bounds/pull/1294), following
+Charles Bethin's PR1278. Krzysztof Wójt's PR5262 supplies a different,
+inverse-aware equal-space model. No new general PIT algorithm, first typed
+path algebra, or literature priority is claimed. The present contribution
+is the typed compact interface, per-type path-witness construction, and
+rerunnable implementation with complete dirty boundaries.
+
+## 1. Typed dependency representation
+
+Create one leaf atom x_i for each original register. Maintain each current
+register as a scalar row of atoms of its own type. At a unary occurrence,
+first read the entire old source row e. Introduce an atom z_j=X_a e, of
+type t(a), with dependency row e supported on atoms of type s(a). APPLY
+replaces its register row by the new unit row; QUERY adds c times that row.
+Scalar operations update rows directly. This also specifies self queries:
+they read the pre-instruction value. Dependencies point only to older atoms.
+Thus exactly r+q atoms suffice without expanding paths.
+
+Let U be the final register rows. Define T_a to have dependency row e in
+row j precisely when atom j was introduced with label a, and zero elsewhere.
+Let V project leaf atoms to their original input register and other atoms
+to zero. Induction on the dependency order gives
+
+    coefficient of w=a_1...a_k in endpoint (o,i)
+        = (U T_a1 ... T_ak V)_(o,i).
+
+Matrix product order is literal: QP applies P first. A row supported on
+atoms of type t(a) becomes a row supported on type s(a) after multiplication
+by T_a; a mismatched arrow gives zero. Therefore every nonzero path has
+the declared endpoint types. Empty paths are identities within one type.
+
+For a pair of programs take block diagonal transitions, concatenate their
+final rows with a minus sign on the right, and stack their leaf projections.
+The two compiled leaf copies project to the same original input roles.
+They do not create additional independent payloads. This gives D states.
+
+## 2. Closure certificate and decision
+
+A certificate supplies reachable rows B_j=U_o T_w, an initial-span matrix H,
+and closure matrices C_a satisfying
+
+    U = H B,      B T_a = C_a B for every a,      B V = 0.
+
+These finite equations imply U T_w V=0 for every path by induction. Typed
+paths form the basis of the free path algebra. Evaluating each arrow in its
+declared rectangular block preserves addition, scalar multiplication and
+composable products, so all complete endpoint blocks agree in every dimension.
+
+Conversely, if every typed coefficient is zero, the reachable row space is
+annihilated by V and stable under all T_a. Choose a basis of reachable rows.
+It has at most D elements and supplies H and C_a. The next section proves
+that a nonzero coefficient contradicts universal equality, completing both
+directions of the theorem.
+
+The producer processes independent rows breadth first, starting with U's
+rows, and enqueues every composable arrow successor. A dependent candidate
+is expressed using earlier accepted rows of no greater path length. Its
+successors are therefore spanned by their successors. Induction on length
+shows no shortest nonzero coefficient is lost by rejecting dependent rows.
+The search accepts at most D rows, so a discovered path has length at most
+D-1. Acyclic atom dependencies also bound its length by the program's maximum
+unary dependency depth. Exact elimination constructs all displayed coordinates.
+
+The checker reconstructs the path rows and checks only the three equations;
+it performs no elimination and does not need basis independence. A negative
+certificate checks a nonzero coefficient and constructs the matrices below.
+It does not certify shortestness. Shortestness is a property of the producer
+and the proof, supplemented by explicit-word comparisons in the finite tests.
+
+## 3. Rectangular path witnesses
+
+Take a nonzero coefficient c in output o, input i and composable word
+w=a_1...a_k. Let t_0 be the output type and t_j=s(a_j), so
+a_j:t_j->t_(j-1) and t_k is the input type. For each t choose a basis
+
+    {e_j : 0<=j<=k and t_j=t}
+
+of V_t. These basis vectors are distinct even when a type repeats. Define
+
+    N_a e_(j+1) = e_j if a_(j+1)=a,
+    N_a e_l = 0 on every remaining basis vector.
+
+Equivalently, N_a is the sum of the matching rectangular matrix units.
+Every factor decreases the global path index by exactly one. Thus a product
+N_u has its (e_0,e_k) entry equal to one exactly when u=w. Shorter products
+cannot traverse k steps; longer products vanish. Repeated vertices and
+repeated arrow labels do not create shortcuts because coordinates retain
+their global indices. Consequently input e_k in register i and zero in every
+other register gives discrepancy c in output register o at coordinate e_0.
+This proves the displayed dimension formula. For k=0 all arrows are zero,
+the visited type has one coordinate, and the empty coefficient is detected.
+
+For a directed chain through distinct types every type must be nonzero for
+its monomial to be nonzero. The construction uses exactly one coordinate at
+each vertex. This observation does not assert a sharp general witness bound
+when types repeat or different monomials interact.
+
+## 4. Tensor substitution and executable boundary
+
+A positive typed identity can be evaluated at X_a=G_a^(tensor f) for each
+positive f, with register type space V_t^(tensor f). Rectangular composition
+still commutes with tensor powers. Scalar c stays c, outside the tensor power;
+the procedure never tensors an entire sum. This is an algebraic substitution
+corollary, not native implementation or a complete supplier invoice.
+
+The theorem is over arbitrary fields. The executable uses exact Q only and
+rejects excess resource sizes. It admits at most sixteen registers, eight
+types, sixteen arrows, and 128 instructions per side, hence D<=288. Input
+scalar encodings have at most 160 characters and 512 numerator/denominator
+bits. Certificate scalars have at most 4096 characters and 8192 bits. A
+larger certificate is explicitly refused by the producer. The unbounded
+field-operation theorem does not claim executable success beyond these caps.
+Program validation rejects mismatched types instead of coercing spaces.
+
+The checker shares the compiler, arithmetic, path reconstruction and witness
+routine with the producer. Those components, the input transcription and
+Python remain trusted. Explicit-word expansion and literal rectangular matrix
+execution are separately implemented finite oracles. The proof is written
+mathematics, not a proof-assistant theorem or independent human review.
+
+No relations between arrows, affine offsets, external aliases, nonlinear
+operations or rounded endpoints are covered. Dirty restoration is checked
+algebraically because every role is retained. Physical storage, native
+delivery, precision, all-size compiler uniformity and the complete signed
+invoice remain separate obligations. No new kappa is claimed.

research/rectangular-dirty-certificates/README.md

@@ -0,0 +1,102 @@
+# Compact universal certificates for rectangular dirty circuits
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+This is a scoped written proof and exact implementation of the independent
+rectangular-operator interface missing from zxv's [PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235).
+Registers may belong to different payload spaces. An arrow has a fixed source
+and target type, and every initial register is arbitrary. Equality certificates
+retain all returned dirt. No supplier or new kappa is claimed.
+
+[PROOF.md](PROOF.md) extends the predecessor's r+q dependency-state method to
+this interface. Two programs need D=2r+q_left+q_right states. An equality
+certificate has at most D reachable rows and finite closure equations.
+A nonzero path of length k has a concrete zero/one rectangular counterexample
+using one coordinate per visit to each type, totaling k+1 coordinates.
+This replaces padding every type to a common square witness dimension.
+It is an upper bound, not a general minimum-dimension claim.
+
+The contribution adds the typed compact compiler, closure checker, explicit
+per-type witnesses and runnable examples. Classical weighted-automata/PIT
+methods and zxv's equal-space bridge retain their credit. Philipp / mightyOil's
+PR1294 already proves expanded typed block identities following Charles Bethin
+PR1278; that result is cited rather than reverified. Krzysztof Wójt's PR5262
+handles named inverses in a common space, a different operator model. The
+retained dirty-echo lineage includes androolloyd, Chafik Boukhalfa / chafreaky
+PR628 and Ali Romman PR621; the tensor and universal-phase lineage retains
+Cinna Davis PR4100/4088, ToikY, Sagar Thakrar and roger-sato.
+
+## Reproduce
+
+From the repository root, using Python 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rectangular-dirty-certificates
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rectangular-dirty-certificates/verify.py
+```
+
+The registered normal and optimized checks print a generated JSON receipt
+with source hashes. They write no files. The finite suite covers 160 program
+pairs against explicit ordered-word expansion, 86 equal and 74 different;
+all 74 differences have literal rectangular matrix witnesses. It also covers
+64 dimension vectors and 352 full-column or zero-input echo cases, including
+zero-dimensional spaces; six dirty product witnesses through degree six;
+and fourteen rejecting or discrepancy controls. The degree-six example uses
+type dimensions 4 and 3, totaling seven rather than a square padded total
+of fourteen. That comparison concerns this path construction only.
+
+Run a single problem and check its inspectable certificate with a fresh output
+path inside a scratch directory:
+
+```sh
+PYTHON=/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12
+"$PYTHON" -I -B research/rectangular-dirty-certificates/typed_words.py \
+  research/rectangular-dirty-certificates/echo.json --output /tmp/rectangular-certificate.json
+"$PYTHON" -I -B research/rectangular-dirty-certificates/check_certificate.py \
+  research/rectangular-dirty-certificates/echo.json /tmp/rectangular-certificate.json
+```
+
+The output path must not exist. To inspect a negative matrix witness, replace
+the two example paths with `chain6.json` and its committed `chain6.certificate.json`.
+Arrow endpoints are `[source_type,target_type]`. Scalar instructions require
+equal types. APPLY requires a loop; QUERY permits rectangular arrows. Scalars
+are integers or explicit rational strings. Order QP means P applies first.
+
+## Scope and trust
+
+The executable uses Q. The written theorem works over any field. Inputs are
+bounded to sixteen roles, eight types, sixteen arrows and 128 instructions per
+side. Exact scalar encoding caps and the trusted shared compiler are documented
+in PROOF.md. A scalar-size refusal is not a verdict of equality or inequality.
+The checker performs no elimination; it shares compilation and arithmetic with
+the producer. The two finite oracles are separately written, not independent
+human reviewers. Independent human and formal proof-kernel review are unclaimed.
+
+Inverse, finite-group and commutation relations are excluded. So are native
+implementation, nonlinear inputs, external aliases, rounding, precision,
+hosting, physical tapes and a complete paid/target invoice. None of the five
+selected framework assumptions is discharged, and the selected record is
+unchanged. This is a changed scope from `joint-query-controller`: it supplies
+an algebraic gate for mixed-width interfaces rather than a cheaper caller.
+The card's selected-baseline orientation passed, with no supplier replay.
+
+Live open/merged searches, main README searches and reservations were checked
+before the advance [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267728).
+The overlap cache covered 317 open PRs and 5858 discussion records; the local
+working search omitted 8486 sparse note paths, so main was also searched
+directly for rectangular certificates, typed operators and quivers. This is
+bounded overlap evidence, not proof of global novelty.
+
+## Open next questions
+
+- Bind a mixed-width supplier's literal source and complete endpoint to this
+  grammar. Start with one declared producer/consumer boundary and record all
+  arrows and dirt. Native relations or unpriced physical delivery may prevent
+  applying this independent-arrow test.
+- Characterize the type graphs for which scalar spaces already separate all
+  paths. Start with acyclic graphs, then isolate the obstruction from multiple
+  cycles. This could reduce diagnostics further; no such classification or
+  random-testing guarantee is supplied here.
+
+Structured questions are in TASK.json. The first proved interface improvement
+is frozen; these follow-ons are outside this contribution.

research/rectangular-dirty-certificates/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839",
+  "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/inverse-dirty-certificates/README.md",
+      "usage": "input",
+      "git_blob": "1f895da66011f6ae59970cc0331b2fa00840568d",
+      "sha256": "e43549a712b8aab26b904b4da140b2924f7fee82407c5cdbe362303802456184"
+    },
+    {
+      "path": "research/universal-dirty-certificates/PROOF.md",
+      "usage": "input",
+      "git_blob": "3a405e327a7fd5d59a570d7f9920f1ce7f229a76",
+      "sha256": "ef4cfcfd65b1dde1f11eedace0ed90a1b47a2cc100daaf778fbecbff3ec685a7"
+    },
+    {
+      "path": "research/universal-dirty-phase-identities/README.md",
+      "usage": "input",
+      "git_blob": "fdebc9c89099f0f59b2b1cc4353bc33786529011",
+      "sha256": "3620ec8ae93b66af22d9dff045a339ff75160b4e6c334518a01768dd69e6a0ea"
+    }
+  ]
+}