Prove exact central UT4 tariffs for every dirty workspace (no κ)

research/ut4-hyperbolic-middle-floor/PROOF.md

@@ -0,0 +1,138 @@
+# Sharp central-target tariffs from a paired middle quotient
+
+This scoped written proof was produced by Nick Petalas. Apache-2.0.
+
+## Statement and inherited model
+
+Use ToikY's [PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662)
+formal model. Let G=UT4(F2), with a=I+E12, b=I+E23, c=I+E34 and
+z=I+E14. On any finite r>=w>=1 roles, every paid factor is
+
+    I_r + ([g]+1) x y^T,   g in {a,b,c},   x,y nonzero in F2^r.
+
+Both idempotent and nilpotent scalar couplings are allowed. The complete
+endpoint is I_r+([z]+1)P, where P=diag(I_w,0), or any common scalar
+conjugate of that projector. Every role has arbitrary input, every extra
+role is restored, and all paid factors, including restoration, are counted.
+Interleaved free scalar GL_r(F2) mixing normalizes into the couplings as in
+PR1662. Augmentation forces the final free scalar map to be identity.
+There are no other free address operations, COPY, ERASE or initialized roles.
+
+Every such word satisfies the new bound
+
+    n_b >= 2w + rank(X_b) + rank(Y_b) >= 4w.
+
+Together with PR1662's n_a,n_c>=2w, and its direct word, this gives the
+exact complete tariff for all nonnegative uniform per-letter prices:
+
+    min cost = 2w alpha + 4w beta + 2w gamma.
+
+In particular, the unit minimum is 8w for every finite dirty workspace.
+The theorem excludes the (2,3) and (3,2) seven-b cases left open by Victor
+Li's [PR3938](https://github.com/CrocSwap/integer-mult-bounds/pull/3938).
+It also supplies a direct algebraic exclusion of every n_b<4w case.
+No chronological search or predecessor census is a premise of this proof.
+
+## Coefficient premises
+
+We use PR1662's fixed degree-three algebra homomorphism
+
+    F2[G] -> Q = F2<A,B,C>/(A^2,B^2,C^2,AC-CA, degree>=4),
+    [a] -> 1+A, [b] -> 1+B, [c] -> 1+C,
+    [z] -> 1+ABC+ACB+BAC+CBA.
+
+Its fixed homomorphism lemma and the outer-letter span bound are credited
+premises, not new audit deliverables. Q has the basis
+
+    1,A,B,C,AB,AC,BA,BC,CB,ABA,ABC,ACB,BAB,BAC,BCB,CBA,CBC.
+
+For a scalar-matrix word, write H_s for the coefficient of a basis
+monomial s in its product over Q. Since ABA, ABC, CBA and CBC have no
+alternative representative from AC=CA, each is the literal ordered
+subsequence sum with those three labels. The endpoint therefore implies
+
+    H_B=H_AB=H_CB=H_BA=H_BC=0,
+    H_ABA=H_CBC=0,   H_ABC=H_CBA=P.                 (1)
+
+All equations hold as full r-by-r matrices, including every dirty block.
+
+## The new paired factorization
+
+Number the n=n_b middle calls in product order. Write their couplings as
+B_j=x_j y_j^T and put
+
+    X = [x_1 ... x_n],             Y = [y_1^T; ...; y_n^T].
+
+For each middle call j, let A_j^- and C_j^- be the sums of the a and c
+couplings strictly before it. Let A_j^+ and C_j^+ be the corresponding
+sums strictly after it. Define
+
+    U_A = [A_j^- x_j]_j,          V_A = [y_j^T A_j^+]_j,
+    U_C = [C_j^- x_j]_j,          V_C = [y_j^T C_j^+]_j,
+    U = [U_A; U_C],               V = [V_A V_C].
+
+Here X has shape r-by-n, Y has shape n-by-r, U has shape 2r-by-n,
+and V has shape n-by-2r. Distributivity in the original chronological
+order, without commuting scalar matrices, gives
+
+    XY = H_B,
+    UY = [H_AB; H_CB],
+    XV = [H_BA H_BC],
+    UV = [ H_ABA  H_ABC ] = [ 0 P ].
+         [ H_CBA  H_CBC ]   [ P 0 ]              (2)
+
+For example, every term in U_A V_C chooses one a call before middle call
+j and one c call after it, so it contributes exactly once to H_ABC.
+The same expansion gives the other three blocks. No assumption that an
+a prefix equals its suffix is needed.
+
+By (1), XY=UY=XV=0. Thus im(Y) is a subspace of ker(X), V takes values
+in ker(X), and U vanishes on im(Y). The product UV factors through
+
+    ker(X)/im(Y),   dimension n-rank(X)-rank(Y).
+
+The matrix on the right of (2) has rank 2 rank(P)=2w: its two image
+blocks are separate copies of im(P). Therefore
+
+    2w <= n-rank(X)-rank(Y).                      (3)
+
+This is the new step. Keeping only H_ABC uses a rank-w product and gives
+the weaker middle quotient bound in PR1662. The zero ABA and CBC blocks
+allow both cross coefficients to contribute their ranks simultaneously.
+
+For completeness, PR1662's remaining middle span argument is short.
+The H_BAC coefficient also includes the BCA subsequences because AC=CA.
+Every summand starts with a b coupling. Its image is consequently in
+im(X). Since H_BAC=P, rank(X)>=w. Similarly H_ACB includes CAB, every
+summand ends with a b coupling, and its row space lies in row(Y).
+Since H_ACB=P, rank(Y)>=w. Substitution in (3) proves n_b>=4w.
+
+## Attainment and exact weighted optimum
+
+PR1662's direct group word (abcb)^2=z has counts (2,4,2).
+On one coordinate role the scalar coupling is the coordinate projector,
+so the same word acts by z on that role and by identity on all others.
+Use it separately on all w active roles. The resulting word has counts
+(2w,4w,2w), implements the complete formal endpoint, and restores every
+dirty role. A common free scalar conjugation gives any conjugate P.
+
+The inherited outer bounds n_a,n_c>=2w and the new n_b>=4w hold
+simultaneously for every word. The direct word attains them simultaneously,
+so its tariff is minimal for any nonnegative alpha,beta,gamma. This
+conclusion permits zero prices, but still concerns finite words only.
+It does not price role-dependent calls or a physical implementation.
+
+## Evidence and limitations
+
+The universal statement is the written factorization and dimension argument.
+The local verifier checks the new paired identity by two different finite
+calculations: polynomial coefficient expansion and prefix/suffix arrays.
+It checks attaining words against the full 64-element group algebra.
+No predecessor program or stored census is imported or executed.
+
+The result is a scoped proof in this formal operation alphabet. It is not
+a native supplier, a rational-frame identity or a complete multiplication
+theorem. Common-label compilation, physical realization, stock, precision,
+tape, analytic recovery and all five selected framework assumptions remain
+separate. No new kappa or selected-frontier change is claimed. Independent
+human and formal proof-kernel review are unclaimed.

research/ut4-hyperbolic-middle-floor/README.md

@@ -0,0 +1,110 @@
+# Exact central UT4 tariffs for every restored dirty workspace
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped proof: in ToikY's PR1662 formal F2[UT4(F2)] model, w central
+targets require at least 4w paid b calls, for every finite number of
+arbitrary restored dirty roles. The stronger bound is
+
+    n_b >= 2w + rank(X_b) + rank(Y_b).
+
+With the credited outer bounds and direct construction, the exact complete
+tariff is 2w alpha+4w beta+2w gamma for all nonnegative uniform letter
+prices. The unit minimum is 8w. In particular, neither remaining
+seven-b rank pattern, (2,3) or (3,2), can realize two central targets.
+This settles the mixed-rank question in Victor Li's
+[PR3938](https://github.com/CrocSwap/integer-mult-bounds/pull/3938).
+
+The new step stacks both a/c prefix maps and concatenates both suffix
+maps. Their product is [[0,P],[P,0]], of rank 2w, and factors through
+ker(X_b)/im(Y_b). [PROOF.md](PROOF.md) gives the full argument.
+The lower bound already holds in the retained degree-three quotient;
+no larger census or higher coefficient is needed. No new kappa or
+selected-frontier change is claimed.
+
+## Reproduce
+
+From the worktree root with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/ut4-hyperbolic-middle-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ut4-hyperbolic-middle-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ut4-hyperbolic-middle-floor --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. The standalone
+verifier works in a Git-free six-file export and writes nothing. It emits
+PASS_UT4_HYPERBOLIC_MIDDLE_FLOOR and a generated receipt containing all
+six file hashes. Registered warning-strict normal and optimized checks
+use explicit exceptions, so optimization cannot disable the checks.
+
+Finite corroboration checks the new paired coefficient identities on
+20,632 words, consisting of every two-role word through length three
+and 192 deterministic eighteen-call three-role words. Polynomial
+multiplication and prefix/suffix construction use different paths.
+Forty-two attaining words through six roles have complete full-group
+algebra endpoint checks, including common scalar conjugations and every
+dirty output block. Eighty omitted-call controls and ten additional
+contract, endpoint and hypothesis controls reject. The universal result
+is the written rank argument, not extrapolation from these fixtures.
+
+## Credit, overlap and scope
+
+Credit ToikY / [PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662)
+for the alphabet, fixed quotient homomorphism, outer and middle span
+bounds, earlier rank-w middle quotient and direct (2,4,2) word. Credit
+Victor Li / PR3938 and
+[PR3887](https://github.com/CrocSwap/integer-mult-bounds/pull/3887) for
+the mixed-rank question and earlier scoped exclusions. Credit Josie
+Elliston / [PR1816](https://github.com/CrocSwap/integer-mult-bounds/pull/1816)
+for two-target unit optimality and the weighted question. Retain Aaron
+Wang / PR1690's profile lineage, ToikY / PR1680's workspace reduction,
+and the steph4n-gh / PR1573, Arham Tahir / PR1589 and Hanson Sun / PR1607
+register-model lineage credited by PR1662. The direct upper word and
+outer floors are inherited. The paired middle quotient is the new result.
+
+All source files in [SOURCES.json](SOURCES.json) are provenance only.
+No predecessor program or census is imported, audited or replayed.
+The scientific base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a,
+priority revision 8. The selected-binding baseline passed. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360859)
+asked about seven middle calls; the same new argument yields the uniform
+tariff directly. Live PR bodies, recent account work, handoffs, batch
+reservations, merged searches and distinctive main README searches were
+checked. Sparse local coverage and unpublished work remain limitations.
+
+The historical bit-new-register-model card is refined to this formal
+tariff obstruction. It gives a stopping rule for this alphabet, rather
+than a physical BIT improvement. Role-dependent prices, extra free
+address maps, rational frames, clean allocation, native realization,
+compiler/hosting, stock, precision, tape and analytic recovery are outside
+the result. The five selected framework assumptions remain. No selected
+supplier replay, Lean or Docker run was made. Independent human and
+formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+Can a changed operation alphabet, such as an additional paid address
+letter, escape the 4w middle floor? Start by computing its image in Q
+and deciding which equations in (1) of the proof cease to hold. A
+candidate must pay for the added operation and retain arbitrary dirty
+restoration before it can affect a supplier invoice. The present theorem
+does not cover that changed alphabet. Structured details are in
+[TASK.json](TASK.json).
+
+## Verifier constraints
+
+The six-file verifier has no recursion, subprocesses, network or output
+files. Its fixed domains have at most six roles, 48 calls, 64 group
+elements and 20,632 coefficient fixtures. Functions are below 60 lines;
+matrix/rank dimensions and file reads have explicit limits. Failures
+propagate as exceptions. The local AST/compile inspection and both
+warning-strict modes are the available Python diagnostics.
+
+Power-of-ten rule 3 deviation: CPython allocates managed integers and
+containers during the finite command. Live state is bounded by the
+fixed domains above, with at most 64 group matrices or 17 quotient
+matrices per endpoint. Rule 9 deviation: rejection controls dispatch
+only to quotient_rank, coupling, validate_word and central_check with
+fixed local fixtures. No arbitrary callback or code loading is accepted.
+An embedded fixed-allocation implementation would need a separate runtime.

research/ut4-hyperbolic-middle-floor/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/ut4-central-tariff-relaxation/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "8137274359979a786568da60bc802eeba2728e7f",
+      "sha256": "4820f0771cc6d5828492bf8cb0bacda2a74d3f00b58a02b8df056ab1db040f21"
+    },
+    {
+      "path": "research/ut4-two-target-nb7-ranks-22/README.md",
+      "usage": "provenance",
+      "git_blob": "d65cec816eb2dc658bd616cc55ca67f807055fa7",
+      "sha256": "5297e8a16e22cdfc54445f3c3e747ebd8f36162dd00ee227dde56e05f1d0be09"
+    },
+    {
+      "path": "research/ut4-two-target-fifteen/README.md",
+      "usage": "provenance",
+      "git_blob": "3d314e22e7a9d1941269b161c833fbd3bcfc8934",
+      "sha256": "fb1026abcf357b5a409a2398eb18c9ae7c72541176dafa0b02c819b79e8f9b5f"
+    }
+  ]
+}