Certify minimum rank for paid connector chart repair

research/connector-chart-rank-repair/PROOF.md

@@ -0,0 +1,146 @@
+# Minimum source repair for a changed connector chart
+
+Let B0,B1:X->Z be linear maps over any field, with finite dimensions n,m.
+Let U,V be their row spaces in X*, with dimensions r0,r1 and intersection
+dimension c. A chart is an arbitrary invertible linear map R:Z->Z. The
+residual source correction is Delta=B1-R B0. Then
+
+    min_(R invertible) rank(Delta) = max(r0,r1)-c.             (1)
+
+This is a rank statement, not a minimum scalar circuit cost or a theorem
+about a restricted native chart alphabet. The familiar equal-kernel criterion
+in the credited predecessor is exactly the zero-residual case. The new
+interface permits and charges the residual when kernels differ.
+
+## Lower bound
+
+The row space of R B0 is U. Modulo V, its rows equal the negatives of the
+rows of Delta; therefore the image of row(Delta) in X*/V contains the image
+of U, which has dimension r0-c. Likewise modulo U the rows of Delta project
+onto the image of V, of dimension r1-c. Hence rank(Delta) is at least both
+r0-c and r1-c, proving the lower bound in (1).
+
+This does not merely count unequal ranks. Two equal-rank maps can have
+different row spaces and a positive minimum. For example the two rank-one
+functionals x0 and x1 need one independent correction.
+
+## Attaining chart
+
+Choose a basis S of U intersect V, extend it by A to a basis of U, and by B
+to a basis of V. The union S,A,B is independent: a relation between A and B
+would put their common combination in U intersect V, contradicting either
+extension. Choose invertible row-operation matrices Q0,Q1 taking B0,B1 to
+
+    Q0 B0 = [S; A; 0],          Q1 B1 = [S; B; 0].
+
+Their common S rows occupy the first c positions; pair the exclusive rows in
+the following positions, padding the shorter list with zeros. Set
+R=Q1^-1 Q0. Then
+
+    Q1 Delta = [0; B-A; unmatched rows; 0].
+
+There are max(r0-c,r1-c) nonzero rows and they are independent by the
+independence of S,A,B. Since Q1 is invertible, Delta attains (1). The same
+argument covers zero maps, zero source dimension, full rank and unequal ranks.
+It uses no generic-position, infinite-field or characteristic assumption.
+
+The binary constructor implements this argument by tracked elimination. It
+extracts the common row basis from relations among independent bases of U,V,
+extends that basis in each row space, solves for its preimages in the original
+rows and appends the full relation basis. These preimages plus the relation
+basis form the invertible Q matrices. The finite oracle independently forms
+actual GL3 orbits rather than trusting the constructed R.
+
+More generally, consider any finite internal transport composed only of
+invertible charts and additive source injections C_j x, with no intervening
+output observation or source mutation. Its endpoint has the form R z+E x;
+E is a sum of invertibly transported C_j. Thus rank(E)<=sum rank(C_j).
+If it carries B0 x to B1 x, E=B1-R B0, so the same quantity in (1) lower-bounds
+the **total injected rank**. One residual injection attains it. This statement
+does not price the charts or the implementation of an injection.
+
+## Dirty endpoint and compulsory restoration
+
+Let x,z,y0,y1 be distinct arbitrary input rows, x immutable. A0,A1 are fixed
+linear readers and can be singular, noncommuting and different. Complete
+queries preserve every other row, private scratch and required head positions;
+their increment is independent of the old target. Reserve z throughout.
+For general characteristic execute, chronologically:
+
+    y0 -= A0 z
+    z  += B0 x
+    y0 += A0 z          # first output delivered; never changed again
+    z   = R z
+    z  += Delta x      # one paid source correction
+    y1 += A1 z
+    z  -= B1 x
+    y1 -= A1 z          # second output delivered
+    z   = R^-1 z
+
+After the first delivery z=z_initial+B0 x. Chart plus correction makes it
+R z_initial+B1 x. The second read/close/read adds A1 B1 x to y1 and leaves
+z=R z_initial. The final inverse restores z exactly. Thus both outputs receive
+their desired increments and all source/connector dirt restores. Nothing
+requires R to fix the initial dirt. The source correction is cancelled by
+the actual B1 close; it is not an unpaid obligation deferred to a consumer.
+Reversing the word and inverting each complete operation gives its inverse.
+
+## Complete comparison and what rank does not buy
+
+For sign-symmetric complete query prices, or upper bounds valid in either
+orientation, the two separately closed echoes cost
+
+    C_closed = I0+P0+D0 + 2(c_B0+c_B1+c_A0+c_A1).
+
+The transported pair costs
+
+    C_repair = I1+P1+D1 + c_B0+c_B1+2(c_A0+c_A1)
+               + c_R+c_Rinv+c_Delta.
+
+I,P,D charge admission/layout/reservation, preparation/synthesis and remaining
+instruction/control work. Each complete c includes its real source/coefficient
+access, arithmetic, scratch restoration, routing, frame obligations and heads.
+For asymmetric signs or ports, sum the actual word prices instead. A saving
+requires
+
+    c_R+c_Rinv+c_Delta + (I1+P1+D1-I0-P0-D0) < c_B0+c_B1.
+
+A rank-r factorization Delta=UV does **not** implement U(Vx) for free.
+Its observations, intermediate storage, dirty cancellation and restoration
+must be included in c_Delta. Likewise arbitrary invertible R in (1) is a
+mathematical search domain, not a free physical gate. Rank-minimizing R can
+lose at actual tariffs; the receipt includes an explicit contrary tariff.
+
+The binary pilot uses B0=(7,6,1), B1=(1,6,5), R=(3,2,4), with bit j denoting
+column j in each row. Delta=(0,0,4), a single source-coordinate XOR into the
+third connector coordinate. The map ranks are2 and3, c=2, so this rank1 repair
+is minimal. The identity chart leaves rank2. R and R^-1 are each the one-XOR
+shear z0+=z1. With identity readers, all required source/read/chart/correction
+operations are literally emitted:26 XORs versus34 for the separately closed
+queries. There are no additional rows. The full4096 dirty states and inverses
+pass, with first-output delivery checked at its actual cut.
+
+This is a fixed-call comparison. Opening the matrices and directly updating
+the two outputs uses only11 XORs; that excluded-alphabet control is retained
+and prevents a claim of general circuit optimality. The pilot therefore
+demonstrates a complete adapter identity and price, not a practical optimizer.
+Its same scalar gates act independently on length-L coordinate blocks, giving
+26L versus34L scalar XORs; physical instruction/address costs still need a
+backend. The fixed-port one-bit tariff explicitly counts movement plus five
+units per XOR, matching the predecessor convention, without claiming a native
+Turing-machine implementation.
+
+## Revision-5 expansion decision
+
+Declared milestone: **local module**. Retain the rank criterion and restored
+adapter; narrow work to this single proof and discriminating example. General
+native chart/repair prices, selected ownership, precision and a selected caller
+remain unknown, not zero. Do not start a dependent optimization round until a
+pinned caller supplies a strict complete allowance and legal connector lifetime.
+The exact scope/boundary/cost ledger and reopening condition are in TASK.json.
+
+Credit woklerx's retained equal-kernel chart interface, Ross Richardson's PR943
+dirty-query accounting and the elementary row-space method. No priority claim
+is made for rank inequalities or change of basis. The contribution is their
+source-pinned residual-repair interface and executable evidence. Prepared by
+ywz65 with substantial OpenAI Codex assistance; Apache-2.0.

research/connector-chart-rank-repair/README.md

@@ -0,0 +1,109 @@
+# Exact rank of a paid connector chart repair
+
+The retained dirty connector chart interface can move B0 x to B1 x without
+another source observation exactly when the two maps have the same kernel.
+This package permits a **paid residual source injection** Delta x and determines
+its minimum rank:
+
+    min_(R invertible) rank(B1-R B0)
+      = max(rank B0,rank B1) - dim(row B0 intersect row B1).
+
+The theorem holds over every field, including singular and unequal-rank maps.
+A constructive change-of-basis proof supplies R and Delta. The same quantity
+lower-bounds the total injected rank of any internal sequence of invertible
+charts and additive source corrections without intermediate observations.
+It does not minimize chart cost, scalar work or a physical native tariff.
+
+This extends woklerx's [equal-kernel chart criterion](../dirty-connector-chart-transport/README.md)
+within Ross Richardson's [dirty-query model](../universal-connector-boundary/README.md).
+Their boundary contracts, cancellation and price conventions retain credit.
+The contribution is the residual-rank interface, its constructive certificate
+and the restored/charged example; no novelty claim is made for elementary
+row-space inequalities or change of basis.
+
+## Complete dirty-state example
+
+Read matrix rows as binary masks:
+
+    B0=(7,6,1), B1=(1,6,5), R=(3,2,4), Delta=(0,0,4).
+
+The paid chart is z0+=z1 and its inverse is the same shear. The correction
+is one XOR from source coordinate2 into connector coordinate2. It has rank1,
+the proved minimum; the identity chart would leave rank2. Four distinct
+three-bit rows x,z,y0,y1 are all arbitrary. Every source, chart, readout,
+correction and final inverse is emitted explicitly; no extra row is needed.
+
+| Fixed one-bit implementation | XORs | Reads | Writes | Head moves | Declared tariff |
+|---|---:|---:|---:|---:|---:|
+| Two closed queries |34|68|34|444|614|
+| Repaired chart pair |26|52|26|368|498|
+| Direct matrices, outside this query alphabet |11|22|11|204|259|
+
+The tariff puts the12 bits at consecutive positions, starts/returns the data
+head one cell before bit0, and charges `2*(max(source,target)+1)+5` for each
+scalar XOR. Its five units are two reads, one write, XOR and dispatch. This
+declared interpreter tariff is not a native tape-compiler certificate.
+The11-gate direct control is deliberately retained:26 is **not** a minimum
+over arbitrary circuits. No selected caller is claimed to need this alphabet.
+
+The first output is delivered before the chart change and never rewritten.
+After the paid correction the connector is R z_initial+B1 x. The second
+read/close/read cancels the charted dirt, and the final R inverse restores the
+actual connector. The source correction is cancelled by the closing B1 call;
+it is not deferred to a later consumer. [PROOF.md](PROOF.md) gives the exact
+word over general characteristic and the full comparison, including admission,
+preparation, instruction work and complete prices of all child operations.
+
+## Reproduce
+
+```sh
+python3.12 scripts/research_package.py --package research/connector-chart-rank-repair
+python -I -O -B research/connector-chart-rank-repair/verify.py
+```
+
+The external finite oracle enumerates all168 GL3 charts and their complete
+orbits, then checks every262,144 pair of binary3-by-3 maps. It agrees with the
+formula's minimum-rank histogram `0:40916, 1:187376, 2:33516, 3:336`.
+The independent constructive method emits8,192 charts across all16 row-space
+classes and512 destinations. No predecessor executable is imported.
+
+All4,096 dirty pilot inputs, literal inverses and first-output cuts pass.
+Four altered programs fail semantically. A separate ordinary-matrix control
+over F3 checks6,561 arbitrary dirty banks and inverses with noncommuting
+readers, and rejects the wrong closing sign. Zero maps, unequal ranks,
+equal-rank unequal kernels and an adverse chart tariff are explicit controls.
+Four export groups cover Git-free read-only replay, source drift, typed/duplicate
+receipt corruption and exclusive regeneration.
+
+Native CPython3.12.7 registered checks and optimized3.14.5 primary replay pass.
+A separate OpenAI Codex agent checked the proof and independently minimized
+4,454 smaller binary map pairs plus all168 charts for the pilot. Evidence is
+finite where described; the all-field theorem relies on the written proof,
+not on extrapolation from the finite checks. No human or formal-kernel review
+or hosted CI result is claimed.
+
+## Expansion decision and limits
+
+Milestone: **local module**. The initial revision4 assignment was preserved
+when main advanced to revision5 (`b4560d9e7216f72b73c5aa940ac099c05e33ccf9`).
+The new family gate was read and the checkout fast-forwarded before packaging;
+scientific predecessor blobs were unchanged. TASK.json contains the five-point
+boundary/obligation ledger and the decision to **narrow** to this proof.
+
+A small rank is not a free observation or a cheap circuit. The general native
+cost of R, R inverse and Delta, dynamic synthesis, selected ownership, precision
+and an actual selected consumer remain unknown. Unknowns are not zero. The
+complete improvement condition is that chart, inverse, correction and changed
+admission/preparation/control cost less than the removed B0 and B1 calls.
+No supplier, recursive contraction, selected-result change or new kappa follows.
+Do not expand the family without a concrete consumer and that strict allowance.
+
+## Open next questions
+
+1. Find a pinned caller with this legal connector lifetime, actual source maps
+   and a favorable complete native repair invoice. Hosting and precision must
+   be included before using this module in a supplier.
+2. For that caller only, optimize within its legal chart alphabet and actual
+   prices. The unrestricted rank optimum may be unavailable or more expensive.
+
+Prepared by ywz65 with substantial OpenAI Codex assistance. Apache-2.0.