Prove a sharp bounded-error threshold for frame cuts (no κ)

research/bounded-error-partition-threshold/PROOF.md

@@ -0,0 +1,159 @@
+# Successful-input fibers preserve partition bounds above 1/q
+
+## Model
+
+Fix an alphabet A of size q>=2. A finite acyclic deterministic circuit has
+W independent uniform input symbols. Each physical wire carries one symbol.
+A gate applies a fixed arbitrary function to its incoming symbols and may
+have several output ports. Copying uses separate physical wires. Fixed clean
+constants and discarded workspace are allowed; preloaded data-dependent
+advice is excluded. The topology and local functions are fixed.
+
+Each designated input w is demanded at one distinct designated sink rho(w).
+Let S be the set of tuples on which all demands succeed, and p=|S|/q^W.
+There is no correctness requirement outside S. Other independent inputs can
+be fixed in the proof; include them among the demands if restoration is
+required. Distinct sinks and independent designated inputs are essential.
+
+Vertices have rational m-by-m frames M_v. Each gate uses one common frame
+on all ports. Charge every physical edge (u,v), including terminal, control
+and fan-out edges, by rank_Q(M_v-M_u). Write s for their sum. Each demand
+has terminal shift M_out(rho(w))-M_in(w)=I_m. No linearity or invertibility
+of the scalar gates is assumed. The attaining examples are invertible.
+
+## 1. Successful-fiber inequality
+
+Choose any vertex class C. Let D be the designated inputs whose sources are
+in C and required sinks are outside. Put d=|D|. Let e be the number of edges
+leaving C, in fixed chronological order. Then
+
+    p <= min(1, q^(e-d)).                                  (1)
+
+Fix all inputs outside D. For a successful tuple, record its e outgoing
+wire symbols. The transcript and fixed outside inputs determine every
+outside vertex: simulate them in topological order, using the recorded
+entry whenever a wire enters from C. Re-entry into C is allowed; no
+chronological-cut hypothesis is needed. There is no extra message channel.
+
+Two distinct successful D tuples cannot have the same transcript. Otherwise
+outside simulation gives the same distinct demanded sinks, although those
+sinks must reproduce different D tuples. Thus at most q^e of the q^d D
+tuples succeed for each fixed outside tuple. There are q^(W-d) outside
+tuples. Counting proves (1). This is the successful-subset extension of
+PR1757's zero-error outgoing-transcript argument.
+
+If p>1/q, then e>=d for every C. Indeed, e<d implies the integer inequality
+e-d<=-1 and hence p<=1/q. The strictness is necessary, as shown below.
+
+## 2. Weighted partition certificates
+
+For a vertex labeling ell, apply e>=d to each label class and sum:
+
+    #{edges (u,v): ell(u)!=ell(v)}
+      >= #{demands w: ell(in(w))!=ell(out(rho(w)))}.         (2)
+
+Each crossing physical edge leaves exactly one class. Each separated demand
+is counted once. Re-entry and fan-out do not change this accounting.
+
+Suppose finitely many labelings ell_j and nonnegative weights c_j satisfy,
+on every physical edge,
+
+    sum_j c_j [ell_j(u)!=ell_j(v)] <= rank_Q(M_v-M_u).
+
+Multiplying (2) by c_j and summing shows that p>1/q implies
+
+    s >= sum_w sum_j c_j
+               [ell_j(in(w))!=ell_j(out(rho(w)))].           (3)
+
+The edge inequalities are required certificates, not an assertion that all
+rational rank metrics have a useful partition representation. The new
+premise p>1/q replaces zero error in the credited partition implication.
+
+## 3. Common-flag consequence
+
+Assume there are one common rational offset A_0 and an invertible B over a
+characteristic-zero extension K of Q such that T_v=B^-1(M_v-A_0)B is upper
+triangular at every vertex. For i=1,...,m label v by (T_v)_ii. The terminal
+shift I_m separates every demand in each of these m labelings.
+
+An upper triangular matrix has rank at least the number of its nonzero
+diagonal entries: its principal submatrix on those indices has nonzero
+determinant. Extending the field and conjugating preserve rational matrix
+rank. Thus the m unit-weight labelings satisfy the edge inequalities in (3):
+
+    p>1/q  implies  s>=Wm.                                 (4)
+
+This includes nonsplit flags over K and noncommuting triangular families.
+The checker uses rational triangular frames. The extension-field conclusion
+rests on the written argument, not on a finite extension-field replay.
+
+For 0<alpha<1 and 0<=r<=m, (r/m)^alpha>=r/m. Therefore the optimistic
+normalized recursive moment is at least s/(Wm)>=1 under (4). Extra
+nonnegative charges cannot create contraction. This is a scoped circuit
+obstruction, not an integer-multiplication lower bound.
+
+## 4. Sharpness with reversible circuits and the same terminals
+
+For every q>=2, m>=1 and W>=2, put P=diag(1,0,...,0). Take two independent
+symbols x,y and prescribe their swap. Their source frames are 0 and P.
+The sink on physical wire zero demands y and has frame P+I_m. The sink on
+physical wire one demands x and has frame I_m. Each demand therefore has
+precisely the required identity shift.
+
+First use the identity circuit, with no gates. It returns (x,y), meeting
+(y,x) exactly when x=y, on q of q^2 inputs. The terminal edge ranks are
+
+    rank(P+I_m)=m,        rank(I_m-P)=m-1.
+
+Hence p=1/q and s=2m-1. All frames are diagonal. Add W-2 untouched identity
+demands with source zero and sink I_m to obtain s=Wm-1 with the same success.
+This proves sharpness even with an invertible scalar map and just one rank
+unit of deficit. It does not assert sharpness for each fixed topology.
+
+An exact swap is available with the same terminal frames. Identify the
+alphabet with Z/qZ and perform
+
+    x <- x+y;    y <- x-y;    x <- x-y.
+
+Each assignment reads the current values. The final values are (y_old,x_old)
+for every q, including composite q. Each gate is invertible and has common
+frame P. Each is represented as a two-input/two-output gate, retaining the
+unchanged operand on an explicit output port. Entrance ranks sum to one,
+internal ranks are zero, and exit ranks sum to 2m-1. Thus s=2m, or Wm with
+the extra identity demands. Every physical wire is charged.
+
+No physical native implementation or zero-cost ordinary arithmetic is
+claimed for these symbolic framed circuits.
+
+## 5. Independent coins and expected cost
+
+Condition on any fixed independent random seed. If its circuit has rank
+bill strictly below the value of a valid partition certificate, (3) bounds
+its success by 1/q. Average over the seed distribution. The same bound
+holds. The certificate and topology may depend on the seed, and the proof
+does not require finitely many seeds. For common flags the premise is
+s<Wm in every seed, with the stated flag and terminal contract in each.
+
+Expected cost alone is insufficient. Choose the exact swap with probability
+lambda in (0,1), and the identity circuit with probability 1-lambda. Their
+terminal frames and demands coincide. Independent mixing gives
+
+    p=lambda+(1-lambda)/q > 1/q,
+    E[s]=lambda Wm+(1-lambda)(Wm-1)=Wm-1+lambda < Wm.
+
+The exact branch costs Wm, so it violates the deficient branchwise premise.
+This is a boundary counterexample, not cheaper exact computation or free
+random control. Literal two-seed mixtures are checked below. Nonuniform
+inputs and data-dependent coins also invalidate the uniform conditional
+count and are outside the result.
+
+## Attribution and proof status
+
+Credit Jose Manuel / jmbarrancoml PR1757 for the zero-error outgoing
+transcript and weighted-partition method, Navinor PR825 for common flags,
+and ywz65 PR2507 for designated demands and disposable workspace. Classical
+successful-subset counting retains its established status. This sharp
+threshold and reversible same-terminal attainment construction were
+produced by Nick Petalas. Predecessor numbers and verifiers are not replayed.
+This is a written proof with bounded exact corroboration, not independent
+human or formal proof-kernel review.

research/bounded-error-partition-threshold/README.md

@@ -0,0 +1,100 @@
+# A sharp bounded-error threshold for rational-frame cut certificates
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped proof with exact finite corroboration.** Allowing errors
+does not evade a weighted partition certificate if simultaneous success is
+strictly greater than `1/q`, for independent uniform inputs over an alphabet
+of size `q`. Arbitrary nonlinear pointwise gates are allowed. For common-flag
+rational frames, success above this threshold still requires `s >= Wm`.
+
+The threshold is sharp. For every `q >= 2`, `W >= 2` and `m >= 1`, an
+invertible identity circuit with a prescribed swap endpoint has success
+exactly `1/q` and rank mass `Wm-1`. All frames are diagonal. An exact swap
+circuit costs `Wm` with the same terminal frames.
+
+Independent random coins preserve the obstruction when every fixed-coin
+branch has the deficient budget. Expected cost alone is different: mixing
+these two circuits gives success greater than `1/q` and expected cost less
+than `Wm`. [PROOF.md](PROOF.md) supplies the quantifiers, successful-input
+fiber argument, exact matrices and attaining gate words.
+
+This is an originally posed change of correctness model, motivated by Jose
+Manuel / jmbarrancoml's [PR1757](https://github.com/CrocSwap/integer-mult-bounds/pull/1757).
+Its zero-error results are cited, not audited or replayed. The new step is the
+successful-input fiber bound, sharp threshold and distinction between
+branchwise and expected budgets. Classical subset counting retains its credit.
+
+## Reproduce
+
+Use CPython 3.12 and the standard library, from the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/bounded-error-partition-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/bounded-error-partition-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bounded-error-partition-threshold
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bounded-error-partition-threshold --check-source-history
+```
+
+Any absolute CPython 3.12 path can replace this interpreter. The direct check
+prints `PASS_BOUNDED_ERROR_PARTITION_THRESHOLD` in a generated JSON receipt
+binding all six package files by SHA256. It writes no files and imports no
+predecessor implementations. The runner prints `PASS_REGISTERED_RESEARCH_PACKAGE`.
+
+The new finite checks enumerate 2,002 map/demand cases and 111,744 vertex
+classes across the declared binary and ternary topologies. They include
+nonlinear ternary maps and count their actual successful-input fibers. They execute both attaining words,
+charge every physical edge and test randomized mixtures by literal seed/input
+enumeration. The 48 framed fixtures execute 1,668 input tuples. Literal random
+mixtures execute another 1,668 seed/input cases. Ten invalid-contract controls
+reject and five boundary controls pass. Exact counts appear in the generated
+receipt. The universal result rests on the written proof, not these finite checks.
+
+## Limits and relation to the frontier
+
+This error-tolerance obstruction is a changed scope under `bit-new-register-model`,
+not a new supplier, kappa or multiplication theorem. An error allowance below
+`1-1/q` alone cannot open a partition-excluded mechanism. Fixed topology,
+independent uniform inputs, distinct designated sinks and complete wire charging
+remain essential. Input-dependent topology and uncharged data-dependent advice
+are excluded. Coins are independent of inputs. The theorem concerns simultaneous
+exact symbol recovery, not numerical distance or individual receiver error.
+
+An arbitrary rational rank metric need not admit a sufficient partition
+certificate. Non-common-flag geometry is not universally excluded. Nonuniform
+inputs, physical realization, native tariffs, dirty ownership, precision/tape,
+stock, compiler and analytic recovery need separate work. No selected cold
+replay, native replay or proof-kernel build was run. Independent human and
+formal proof-kernel review are unclaimed. Selected PR6030 is unchanged.
+
+## Open next questions
+
+- For a named producer's actual nonuniform distribution, what is the maximum
+  mass of a successful transcript fiber? Start with that distribution and one
+  deficient cut. A justified distribution and its acquisition costs are missing.
+- Can a proposed approximate supplier provide a useful partition certificate
+  and simultaneous symbol-success contract? First extract its complete graph,
+  endpoints and all wires. Numerical error and physical recovery remain separate.
+
+Structured questions and the stopping decision are in [TASK.json](TASK.json).
+The work stops at this first verified threshold result.
+
+## Sources and verification bounds
+
+Base main is `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision eight.
+[SOURCES.json](SOURCES.json) pins predecessor statements as provenance, with no
+runtime scientific dependencies. Credit Navinor / PR825 for common flags,
+Jose Manuel / PR1757 for outgoing transcripts and weighted partitions, and
+ywz65 / PR2507 for designated demands and disposable workspace. Their retained
+finite-shear and circuit lineages remain credited. The six-frame zero-error
+theorem PR5944 and fixed-support Hurwitz success theorem address different
+boundaries and are not targets here.
+
+The verifier has fixed finite domains, explicit exceptions and functions below
+sixty lines. It has no recursion, subprocesses, network, generated code or input
+callbacks. Warning-strict normal and optimized replay supply the available
+standard-library diagnostics. Power of Ten rule three deviation: Python
+allocates integers, fractions, tuples and dictionaries during verification.
+Fixed domains bound live states to 125 input tuples and at most nine circuit
+vertices. A fixed-allocation port is outside this bounded checker. Dimensions,
+ports and tables are validated at entry.

research/bounded-error-partition-threshold/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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/nonlinear-frame-cut-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "1fae484c0dc371afb0ec0d0c9b1f781d78dbffbb",
+      "sha256": "411b78a56180e835bb97e59b9845968d84ad3fb8f5658acde684e4491b3b1c3e"
+    },
+    {
+      "path": "research/common-flag-frame-obstruction/README.md",
+      "usage": "provenance",
+      "git_blob": "fc38e760e0a88685b430479a2dc885590ecca327",
+      "sha256": "5636ffab46cf3801ac9b98ed681abbf237617f7189fa0a71aaf1883061a39cde"
+    },
+    {
+      "path": "research/common-flag-disposable-workspace/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "0db642e3dfb9c45180711a2ff40bed7eed316eb5",
+      "sha256": "5fe4e011011b59abd7e6b2004c7964655a30df000e7fb71beecb6b4435747ed5"
+    }
+  ]
+}