Prove the exact weighted tariff for two normal semilinear targets

research/semilinear-two-normal-prices/PROOF.md

@@ -0,0 +1,169 @@
+# Exact weighted price for two normal targets
+
+This is a scoped written proof. It answers the two-target first experiment
+in Open next question 1 of Krzysztof Wojt's PR5242. The earlier unit-price
+semilinear theorem, scalar normalization and natural representation retain
+their predecessor credit. The new contribution is the quotient-loop rigidity,
+including repeated labels, and its weighted tariff consequence. Josie Elliston / PR6048
+already excludes three calls for distinct pair targets in every group when
+no paid label is a target. Its distinct-target floor is credited rather than
+claimed as new here. The proof below does not need that predecessor as an
+assumption; it also covers the repeated-label case excluded there.
+
+## Contract
+
+Let p be any odd prime, F = F_(2^p), and G = F* semidirect C_p, with
+
+    (a,j)(b,k) = (a b^(2^j), j+k mod p).
+
+Work in Mat_r(F2[G]) for any finite r >= 2. All roles start independently
+arbitrary. A paid call is D_P(g) = I + P tensor ([g]+[1]), where g != 1
+and P = u v^T is a binary rank-one idempotent, v^T u = 1. Free operations
+are arbitrary GL_r(F2) scalar maps. The exact full formal endpoint is
+
+    diag([h_1], [h_2], [1], ..., [1]),
+
+where h_1 and h_2 are nonidentity normal elements, meaning (a,0), a != 1.
+Repeated labels are allowed. Thus every other dirty role must be restored.
+A normal call costs a > 0 and an outside call costs b > 0, uniformly within
+each type. There are no other free address maps or higher-rank paid calls.
+
+**Theorem.** The exact minimum price is 2 min(a, 2b).
+In particular, the minimum number of outside-only calls is four.
+The prices are arbitrary positive real numbers. They are formal complete
+per-call prices within this contract, not a claimed physical supplier bill.
+
+## A three-factor quotient lemma
+
+Let K be any extension of F2. For i = 1,2,3 let P_i be binary rank-one
+idempotents and let lambda_i be nonzero elements of K different from 1.
+Set A_i = I + (lambda_i+1) P_i. Then
+
+    A_3 A_2 A_1 = I  implies  P_1 = P_2 = P_3.
+
+It also implies lambda_1 lambda_2 lambda_3 = 1.
+
+Write P_i = u_i v_i^T with binary vectors and v_i^T u_i = 1.
+Since A_3 is invertible,
+
+    A_2 A_1 - I = (lambda_3^(-1)+1) P_3
+
+has rank one. Put c_i = lambda_i+1 != 0. Direct multiplication gives
+
+    A_2 A_1 - I = c_1 u_1 v_1^T + c_2 u_2 v_2^T
+                    + c_1 c_2 (v_2^T u_1) u_2 v_1^T.
+
+If both the two columns u_1,u_2 and the two rows v_1,v_2 are independent,
+this expression factors as a full-column-rank matrix, an invertible 2 by 2
+triangular matrix with diagonal c_1,c_2, and a full-row-rank matrix.
+Its rank is two, a contradiction. Consequently either u_1=u_2 or v_1=v_2.
+Nonzero binary vectors that are proportional over K are equal.
+
+Suppose u_1=u_2=u. If v_1 != v_2, the product difference is
+
+    u (lambda_2 c_1 v_1^T + c_2 v_2^T).
+
+Both row coefficients are nonzero. Its column space is Ku, so the binary
+column in P_3 must be u. Also
+
+    span_K(v_1,v_2) intersect F2^r = span_F2(v_1,v_2).
+
+For completeness, binary independent rows admit binary coordinate duals;
+applying these to a binary vector in their K-span recovers binary
+coefficients. The only possible nonzero v_3 are v_1, v_2 and v_1+v_2.
+The first two are excluded because both displayed coefficients are nonzero.
+The last satisfies (v_1+v_2)^T u = 0, contradicting idempotence of P_3.
+Therefore v_1=v_2. The common-row case follows by transposing the two-factor
+product and using the same argument in reversed order. Thus P_1=P_2.
+Their product is I+(lambda_1 lambda_2+1)P_1. It cannot be I because
+A_3 != I. Comparison with A_3^(-1) yields P_3=P_1 and the scalar identity.
+This proves the lemma for every finite r, without a dimension census.
+
+The binary restriction matters. Over F4, let w^2+w+1=0 and use common
+column e_1 with rows (1,0), (1,1), (1,w). All three projectors are
+idempotent and different. Taking lambda_i=w gives A_3 A_2 A_1=I.
+The verifier checks this boundary exactly. It is outside the contract.
+
+## Three outside calls cannot deliver the two normal targets
+
+Move all free scalar maps to the right using
+
+    S D_P(g) = D_(S P S^(-1))(g) S.
+
+Augmentation [g] -> 1 sends every paid factor and the required target to I,
+so the remaining free scalar product is I. Normalization preserves binary
+rank-one idempotence, labels and prices. This is PR5242's normalization.
+
+Choose a characteristic-two extension K containing a primitive p-th root
+zeta. The quotient character chi(a,j)=zeta^j extends to the group algebra.
+Every outside label has chi(g) != 1 and every normal target has character 1.
+Thus a hypothetical three-outside-call word gives A_3 A_2 A_1=I in this
+representation. The lemma forces all three normalized projectors to be P.
+In the full formal algebra, their product then equals D_P(g_3 g_2 g_1).
+This equality follows from P^2=P and (I-P)P=P(I-P)=0; no commutation of
+the group labels is assumed.
+
+A single such projector cannot equal the two-target endpoint. Define a
+binary linear functional ell on F2[G] that sends [1] to zero and both
+[h_1] and [h_2] to one. This is well-defined even when h_1=h_2, since the
+normal targets are nonidentity basis labels. Apply ell entry by entry to
+the difference from I. The target gives diag(1,1,0,...,0), of rank two.
+D_P(g_3 g_2 g_1)-I gives a scalar multiple of P, of rank at most one.
+This contradiction proves the new obstruction, including arbitrary
+restored dirty workspace.
+
+## Lower bound for arbitrary mixtures and prices
+
+Use the natural representation rho(a,j)(z)=a z^(2^j) on F. PR5242 proves
+its displacement rank is p on normal labels and p-1 on outside labels.
+Rank telescoping therefore gives, for N normal and O outside calls,
+
+    p N + (p-1) O >= 2p.
+
+This cited premise is used without replaying the predecessor theorem.
+If N >= 2, the price is at least 2a. If N=1, the inequality excludes O<=1,
+so the price is at least a+2b. If N=0, it excludes O<=2, and the new
+three-call obstruction excludes O=3. The price is then at least 4b.
+Every legal word consequently costs at least
+
+    min(2a, a+2b, 4b) = 2 min(a,2b).
+
+This is a case split over all possible call counts, not a bounded search.
+
+## Attainment
+
+One coordinate normal call on each of the two target roles costs 2a.
+Every nonidentity normal element h=(c,0) factors as
+
+    h = (c,-1) (1,1).
+
+Both factors are outside because p is odd. Applying the two corresponding
+calls successively on the same coordinate projector gives D_(E_ii)(h).
+Doing this on each target role costs 4b, restores every other role, and
+attains the full formal endpoint. Replacing only one role gives the
+intermediate price a+2b. Choosing the cheaper endpoint price proves the
+theorem. The attaining words use no clean workspace.
+
+## Limits and credit
+
+The all-prime and all-workspace quantifiers rest on this written proof.
+Finite checks corroborate the new quotient lemma and attaining words.
+They are not independent human review or formal proof-kernel acceptance.
+Three or more normal targets, mixed target lists, arbitrary per-label
+prices, nonbinary free mixing and higher-rank paid calls remain outside
+this theorem. No universal optimum for all semilinear target lists is claimed.
+
+Native realization, physical movement, ownership, restoration implementation,
+precision, stock/compiler, recursive and outer invoices remain unpriced.
+No new kappa, supplier admission, complete multiplication theorem or
+selected-frontier change follows.
+
+This proof and its verifier were produced by Nick Petalas. Credit Krzysztof
+Wojt / PR5242 for the question, quotient character, mixed unit-price theorem
+and support-rigidity method; Nick Petalas / PR5202 for the normal-C7 rank
+bound; Cinna Davis / PR2011 and PR3893 for the model and representation
+precedent; eumemic / PR288 and the retained register-model lineage.
+Josie Elliston / PR6048 supplies the distinct-label all-group short-word
+obstruction, following Nick Petalas / PR6038. The source statements are
+pinned as provenance in SOURCES.json.
+Apache-2.0.

research/semilinear-two-normal-prices/README.md

@@ -0,0 +1,103 @@
+# Exact weighted tariff for two normal semilinear targets
+
+**Scoped written proof with exact finite corroboration; no new kappa.**
+For every odd prime p, two nonidentity normal targets in
+F2[F_(2^p)* semidirect C_p] have exact price
+
+    2 min(a, 2b),
+
+when every normal call costs a>0 and every outside call costs b>0.
+The theorem permits repeated target labels, arbitrary finite restored dirty
+workspace and free binary scalar mixing. Paid factors are rank-one
+idempotents, and the endpoint is the complete formal group-algebra operator.
+
+This settles the two-normal-target first experiment in Open next question 1
+of [Krzysztof Wojt's PR5242](https://github.com/CrocSwap/integer-mult-bounds/pull/5242).
+The new step excludes three outside calls. In the quotient character,
+a three-call identity forces all three binary projectors to coincide;
+one shared projector cannot deliver two independent nonidentity outputs.
+Four outside calls attain the target, by factoring each normal label into
+two outside labels. The [written proof](PROOF.md) combines that obstruction
+with PR5242's credited natural-rank budget to settle every mixture and price.
+Josie Elliston's [PR6048](https://github.com/CrocSwap/integer-mult-bounds/pull/6048)
+already excludes three calls for distinct pair targets in every group when
+no paid label is itself a target. That prior distinct-label floor is credited.
+The new quotient-loop rigidity also treats repeated labels, which PR6048
+explicitly excludes, and yields the weighted tariff above. No new
+distinct-pair unit-price floor is claimed. No predecessor census is rerun
+as a deliverable.
+
+## Exact finite evidence
+
+The deterministic verifier checks the new three-factor lemma over F4 and
+F8, with one to three roles. It enumerates 32,840 ordered factor pairs and
+all 1,120 resulting three-factor loops; every loop has one common projector.
+It also checks 4,116 literal three-outside-call words in the full order-21
+algebra and 144 attaining words for all 36 ordered pairs of normal targets,
+including their arbitrary third dirty role. Each full endpoint comparison
+checks every formal coefficient. A 13,203-case bounded count/price screen
+corroborates the written unbounded case split. Eleven rejection controls and
+an explicit nonbinary three-projector counterexample check the hypotheses.
+A separate direct triple loop checks all 1,728 F4 two-role triples, without
+the pair/inverse lookup used by the main finite census.
+The finite fields and sizes do not prove the universal quantifiers.
+
+The verifier prints a freshly generated JSON receipt with hashes of all
+package files. It writes no files and has no external runtime inputs.
+[SOURCES.json](SOURCES.json) pins the original question and cited proof as
+provenance, alongside the catalogue and selected record at canonical main
+7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8.
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360644)
+records the target before substantial work.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/semilinear-two-normal-prices/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/semilinear-two-normal-prices/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/semilinear-two-normal-prices
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/semilinear-two-normal-prices --check-source-history
+```
+
+Another CPython 3.12 path works. The registered normal and optimized commands
+have a 60-second bound each. The direct checker also runs without Git in an
+export containing this package. Package and publication checks authenticate
+bytes and source history separately from the mathematical argument.
+
+## Scope and remaining obligations
+
+This is a formal weighted tariff, not an implemented physical supplier.
+Native address operations, hosting/owners, physical restoration, movement,
+precision, stock/compiler and a complete recursive/outer bill are unknown.
+No new kappa, selected-frontier change or multiplication theorem is claimed.
+Independent human and formal proof-kernel review are unclaimed. Lean, Docker
+and the selected scientific cold replay are not part of this package.
+
+## Open next questions
+
+- Does a joint saving become possible for three normal targets with unequal
+  type prices? The three-call loop lemma does not classify longer quotient
+  identities. Start with the cheapest outside-only counts allowed by the
+  natural-rank inequality and prove their full formal endpoint, rather than
+  treating the rank relaxation as attainable. The blocker is a longer-word
+  structure theorem or an explicit sharing construction.
+- Can one actual native caller realize the two-outside factorization with
+  a physical price below its normal call? First price both outside maps,
+  binary role changes, routing and restoration at one named boundary.
+  A legal source-bound physical interface is missing.
+
+These questions are unreserved and structured in [TASK.json](TASK.json).
+The result is shipped at this first proved improvement.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Krzysztof Wojt / PR5242
+supplies the question, quotient-character method and natural-rank premise;
+Nick Petalas / PR5202 supplies the normal-C7 theorem; Cinna Davis / PR2011
+and PR3893 supply the semilinear model and representation precedent;
+Josie Elliston / PR6048 supplies the distinct-label short-word obstruction,
+building on Nick Petalas / PR6038; eumemic / PR288 and the retained
+register-model lineage keep their credit.
+No predecessor files or credit lines are changed. Apache-2.0.

research/semilinear-two-normal-prices/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/conjugate-pair-group-free-audit/README.md",
+      "usage": "provenance",
+      "git_blob": "c0ae47bf6c566c69466e150661641d61fd9ff636",
+      "sha256": "3adf65a79d27ea7a60ec8978fa6b45f75d65c07c3aed019080b64431078f28f3"
+    },
+    {
+      "path": "research/semilinear-mixed-tariff/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "bc81fbd7ec32d8aeed9aa93fa3cf40396fef51bc",
+      "sha256": "171129b057490dea131aeeaab6941d4ae55b756143356f5a3656215ccfb44b2f"
+    },
+    {
+      "path": "research/semilinear-mixed-tariff/README.md",
+      "usage": "provenance",
+      "git_blob": "dc95473ba57ec799194c33fc030f1f82dba484d2",
+      "sha256": "edecd78f1ab2661ac4115c09cd7b47d06274672f4a6a7a20202d9b5812a84c80"
+    }
+  ]
+}