Prove the sharp tariff for paid UT3 central calls

research/ut3-priced-central-calls/CERTIFICATE.json

@@ -0,0 +1,116 @@
+{
+  "status": "PASS_UT3_PRICED_CENTRAL",
+  "fixtures": [
+    {
+      "k": 1,
+      "r": 3,
+      "central_calls": 0,
+      "a_calls": 2,
+      "b_calls": 2
+    },
+    {
+      "k": 1,
+      "r": 3,
+      "central_calls": 1,
+      "a_calls": 0,
+      "b_calls": 0
+    },
+    {
+      "k": 2,
+      "r": 4,
+      "central_calls": 0,
+      "a_calls": 4,
+      "b_calls": 4
+    },
+    {
+      "k": 2,
+      "r": 4,
+      "central_calls": 1,
+      "a_calls": 2,
+      "b_calls": 2
+    },
+    {
+      "k": 2,
+      "r": 4,
+      "central_calls": 2,
+      "a_calls": 0,
+      "b_calls": 0
+    },
+    {
+      "k": 3,
+      "r": 5,
+      "central_calls": 0,
+      "a_calls": 6,
+      "b_calls": 6
+    },
+    {
+      "k": 3,
+      "r": 5,
+      "central_calls": 1,
+      "a_calls": 4,
+      "b_calls": 4
+    },
+    {
+      "k": 3,
+      "r": 5,
+      "central_calls": 2,
+      "a_calls": 2,
+      "b_calls": 2
+    },
+    {
+      "k": 3,
+      "r": 5,
+      "central_calls": 3,
+      "a_calls": 0,
+      "b_calls": 0
+    },
+    {
+      "k": 4,
+      "r": 6,
+      "central_calls": 0,
+      "a_calls": 8,
+      "b_calls": 8
+    },
+    {
+      "k": 4,
+      "r": 6,
+      "central_calls": 1,
+      "a_calls": 6,
+      "b_calls": 6
+    },
+    {
+      "k": 4,
+      "r": 6,
+      "central_calls": 2,
+      "a_calls": 4,
+      "b_calls": 4
+    },
+    {
+      "k": 4,
+      "r": 6,
+      "central_calls": 3,
+      "a_calls": 2,
+      "b_calls": 2
+    },
+    {
+      "k": 4,
+      "r": 6,
+      "central_calls": 4,
+      "a_calls": 0,
+      "b_calls": 0
+    }
+  ],
+  "omission_controls": 100,
+  "tariff_checks": 2102,
+  "representation_products": 64,
+  "sharp_cost": "k*min(2*(alpha+beta),gamma)",
+  "not_run": [
+    "physical call implementation",
+    "supplier admission",
+    "all-size compiler",
+    "hosting",
+    "precision/tape",
+    "outer assembly"
+  ],
+  "new_kappa": false
+}

research/ut3-priced-central-calls/PR1573-README.md

@@ -0,0 +1,214 @@
+# A sharp commutator call bound with arbitrary restored dirty workspace
+
+**Scoped theorem; no new kappa.** In the formal `F2[UT_3(F2)]` register
+model of [PR1478](https://github.com/CrocSwap/integer-mult-bounds/pull/1478),
+`k` central commutator targets require at least **2k calls of each generator**,
+hence exactly **4k paid calls**, for every finite register count `r >= k >= 1`.
+Any number of additional arbitrary dirty registers, restored at the endpoint,
+cannot save calls. The direct construction attains both separate bounds.
+
+PR1443 by @woklerx established the two-register D8 case; PR1478 by @juper997
+established the eight-call minimum for two targets on exactly two or three
+registers by a finite exhaustive census. Its explicit
+open question was whether the restriction on workspace could be removed.
+The proof below removes that restriction and handles any target count. It
+uses two small representations and a rank inequality, with no census of
+register words or extrapolation from tests. Credit for the model, earlier
+finite result and question remains with PR1478 and its predecessors.
+
+The final overlap refresh found Arham Tahir's concurrent
+[Discussion1569](https://github.com/CrocSwap/integer-mult-bounds/discussions/1569),
+claiming the **two-target, arbitrary-register** case by a degree-two quotient
+and separate label parity. This package's additional scope is **every target
+count k**, with separate `2k` lower bounds for each label and the resulting
+weighted tariff. It also supplies independently implemented exact witnesses
+and failure controls. No priority is claimed for the overlapping two-target
+case, and the concurrent claim is not used as an established premise.
+
+## Exact model and bill
+
+Let `G = UT_3(F2)` with elements `(x,y,z)` representing entries `01,12,02`.
+Multiplication is
+
+`(x,y,z)(X,Y,Z) = (x+X, y+Y, z+Z+xY)`.
+
+Write `a = I+E01`, `b = I+E12`, and `c = abab = I+E02`. The group has eight
+elements; `a,b,c` are involutions and `c` is central. Work over the **formal
+group algebra** `R = F2[G]`, not only its natural three-dimensional image.
+There are `r` scalar registers with arbitrary inputs. An allowed paid factor is
+
+`D_N(g) = I_r + ([g]+1) N`,
+
+where `g` is `a` or `b`, and `N = u v^T` is a binary rank-one idempotent:
+`v^T u = 1`. Each occurrence costs one. Arbitrary scalar `GL_r(F2)` maps are
+free. No other address operation, higher-rank paid call, clean allocation,
+COPY, ERASE or free undo is admitted. The exact endpoint is
+
+`T = diag([c], ..., [c], 1, ..., 1) = I_r + ([c]+1) P`,
+
+where `P = diag(I_k,0)` has rank `k`. The last `r-k` roles are restored as
+operators on **all** inputs, not merely initialized to zero. The same result
+holds for a scalar conjugate of this endpoint, by changing the register basis.
+
+As in the predecessor's augmentation argument, interleaved free scalar maps
+can be moved to one end by conjugating each `N`. Augmentation `[g] -> 1`
+sends every paid factor and `T` to `I_r`, so that remaining scalar map is
+`I_r`. Every conjugate of a rank-one idempotent is again an allowed projector.
+It therefore suffices to consider a product of the displayed paid factors.
+
+The complete attaining word applies `(a,b,a,b)` to each of the first `k`
+coordinate projectors. On that coordinate the product is `[abab]=[c]`;
+on every other coordinate it is identity. It uses `2k` a-calls and `2k`
+b-calls, exactly `k` data roles and `r-k` unused/restored dirty roles, with
+no scalar mixing, source-access operation, copy or restoration outside those
+`4k` calls. This is an abstract paid-call bill. It does not price an
+implementation of these calls in the selected multiplication supplier.
+
+## Proof for all register counts
+
+All ranks and spans in this proof are over `F2`. Products are written in
+left-to-right matrix order. Let `n_a,n_b` count the occurrences of the two
+labels. For each label collect its column factors `u_j` as columns of `X_a`
+or `X_b`, and its row factors `v_j^T` as rows of `Y_a` or `Y_b`. In particular,
+
+`sum_{a calls} N_j = X_a Y_a`, and similarly for `b`.
+
+**First representation.** Apply the natural representation of `G` entrywise
+to the formal register matrix, and reorder coordinates into three address
+blocks of size `r`. The two paid factors become
+
+```text
+a: [ I  N  0 ]       b: [ I  0  0 ]
+   [ 0  I  0 ]          [ 0  I  N ]
+   [ 0  0  I ]          [ 0  0  I ].
+```
+
+Multiplying them gives diagonal blocks `I`, blocks `01` and `12` equal to
+the respective projector sums, and block `02` equal to
+
+`C_ab = sum_{i<j, g_i=a, g_j=b} N_i N_j`.
+
+There are no terms of higher degree because the strictly upper-triangular
+address matrices have only the path `0 -> 1 -> 2`. The exact formal target
+therefore implies
+
+`X_a Y_a = 0`, `X_b Y_b = 0`, and `C_ab = P`.
+
+Each summand `N_i N_j = u_i (v_i^T u_j) v_j^T` has its column space in
+`im X_a` and its row space in `row Y_b`. Consequently
+
+`rank X_a >= k`, `rank Y_b >= k`.
+
+**Second representation.** The map
+
+`sigma(x,y,z) = (y,x,z+xy)`
+
+is a group automorphism: substitution into the displayed group law verifies
+multiplicativity, and `sigma^2` is identity. It swaps `a` and `b` and fixes
+`c`. (Simply swapping `x,y` without the `xy` correction is not this map.)
+Compose the natural representation with `sigma`. The same endpoint now
+forces
+
+`C_ba = sum_{i<j, g_i=b, g_j=a} N_i N_j = P`.
+
+Its column space is contained in `im X_b` and its row space in `row Y_a`, so
+
+`rank X_b >= k`, `rank Y_a >= k`.
+
+**Dimension bound.** Since `X_a Y_a = 0`, the image of
+`Y_a : F2^r -> F2^{n_a}` lies inside the kernel of
+`X_a : F2^{n_a} -> F2^r`. Rank-nullity gives
+
+`rank X_a + rank Y_a <= n_a`.
+
+Both terms are at least `k`, so `n_a >= 2k`. Applying the same argument to
+`b` gives `n_b >= 2k`. The direct word attains equality in both bounds.
+This proves the stated minimum for every `r >= k`, without an upper bound
+on dirty workspace or word length.
+
+For fixed positive per-label tariffs `cost(a)=alpha`, `cost(b)=beta`, the
+same proof and witness give exactly `2k(alpha+beta)`. This corollary assumes
+uniform prices within each label; it is not a statement about port-dependent
+or word-dependent implementation overhead.
+
+Neither representation is faithful on the group algebra. They are used
+only for necessary conditions in the lower bound. The attaining word is
+proved in the formal algebra itself. In particular, the nonzero element
+`lambda = ([a]+1)([c]+1)` is killed by **both** representations; a suitable
+off-diagonal `lambda` perturbation of the endpoint must still be rejected.
+The verification includes this control explicitly.
+
+## Reproduce and evidence boundary
+
+From the repository root, using Python 3.12 or later and its standard library:
+
+```sh
+python3 -I -O -B research/ut3-commutator-all-registers/verify.py
+```
+
+`verify.py` uses formal group-algebra coefficients. `independent.py` imports
+none of that implementation and constructs a faithful regular representation
+from explicit binary address matrices. The committed `CERTIFICATE.json`
+records their deterministic finite checks. The default command is read-only;
+`--emit` prints a fresh receipt for comparison without overwriting files.
+The registered replay is
+
+```sh
+python3.12 scripts/research_package.py --package research/ut3-commutator-all-registers
+```
+
+The scripts check the algebraic maps, attaining words, full dirty boundaries
+and semantic mutations. They are finite corroboration of the definitions and
+witnesses. The argument above, not those finite fixtures, proves the unbounded
+register and target statement. This is not a proof-assistant verification or
+an independent human review. Exact executed coverage is in the certificate
+and `VALIDATION.md`.
+
+## Provenance, selection and limits
+
+Base: `680967accfd4311f3241dc154e1f434869747b43`. OS assignment seed **14**
+selected the bit-supplier track. Its residue selects the three-target,
+one-dirty-extra fixture (`k = 1 + 14 mod 3 = 3`, `r = 4`) for emphasis;
+the mathematical proof is seed-independent. `CLAIM.json` records all three
+candidates, overlap checks, the local claim and the stopping rule. No pinned
+sprint issue existed. `TASK.json` records the catalogue refinement.
+
+PR1478 is pinned at `b30fdba48f3db70e3589ba740b0782b56ec0ba2e`.
+PR1443 is pinned at `965ff75aabb16cdd0978f4bf9222bcdedf514021`.
+The selected record at the base is PR1094, conditional
+`kappa = 0.001672660197076918`, with PR589 on PR555 as the bit supplier;
+the complex supplier binds. `SOURCES.json` records exact contextual source
+pins. No predecessor executable is imported or needed by the standalone check.
+
+This closes the arbitrary-workspace question for **these central targets
+and this two-letter alphabet**. It does not exclude savings for other
+targets, expanded address alphabets, clean/noninvertible workspace contracts,
+or different realization interfaces. It neither reopens the already proved
+abelian three-register result nor establishes an all-size rational-frame
+identity. There is no proposed selected-supplier replacement, new paid rank
+histogram, new kappa, physical compiler, hosting, precision/tape or analytic
+transfer result. The selected construction and `upstream/` are unchanged.
+
+## Open next questions
+
+Can a legally priced larger address alphabet improve the complete supplier
+budget? Allowing `c` itself at price `gamma` already offers the direct
+`k*gamma` bill, while the proved two-letter bill is `2k(alpha+beta)`.
+The first useful step is to specify and fully price one actual implementation
+of the additional call, including frames and restoration, before any search.
+The blocker is its realization in the supplier: declaring it a unit-cost
+operation would change the model without establishing an improvement.
+The present theorem settles the workspace-only route in the stated model.
+
+## Credit and disclosure
+
+Prepared for **steph4n-gh** with substantial **OpenAI Codex assistance** in
+research, proof, implementation, independent AI checking and packaging.
+Credit @juper997 (PR1478) for the finite commutator result and explicit
+all-register question; @woklerx (PR1443) for the earlier two-register D8
+commutator result; Arham Tahir (Discussion1569) for the concurrent two-target
+all-register argument; Gareth Davidson / @bitplane (PR1333) for the
+restricted-alphabet direction and augmentation normalization; @commdata2338
+(PR1414) for the related coordinate-swap investigation; and eumemic (PR288),
+Ali Romman (PR468), David Govea (PR720) and the retained register-model
+lineage. No broader literature-priority claim is made. Apache-2.0.

research/ut3-priced-central-calls/PREDECESSOR.json

@@ -0,0 +1,10 @@
+{
+  "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1573",
+  "head": "0b8c5a69297c794f2de22c04494c83e41300ae36",
+  "path": "research/ut3-commutator-all-registers/README.md",
+  "git_blob": "4a6a4ee9d995818348b3b853a95500dcce81228d",
+  "sha256": "fdd5405da1c0535a407013f2a4628a07dae4957fd9fb776cd14f05315d1aa26b",
+  "author": "steph4n-gh",
+  "license": "Apache-2.0",
+  "usage": "proof predecessor; no executable imported"
+}

research/ut3-priced-central-calls/README.md

@@ -0,0 +1,47 @@
+# Sharp tariff after adding a paid UT3 central call
+
+For every finite register count r >= k >= 1, the exact positive uniform tariff for k central targets in the formal F2[UT3(F2)] model with paid labels a, b and c=abab is
+
+`k min(2(alpha+beta), gamma)`.
+
+Here alpha, beta and gamma are positive inclusive per-call prices. Mixing central and noncentral calls cannot beat both direct choices, even with arbitrary free scalar mixing and arbitrarily many restored dirty registers. This is a scoped tariff theorem, not an implemented supplier improvement or new kappa.
+
+## Model and precise delta
+
+Retain PR1573's formal group algebra, rank-one binary idempotents N=uv^T with v^T u=1, arbitrary scalar GL_r(F2) basis changes, and endpoint diag([c] repeated k times, identity on all remaining dirty roles). The changed alphabet admits D_N(c)=I+([c]+1)N as an additional **paid** primitive. Each a, b and c call costs alpha, beta and gamma respectively. No COPY, clean allocation, higher-rank unit-price call or free restoration is added. Prices must include their actual implementation overhead if used in a supplier comparison; this package supplies no such implementation.
+
+The two-letter theorem in PR1573 gives n_a,n_b >= 2k. Its open question observes the two direct bills after adding c, but does not prove that hybrid words cannot undercut both. The new implication is
+
+`n_a,n_b >= 2 max(k-n_c,0)`.
+
+The first assignment's third-register census was abandoned upon overlap with PR1478, PR1573, PR1742 and PR1792. Its pilot is not counted as a result. The present change is one bounded alphabet pivot.
+
+## Proof
+
+Normalize free scalar maps into rank-one projectors by conjugation, as in PR1573; augmentation forces the final free scalar map to be identity. Write P=diag(I_k,0) and S=sum of the n_c central-call projectors. Apply the natural three-dimensional representation of UT3 entrywise to the complete register word. In address-block order, a contributes N at block01, b contributes N at block12, and c contributes N at block02. Products involving a central off-diagonal block and any other strictly upper-triangular block vanish. Thus the endpoint implies
+
+`X_a Y_a=0`, `X_b Y_b=0`, `C_ab + S=P`,
+
+where C_ab=sum over ordered a-before-b pairs of N_i N_j, X_g collects the u columns and Y_g the v rows. The automorphism sigma(x,y,z)=(y,x,z+xy) swaps a,b and fixes c. Its representation likewise gives `C_ba+S=P`.
+
+Put q=rank(P+S). Since rank(S)<=n_c, q>=max(k-n_c,0). The column and row containments of C_ab and C_ba imply rank(X_a), rank(Y_a), rank(X_b), rank(Y_b) >= q. The zero products X_g Y_g=0 imply rank(X_g)+rank(Y_g)<=n_g by rank-nullity. Hence each noncentral count is at least2q, proving the displayed implication for every r and every word length.
+
+Consequently the complete abstract bill is at least `2 max(k-n_c,0)(alpha+beta)+gamma n_c`. For 0<=n_c<=k this is affine in n_c, and above k its positive central term is at least k gamma. The minimum is therefore the claimed k times the cheaper direct tariff. It is attained by c on each target if gamma is smaller, or by abab on each target otherwise. More generally t central targets and k-t commutator targets attain every endpoint of the count tradeoff: `(n_a,n_b,n_c)=(2(k-t),2(k-t),t)`. All unused roles are identity operators on arbitrary inputs. This is an algebraic proof; finite fixtures are corroboration, not its substitute.
+
+## Reproduce and evidence
+
+`python -I -O -B research/ut3-priced-central-calls/verify.py`
+
+`python scripts/research_package.py --package research/ut3-priced-central-calls`
+
+Fourteen mixed words cover k=1..4 and every t=0..k with two extra dirty roles. A separate faithful regular-action engine uses literal binary 3x3 address matrices; it does not use the group-ring multiplication engine. Scalar-conjugated fixtures deliberately mix dirty inputs into targets. Every individual call omission is rejected. Further controls expose the invalid reuse of the two-letter bound after adding c, the need to price a rank-two central operation as two rank-one calls, and a zero-dirt false positive. Exact integer/rational tariff checks corroborate the affine optimization. The written rank proof supplies the arbitrary-register statement.
+
+The selected result, native circuits, hosted supplier, all-size compiler, precision/tape, outer assembly and analytic transfer were not replayed. No new paid rank histogram, physical central implementation or kappa is claimed. The natural representations serve only necessary lower-bound conditions; formal equality of the upper constructions is separately checked.
+
+## Open next questions
+
+Can a real central operation have inclusive price below 2(alpha+beta)? That is now necessary for an improvement through this alphabet. Start with one concrete supplier frame and charge its entire central operation, frame transitions and restoration. The blocker is realization, not the abstract mixture optimization. Structured questions are in TASK.json.
+
+## Sources and credit
+
+The exact PR1573 README is preserved unchanged in PR1573-README.md with full commit, Git blob and SHA256 in PREDECESSOR.json. Credit steph4n-gh for the arbitrary-register two-representation/rank proof, juper997 PR1478 and woklerx PR1443 for finite D8 predecessors, Arham Tahir Discussion1569 for concurrent two-target reasoning, Gareth Davidson/bitplane PR1333 and the register-model lineage retained in the source. The new step allows paid c calls and proves the hybrid count/tariff bound. Prepared for woklerx with substantial OpenAI Codex assistance. Apache-2.0; no independent human review claimed.