Mister-Meeseeks · Oct 22, 2026 · Oct 22, 2026 · Oct 22, 2026
diff --git a/research/fixed-word-gauge-limits/MANIFEST.json b/research/fixed-word-gauge-limits/MANIFEST.json
@@ -0,0 +1,58 @@
+{
+  "files": {
+    "NOTICE.md": "a0f77933aef1f5e9301ae171ef03371fd59fcc67f4f2fecdfd85b6b4562453d6",
+    "PROOF.md": "d38d5c8c7565f4baa3ba66e84389cfd30bf14d1f9ec057773b47e03c8e8558d5",
+    "PROVENANCE.md": "9c44733b62b349ed5f7007a073593ce87a08edbd52a74b253a2dbe157aae6108",
+    "README.md": "4dc6f4b3a1d3d2e5bfeef55b91190dcc6574bcac15ea1392a49b908f4209d044",
+    "RELATED-WORK.md": "38f8d26789e22d017b4accd4df302c9f485e0fbc622fe864438e4aa3e671bcca",
+    "SOURCES.json": "d094cdf81582cc4e95dad10887c8f29684f779f18f4d6eb22c637bdcd19329ba",
+    "VALIDATION.md": "1386abfaf8353ae6c4579dc6914fd8b5ae8486a906d1e96fb68be81a3dcdef66",
+    "certificates/THRESHOLD-GAUGE-COMMON.json.gz": "1e37dfee90763660ee04edb74ea8814a84846c5912f299ff1cbc26cdf6823c22",
+    "certificates/THRESHOLD-MULTI-GAUGE-128-256.json.gz": "960f3f80a7119d5c99c7782160c0d1d27bcb05ce3fd29f2b5fd769b87a99efc6",
+    "certificates/THRESHOLD-MULTI-GAUGE-CENTRE415.json.gz": "1e7b2a8ba177d0ed27a6138f0edd43472e3c91d71e187b7b60ce8e1a2c1b0fd2",
+    "certificates/THRESHOLD-MULTISTATE-GAUGE-128-256.json.gz": "acf975c6971df8eb1d54e4d5c6c6883842f3ad1f450b1ef68ff5aaeaae2f210c",
+    "certificates/WIRE-GAUGE-LINE42-PATHS.json.gz": "5362b6644eef8a00c8135432f877348be44a37be737a521f68be1b7ae2ce5284",
+    "certificates/WIRE-GAUGE-ODD-PATHS.json.gz": "8887f80c4446738e859f2a8355922e84c3bc7a0f7072a0d8deddd48364fdae84",
+    "certificates/WIRE-GAUGE-PAIRED-COMMON.json.gz": "8be93c23f0a71339c825fdf2a2893e3c0b2b3c880c7c5d044cb93c0a9b174a2c",
+    "checkers/check_common_product_rank.py": "d41c401b9a3ca0670d1b117dbc5dc6c9036fab7a57700359affa9a4e6a9c84e6",
+    "checkers/check_line_paths.py": "06b9589a76b6b84e3ab628bfe940cd07a90fd363aa6ba462d314eb13402cec63",
+    "checkers/gauge_negative_controls.py": "c07cf9789a314abfaf8cbfb5a4440005e7ed4fd6cba1796e0a496fa84f791a8a",
+    "checkers/review_compound_gauge.py": "9e2d216f15081dd655685da6f4bbb0a116db2a6e2557c649f4dc1af889ed83df",
+    "checkers/review_four_state_gauge.py": "403f53c6ae128e6ea6fe50b41560e2c990f899889b0579b22bee85f48769b530",
+    "checkers/review_threshold_certificate.py": "bb1786e568ccda265825add83b4f06322ad7f5ed60d0a8147c90f4c26b275e7c",
+    "checkers/review_wire_gauge.py": "1cce6ddeabd60f52e9ebafb02e2db4d289e68cdf5baaa106ca2397bf9cf7241a",
+    "checkers/verify_odd_paths.py": "a7aad7ee518b12683eba62aa451fa1b946c7a1e31553a38e999074dba6a5fd8d",
+    "data/CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219",
+    "data/LOCAL-PROGRAMS.json.gz": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a",
+    "evidence/historical/ALL-LINE-PATH-REVIEW.json": "9beb0c253e6db68a47fc6eb8db4e1930f17e3f43ab1e9beee508090fb8169284",
+    "evidence/historical/COMMON-PRODUCT-RANK-REVIEW.json": "46f400fd6e94c4809b498cfdc563ac98d8363f5119f036d155bc5d4228525b32",
+    "evidence/historical/GAUGE-NEGATIVE-CONTROLS.json": "ce4c1b1d730a2557c7232f01eb959a689e237565ffaa65becc253f29974fa01e",
+    "evidence/historical/THRESHOLD-GAUGE-COMMON-REVIEW.json": "c9a335512412fba7ca8b15d0960b8a10e5e7722960527fe778bc9fe478d86636",
+    "evidence/historical/THRESHOLD-MULTI-GAUGE-128-256-REVIEW.json": "6aa8a784bd6814ea333ebb67673cecdeb51244b14de928ad6110d5d1e3b4c91c",
+    "evidence/historical/THRESHOLD-MULTI-GAUGE-CENTRE415-REVIEW.json": "33ef8dfa5b6b77456b030708225322f2b55311674117bdd34a3b636840fb76d7",
+    "evidence/historical/THRESHOLD-MULTISTATE-GAUGE-128-256-REVIEW.json": "9b00098d9f17a856df5de02ba4debb5eb5bfc2e6eef0370954867fa2f562f13e",
+    "evidence/historical/WIRE-GAUGE-PAIRED-COMMON-REVIEW.json": "e75b3c088e17ae9443f6651d1253a78e0e5c4c34a36241f5719dc199899cc8da",
+    "evidence/replay/REPLAY.json": "7f81d82c4ac340296a567eb379de0464ab617f69fb91dae3f71c8d23752ef8b9",
+    "evidence/replay/all-lines-pairing.json": "c493174b5f29b19003618ca022fb87566df71d99681528eb491fc80ba23fca08",
+    "evidence/replay/all-lines-span.json": "eeae7231add00963a57f6f8708c7ff6f59de2e3b5134bc465d23b0ab6df23b62",
+    "evidence/replay/common-product-rank.json": "bbac61ccba8a6d8094f14b5bf3c379a85b9969d7c5a9b311db1042b15817ecd8",
+    "evidence/replay/common-rank.json": "001917257546807ea4d031c547b6221b23da12e50a2dba4ae6739e060e155923",
+    "evidence/replay/common-thresholds.json": "c9a335512412fba7ca8b15d0960b8a10e5e7722960527fe778bc9fe478d86636",
+    "evidence/replay/four-state-thresholds.json": "9b00098d9f17a856df5de02ba4debb5eb5bfc2e6eef0370954867fa2f562f13e",
+    "evidence/replay/frame415-thresholds.json": "33ef8dfa5b6b77456b030708225322f2b55311674117bdd34a3b636840fb76d7",
+    "evidence/replay/negative-controls.json": "ce4c1b1d730a2557c7232f01eb959a689e237565ffaa65becc253f29974fa01e",
+    "evidence/replay/product-thresholds.json": "6aa8a784bd6814ea333ebb67673cecdeb51244b14de928ad6110d5d1e3b4c91c",
+    "notices/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4",
+    "notices/research/gauge44-slots-t16/NOTICE.md": "7a8d17b04da1e6c9d0ec217fb5bda72faa09d9a21695128722dd1e2827870fcf",
+    "notices/research/gauge44-slots-t16/UPSTREAM-NOTICE.md": "a75967ebc34e3bf2ff2c25c08e6c7f1a61b0c0d171cfd1b62196ae2caaf2c610",
+    "notices/research/gauge44-slots-t16/construction/NOTICE.md": "defe7e44af610e25a6c50c1c3b2efd0972d0690574995c0c872fc50eebf4c816",
+    "notices/research/gauge44-slots-t16/construction/UPSTREAM-NOTICE.md": "a75967ebc34e3bf2ff2c25c08e6c7f1a61b0c0d171cfd1b62196ae2caaf2c610",
+    "notices/research/gauge44-slots-t16/t16/NOTICE.md": "902370e6bfcd39dbea2ece474f15fccbcce3b8e966b2b94066bd03e5174591b5",
+    "proofs/ALL-LINE-GAUGES.md": "006d8882d3865e2dea88840b62a0b792d7d2ff11bd0bb6b7fd26c9756fe842cb",
+    "proofs/BOUNDARY-GAUGE.md": "0ead988c25cc52ac64d7396761e143312de617e78381ba3fd96b97256b55d44c",
+    "proofs/COMMON-PRODUCT-RANK.md": "5db8a5730b70f61acd499712e909e952b1951fc3263aeeb11e07b573cf528599",
+    "proofs/GAUGE-REVIEW.md": "064d331bf5f4bbc6c9f4b33bd9dd279b3f456248b91a6f5e91855e290d9f1d7c",
+    "replay.py": "1120f28ea69263b74e5932aec64bc7f78ad18fb5912b73bcb416132ac1826eab"
+  },
+  "format": "sha256-package-files-v1"
+}
diff --git a/research/fixed-word-gauge-limits/NOTICE.md b/research/fixed-word-gauge-limits/NOTICE.md
@@ -0,0 +1,39 @@
+# Attribution and license
+
+New proof, certificate, review, and packaging work in this package was
+prepared with substantial OpenAI Codex assistance in the centre-encoding
+campaign. The source-domain lane supplied the gauge certificates and the
+all-line and common-product arguments. The temporal-reuse lane supplied
+separate source, graph, flow, rigidity, and threshold checks. The
+encoded-controller review lane supplied a separate graph construction,
+symplectic pairing checks, and common-product proof review. These are
+separate AI-agent checks, not independent human peer review.
+
+The exact local scalar word and frame data are inherited from the gauge44
+and T16 lineage at historical commit
+`bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. This package preserves these
+source notices without changes:
+
+- [Gauge44 notice](notices/research/gauge44-slots-t16/NOTICE.md).
+- [Construction notice](notices/research/gauge44-slots-t16/construction/NOTICE.md).
+- [T16 integration notice](notices/research/gauge44-slots-t16/t16/NOTICE.md).
+- [Complete upstream notice](notices/research/gauge44-slots-t16/UPSTREAM-NOTICE.md).
+
+The T16 notice credits Jeremy Kothe's accepted
+[PR #799](https://github.com/CrocSwap/integer-mult-bounds/pull/799) local
+word, Chafik Boukhalfa's
+[PR #741](https://github.com/CrocSwap/integer-mult-bounds/pull/741) frames,
+and the preceding supplier and owner construction. It credits Hao Yan
+for T16 integration. The retained notices credit icekylinx for the source
+gauge and supplier pipeline, DreamingOfClouds and other contributors for
+the earlier source lineage. Those constructions are consumed predecessors;
+they are not new results of this package.
+
+The packaged source members are unchanged. Checker edits replace local
+Git and campaign paths with package-relative inputs and explicit external
+output paths. `SOURCES.json` records each original hash and adapted hash.
+The mathematical checks are retained. The present proof combines only the
+reviewed claims; the frozen notes retain their original scope statements.
+
+Apache-2.0 applies to this package. The [license](notices/LICENSE) and
+all retained attribution remain applicable.
diff --git a/research/fixed-word-gauge-limits/PROOF.md b/research/fixed-word-gauge-limits/PROOF.md
@@ -0,0 +1,287 @@
+# Fixed-word gauge theorem and its limits
+
+All finite graph claims in this proof use the two source members in
+`data/`, from historical commit
+`bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. The complete scalar program and
+all native event positions remain fixed. A gauge is an invertible operator
+on the full array. Native rank means the binary relative-frame rank used
+by this source. This proof gives no new kappa value.
+
+## 1. Exact boundary condition
+
+Write the physical value on wire segment `v` as `T_v z_v`. Replace its
+frame by `T_v G_v`. Use the same `G_v` for both live values of each scalar
+ADD or COPY. A CLEAR starts a new zero value and gives no relation to the
+old target gauge. Replace a native transition from `u` to `v` by
+
+```text
+T_v G_v G_u^-1 T_u^-1.
+```
+
+The scalar coefficients commute with these operators. Induction over the
+program gives the new physical endpoint
+
+```text
+diag(T_out) diag(G_out) P diag(G_in)^-1 diag(T_in)^-1,
+```
+
+where `P` is the old scalar endpoint. The outer frames are invertible.
+Thus the endpoint equals the old physical endpoint if and only if
+
+```text
+diag(G_out) P = P diag(G_in).
+```
+
+No commutation of a gauge with an old frame is assumed. This identity
+includes global phases and holds for the full operators at every tensor
+power.
+
+Exact rational replay on all 712 input columns gives
+
+```text
+forward:  (x,y,h,c) -> (x,y+x,h,0)
+backward: (x,y,h,c) -> (x-y,y,h,0).
+```
+
+There are 112 rows in each data bank, 480 arbitrary helpers, and eight
+private values. The three nonzero blocks for each data pair force one
+gauge at its four boundary points. Each helper forces one gauge at its
+input and output. The private rows and columns of `P` are zero. They give
+no boundary relation. The actual scalar accesses still give relations.
+The full residual on a helper remains
+`T_out G (T_in G)^-1 = T_out T_in^-1`.
+
+## 2. Source graph and rank rule
+
+Split each wire at every native event. Join only scalar ADD/COPY operands
+and the boundary pairs from Section 1. The source gives 5,784 segments,
+1,979 components, and 5,064 native events. Eight components are final
+cleared private values with no native event. The other 1,971 components
+meet native events. There is no fixed external gauge.
+
+The native profile, including rank zero, is
+
+```text
+{0:1570, 1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}.
+```
+
+Its rank mass is 5,586. The events are 3,486 climbs, eight centres, 1,090
+adapters, and 480 residual adapters. Thus a change at an old rank-zero
+wrapper is charged.
+
+For a frame subspace `U` in `F_2^9`, its inverse-image diagonal Pauli space is
+
+```text
+L_U = {(u,u+v): u in U, v in U-perp}.
+```
+
+It is a nine-dimensional Lagrangian. Two such labels have relative rank
+`dim(L_U + L_V)-9`. Equivalently, the rank is the rank of their 9 by 9
+symplectic pairing matrix. The two independent checkers use these two
+formulas. Both check each old source rank. Left monomial wrappers preserve
+this label.
+
+A translation-line gauge has binary action
+
+```text
+S_a(x,z) = (x+a(a dot z),z).
+```
+
+This is a symplectic involution. Therefore a binary crossing has the same
+rank at either end of an edge. Equal gauge bits leave the rank unchanged.
+This statement is about ranks; Section 1 gives the separate exact endpoint
+condition.
+
+The forward and backward scalar partitions and undirected native graphs
+are isomorphic. In backward coordinates the frame is `D_U=T_U F^-1`.
+The line gauges commute with `F`, so the same line gauges have the same
+ranks in both orientations. A general forward gauge `G` instead requires
+backward gauge `F G F^-1` for this correspondence.
+
+## 3. All 511 fixed lines
+
+Fix one nonzero line vector `a` for the whole word. Each component may
+choose `I` or `C_a`. The line cannot vary between components. After each
+native event is priced, combine parallel edges. The rank change is
+
+```text
+E(epsilon) = sum_e w_e [epsilon_u != epsilon_v].
+```
+
+For each odd line, the exact certificates route every negative demand
+`d=-w_(u,v)` from `u` to `v` through positive edges. Route amounts are
+positive integers. They cover every demand exactly and use no positive
+edge beyond its capacity. If a cut separates the endpoints, each route
+crosses that cut at least once. Sum this inequality over the routes.
+The capacity condition gives `E(epsilon)>=0` for every cut. A constant
+assignment attains zero.
+
+The two path certificates cover all 256 odd lines exactly once. They
+contain 10,488 paths. The independent pairing checker verifies all
+1,609,650 distinct-pair ranks over all 511 nonzero lines. The separate
+span checker also verifies the full line family. For each of the 255 even
+lines, every changed native edge has rank at least its old rank. Thus an
+even line also cannot reduce any sum of nondecreasing native rank costs.
+
+For the odd lines outside the common family below, the total-rank theorem
+does not settle all child moments or the profiles of all zero-rank cuts.
+
+## 4. Common lines and concave costs
+
+The common intersection of the eight centre frames has basis
+
+```text
+30, 45, 75, 128, 256.
+```
+
+Its 16 odd vectors are
+
+```text
+128,158,173,179,203,213,230,248,
+256,286,301,307,331,341,358,376.
+```
+
+For each line, an exact signed-cut certificate has minimum rank change
+zero. If at least one centre edge is crossed, the minimum is 13. The
+latter means at least one centre, not all eight centres simultaneously.
+There are 3,384 exact flow/cut cases across these tests.
+
+Here is the finite certificate argument. Choose a vertex cover of the
+negative edges and enumerate every assignment to it. All remaining edges
+between free vertices have nonnegative weights. A fixed/free edge gives
+a unary cost. Subtract the smaller unary value into a constant and use
+the difference as a source or sink capacity. Every case supplies an
+integer feasible flow and a cut of equal value. Capacity, conservation,
+branch coverage, cut value, and the original signed objective are checked
+exactly. Their equality proves that branch's minimum. Enumeration proves
+the global minimum.
+
+Only the constant cover branches reach zero. In each such branch,
+residual source or sink reachability forces every free native component
+to the same side as the cover. Thus every rank-zero cut is constant on
+all 1,971 native components. The eight isolated cleared values may vary.
+The full native profile is unchanged at equality.
+
+The separate capped-cost certificate proves minimum zero for
+`f_k(r)=min(r,k)`, for `k=1,...,8`, on all 16 lines. It has 800 exact
+flow/cut cases. All ranks in this family lie between zero and eight.
+For `f(0)=0`, set `d_j=f(j)-f(j-1)`. If
+`d_1 >= ... >= d_8 >= 0`, then
+
+```text
+f(r) = d_8 min(r,8)
+       + sum_(k=1)^7 (d_k-d_(k+1)) min(r,k).
+```
+
+All coefficients are nonnegative. Hence every increasing concave rank
+cost is nondecreasing. This includes `sum r^(1-b)` for `0<=b<1`. At `b=1`,
+use zero at rank zero and one at every positive rank. That is the paid
+child count `min(r,1)`.
+
+## 5. Common products and the four-state family
+
+For the binary family `I,G` with `G=C_128 C_256`, the changed edge ranks
+are computed directly from the two commuting transvections. The exact
+rank minimum is zero, and all rank-zero cuts have the same rigidity.
+Capped-cost certificates through cap nine give minimum zero. The
+nonnegative decomposition in Section 4 therefore applies through rank
+nine.
+
+For the four states `I,C_128,C_256,C_128 C_256`, every native rank table
+depends only on the XOR of the endpoint states. The exact rank objective
+has a pointwise lower bound which separates the two bits. Both signed
+lower graphs have minimum zero and the same zero-cut rigidity. A constant
+state attains zero in the true problem. Thus every zero-rank state choice
+is constant on all native components.
+
+For each cap, let `d_1,d_2,d_3` be the changes at XOR states `01,10,11`.
+Put `m=max(0,d_1+d_2-d_3)`. The weights `2d_1-m` and `2d_2-m` give a
+separable lower bound for twice the true edge cost. At states `01` and
+`10`, this follows from `m>=0`. At state `11`, it follows from
+`m>=d_1+d_2-d_3`. The check also verifies each actual table entry.
+Both signed lower graphs have minimum zero at every cap from one to nine.
+Thus the four-state family cannot reduce any increasing concave rank cost.
+The solver status and exploratory saved state are not used in this proof.
+
+## 6. Full-frame counterexample and its limited moment bound
+
+The binary family `I,T_415` has rank minimum zero and rank-zero rigidity,
+but its cap-one minimum is minus one. A cut which differs from a constant
+only at component 608 removes one rank-eight centre child. Seven incoming
+edges retain rank four; seven outgoing rank-one edges become rank nine.
+The rank change is 48, and the profile is
+
+```text
+{0:1571, 1:2405, 2:418, 3:432, 4:142, 5:82, 8:7, 9:7}.
+```
+
+The child-moment change for this cut is
+`7*9^(1-b)-7-8^(1-b)`. Thus a no-gain claim for every increasing concave
+cost on this full-frame family would be false.
+
+The exact cap minima for caps one through nine are `-1,0,0,0,0,0,0,0,0`.
+Every native rank increment is even. Rank-zero rigidity therefore makes
+every changed native cut have total-rank increase at least two. With
+`a=1-b`, the threshold decomposition gives
+
+```text
+Delta sum r^a >= 2*(9^a-8^a) - (2-2^a).
+```
+
+For `3/5<=a<=1`, the first term is greater than `24/49`, and the
+subtracted term is less than `97/200`. The exact integer checks
+`49^5>81*20^5` and `303^5<8*200^5` establish these strict bounds.
+Consequently every changed native cut has moment increase greater than
+`47/9800` for `0<=b<=2/5`. Constant native gauges retain the profile.
+
+`T_415` does not commute with `F`. This forward certificate applies to
+`F T_415 F^-1` in backward coordinates. It gives no identical-`T_415`
+claim there.
+
+## 7. Local rank bound for arbitrary common-line products
+
+Let `A subset U subset F_2^n`, let `e=dim(U)`, and let `s` be the rank of
+the standard dot product restricted to `A`. Permit arbitrary products of
+`C_a`, with `a in A`, at both ends of a native descent from `T_U` to the
+identity. Their relative binary action has the form
+
+```text
+S_B(x,z) = (x+Bz,z),   B = sum_j a_j a_j^T.
+```
+
+Here `im(B) subset A`, and `B` kills `U-perp`. An intersection point of
+`L_U` and `S_B L_0` has a unique form
+
+```text
+z=w+u,  w in U-perp,  u in U,  Bu=u.
+```
+
+A fixed vector of `B` in `U-perp` is zero. The intersection dimension is
+`n-e+dim Fix(B|U)`, so the exact relative rank is
+`e-dim Fix(B|U)`. Every fixed vector lies in `A` and in the image of
+`B|A`. The map `B|A` factors through the dot-product map on `A`, whose
+rank is `s`. Therefore
+
+```text
+native rank = e-dim Fix(B|U) >= e-s.
+```
+
+Applying a common symplectic map to both labels reduces two arbitrary
+endpoint products to their relative product. Thus the same bound holds
+with arbitrary common-line product gauges at both endpoints.
+
+For the actual common basis, the Gram rows are `0,0,0,8,16`. The Gram
+rank is two, and each centre has dimension eight. Hence each descent has
+rank at least six. Direct pairing checks show that `C_128 C_256` attains
+six at each of the eight centres. This local bound does not price the
+rest of the scalar graph or exclude a complete-cost gain.
+
+## Verification boundary
+
+The replay checks the complete finite source words, exact rank tables,
+integer path certificates, flow/cut witnesses, and 13 damage controls
+under optimized Python. It does not emit a changed physical supplier.
+The all-size compiler, hosting, precision, and analytic obligations of a
+multiplication theorem are outside this package. Its graph-specific
+conclusions do not transfer to a changed current construction without a
+new source-bound proof.