Prove exact source-injection tariffs for completed partial echoes

research/completed-partial-echo/PROOF.md

@@ -0,0 +1,149 @@
+# The exact completed-observation injection tariff
+
+This contribution was produced by Nick Petalas. It is a scoped written
+algebraic proof. Exact finite checks corroborate the implementation; they
+are not a proof-kernel verification or a multiplication theorem.
+
+## Boundary and alphabet
+
+Work over any field of characteristic zero. Let X and W be vectors in the
+same nonzero finite-dimensional space, and let D be a vector in another
+nonzero finite-dimensional space. All three incoming vectors are arbitrary
+and independent. X is an immutable source, W is borrowed dirty workspace,
+and D is an additive receiver. There is no other data storage.
+
+Fix s independently arbitrary linear maps L_i from the source space to the
+receiver space. A word must work uniformly for every tuple of these maps.
+Its available instructions, including their positive complete prices, are
+
+| Instruction | Action | Price |
+| --- | --- | --- |
+| H_i | D += L_i W | c_i^+ |
+| H_i inverse | D -= L_i W | c_i^- |
+| J_+ | W += X | a |
+| J_- | W -= X | b |
+
+Every instruction leaves the other fields unchanged. H_i and its inverse
+are fixed indivisible source-preserving blocks, including any internal
+workspace restoration and normalization. No direct L_i X evaluation,
+scalar rescaling, output feedback, query retention, map-dependent word,
+additional borrowed field or free copying is permitted. Repetition and
+arbitrary interleaving of all labels are allowed. In particular, a lower
+bound may not assume that only H_i occurs between checkpoints i-1 and i.
+
+There are ordered, read-only output checkpoints O_1,...,O_s. At O_j the
+required receiver is exactly
+
+    D_initial + (L_1 + ... + L_j) X.
+
+The observer sees only D. W need not have its incoming value at a checkpoint.
+At return, X and W must both equal their incoming values, and D must still
+equal its final observed value. Observation execution has a separate cost,
+common to every compared word and excluded from this instruction tariff.
+
+## Theorem
+
+The exact minimum complete instruction price is
+
+    sum_i (c_i^+ + c_i^-) + ceil(s/2) (a+b).                 (1)
+
+In particular, exactly 2 ceil(s/2) source injections suffice. Every word
+needs at least one forward and one inverse use of each label and at least
+ceil(s/2) uses of each injection direction. These bounds hold simultaneously
+and are simultaneously attained, for arbitrary positive prices.
+
+The unit-price minimum is 2s + 2 ceil(s/2). Separately executing s ordinary
+restored echoes costs 4s. For s=2 the minimum falls from eight to six, with
+both complete partial outputs observed. This comparison does not remove
+any child calls. If a complete array injection costs N scalar additions,
+the saving is 2 floor(s/2) N additions, before any changed routing costs.
+
+## Lower bound
+
+At every time the workspace has the form W_initial + eX, where e is an
+integer. It starts with e=0. Only J_+ and J_- change it, by +1 and -1.
+
+For each label i let A_i and B_i be the integer coefficients in the
+receiver expression
+
+    D = D_initial + sum_i (A_i L_i W_initial + B_i L_i X).
+
+Initially all coefficients are zero. An H_i instruction with sign
+epsilon in {+1,-1} changes A_i by epsilon and B_i by epsilon e.
+Injections change none of these coefficients.
+
+Uniformity in the independently arbitrary maps, together with independent
+arbitrary X and W_initial, makes coefficient comparison legitimate.
+For example, set all maps except L_i to zero and then set either input
+vector to zero. A nonzero scalar multiple of every possible L_i cannot
+vanish in characteristic zero. Thus at checkpoint j necessarily
+
+    A_i = 0 for every i;       B_i = 1 if i <= j, else 0.   (2)
+
+Include time zero as checkpoint zero. In the interval from checkpoint
+i-1 to checkpoint i, A_i changes by zero while B_i changes by one.
+Consequently the net number of forward minus inverse H_i instructions
+in that interval is zero, and some H_i instruction must occur. There
+must be at least one of each sign. Summing these label-specific bounds
+gives the first term of (1), even if other labels occur in those intervals.
+
+Every one of the s checkpoint intervals contains an injection. Otherwise
+e would be constant on that interval, and the changes for every label
+would satisfy Delta B_i = e Delta A_i. Equation (2) would give the
+contradiction 1=0 for its newly observed label.
+
+Let u,v be the total numbers of J_+,J_- instructions, including any
+instructions after the final observation. Exact return of arbitrary W
+requires u=v. Therefore 2u=u+v>=s, so u=v>=ceil(s/2).
+All prices are positive. Adding these simultaneous bounds proves (1).
+
+## Attainment and the first improvement
+
+Start with e=0. For odd i execute the chronological triple
+
+    H_i inverse; J_+; H_i; observe O_i.
+
+Its receiver change is -L_i W_initial + L_i(W_initial+X)=L_i X,
+and it changes e from zero to one. For even i execute
+
+    H_i; J_-; H_i inverse; observe O_i.
+
+Its receiver change is L_i(W_initial+X)-L_i W_initial=L_i X,
+and it changes e from one to zero. These statements preserve arbitrary
+incoming D and every prior completed output. If s is odd, finish with J_-.
+If s is even no final instruction is needed. The final correction changes
+only W, so the last observed output is preserved at return.
+
+The word uses each H_i once in each direction, ceil(s/2) J_+ instructions,
+and ceil(s/2) J_- instructions. It attains every bound above.
+
+For the smallest strict improvement, s=2, the complete word is
+
+    H_1 inverse; J_+; H_1; O_1; H_2; J_-; H_2 inverse; O_2.
+
+At O_1 the workspace is W_initial+X; at O_2 and return it is W_initial.
+Both receiver observations contain the external-source update, without
+any contribution from W_initial. No hidden receiver observation is used.
+
+## Relation to the cyclic question and its limit
+
+PR4860 asks for completed partial external-source echoes, beyond its
+canonical partial-batch record. The present result answers the normalized
+block subproblem: supply a complete canonical batch H_i, price that block
+and its actual inverse, and then apply the schedule above. Ross Richardson's
+PR1287 supplies the cyclic-equivariant batching and ordinary dirty echo;
+PR4860 supplies the canonical normalization tariff. Their costs are included
+in c_i^+,c_i^- and are not re-established here.
+
+The observer must allow the borrowed workspace to retain the shift X at odd
+checkpoints. If W is also required to be restored at every observation,
+the same proof applied within each interval forces at least one injection
+of each sign there. Separate echoes then attain the exact price
+
+    sum_i (c_i^+ + c_i^-) + s(a+b).
+
+This explains the source of the saving and its boundary. It is not a claim
+that canonical cyclic frames may be ignored inside a child, or that a caller
+permits shifted workspace at its observations. No actual selected supplier
+or observer is bound. The five framework assumptions, physical movement,
+native access, ownership, precision, compiler and outer funding remain open.

research/completed-partial-echo/README.md

@@ -0,0 +1,160 @@
+# Completed partial echoes share source injections
+
+This contribution was produced by Nick Petalas. Claim type: scoped algebraic
+construction and exact optimality proof, with finite corroboration. No new
+kappa or physical supplier is claimed.
+
+Two successive complete external-source updates need six macro calls rather
+than eight separate-echo calls, while preserving every observed output and
+restoring arbitrary borrowed data. The new step answers the normalized-block
+part of [PR4860's second open question](https://github.com/CrocSwap/integer-mult-bounds/pull/4860).
+
+For s independently arbitrary linear blocks
+
+    H_i(D,W) = (D + L_i W, W),
+
+let the complete forward/inverse prices be c_i^+,c_i^-. The only additional
+instructions are W += X and W -= X, priced a,b>0. X is immutable; X,W,D
+all start arbitrary. At checkpoint j the observer must see precisely
+D_initial + sum_(i<=j) L_i X. It observes D only. W may retain a source shift
+between checkpoints and must return exactly to its incoming value.
+
+For every s>=1 over a characteristic-zero field, the exact minimum is
+
+    sum_i (c_i^+ + c_i^-) + ceil(s/2) (a+b).
+
+Every uniform word needs at least one use of each H_i direction, and at least
+ceil(s/2) injections of each sign. The same word attains all these bounds,
+even with unequal positive prices. The lower bound permits arbitrary
+repetitions and interleavings of every child label.
+
+The first strict improvement is this chronological word:
+
+```text
+H_1 inverse; W += X; H_1; observe D_initial + L_1 X
+H_2; W -= X; H_2 inverse; observe D_initial + (L_1+L_2) X
+```
+
+The workspace is W_initial+X at the first observation and W_initial at
+return. Each output is already complete when observed. For unit prices,
+the optimum is 2s+2 ceil(s/2), versus 4s for separate restored echoes. No
+child call is removed. With N scalar additions per array injection, the
+copying saving is 2 floor(s/2) N, before any changed routing costs.
+
+[PROOF.md](PROOF.md) supplies the coefficient comparison, injection lower
+bound, attaining word and the contrasting restored-workspace boundary.
+If W must also be restored at every checkpoint, the exact price is instead
+sum_i(c_i^++c_i^-)+s(a+b). Thus the saving requires an explicit observer and
+workspace contract.
+
+## Evidence and reproduction
+
+The standard-library verifier is read-only. From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/completed-partial-echo/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/completed-partial-echo/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/completed-partial-echo
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/completed-partial-echo --check-source-history
+```
+
+Substitute another CPython 3.12 path elsewhere. The last command checks
+publication bytes and declared source ancestry after committing. Expected
+markers are PASS_COMPLETED_PARTIAL_ECHO, PASS_REGISTERED_RESEARCH_PACKAGE
+and PASS_RESEARCH_COMMIT_BYTES.
+
+The checks enumerate:
+
+- 1,600 exact weighted schedule cases through 64 blocks, including unequal
+  forward/inverse prices and rational injection prices. All 64 shared and
+  separate-echo words check every formal checkpoint and final return.
+- 448 literal matrix fixtures, 2,328 independent X/W/D input columns and
+  6,294 complete output observations. These include all scalar map tuples
+  over {-1,0,1} through four blocks, all pairs of binary-entry 2-by-2 maps
+  interpreted in characteristic zero, and rectangular rational fixtures.
+- Eight separately implemented shortest-word searches for one or two blocks
+  with positive integer prices. They permit repeated labels, arbitrary
+  interleavings and source shifts outside {0,1}; they do not assume the
+  attaining schedule. The unit-price minima are four and six.
+- Seventeen rejection controls for omitted directions, reversed injections,
+  missing observations, unreturned workspace, post-observation corruption,
+  dependence on repeated maps, a wrongly canonical workspace boundary, and
+  invalid counts or inexact prices. Checks remain active with optimization.
+
+Each run emits a generated receipt bound to the six package files and both
+declared predecessor text inputs by SHA256. Counts are recomputed, and no
+handwritten receipt is used. The all-length lower bound is the written proof;
+the finite searches do not exhaust arbitrary word lengths or field elements.
+
+## Scope, costs and provenance
+
+Canonical base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8.
+The selected record remains PR6030. TASK.json records the change from the
+formal-interface card to this abstract boundary subproblem. The current
+selected-baseline binding control passed; no selected scientific replay is
+part of this result. SOURCES.json pins the catalogue, selected record and
+two predecessor READMEs. The verifier authenticates the latter without
+importing or replaying their implementations.
+
+Ross Richardson's PR1287 supplies complete cyclic-equivariant batches and
+ordinary dirty echoes. PR4860 supplies the canonical batch tariff and asks
+for completed external-source observations. Here every H_i includes its
+complete normalization, internal scratch restoration and literal inverse
+cost. A block's internal cyclic frame cannot be ignored to claim this saving.
+The new proof concerns the outer observation/injection schedule only.
+
+This is a uniform-word theorem for independently arbitrary maps. Special
+relations among fixed L_i can permit other words. Direct L_i X calls,
+opened child bodies, scalar rescaling, output feedback, additional fields,
+query records, adaptive observations or map-dependent words change the
+alphabet and are outside scope. Observation execution and physical source
+movement have separate costs. No actual native caller, precision/ownership
+contract, tape program, compiler closure, complete signed invoice or outer
+funding is supplied. The five inherited framework assumptions remain.
+Independent human and formal proof-kernel review are unclaimed.
+
+The bounded implementation accepts at most 64 blocks and 384 instructions.
+Exact positive prices are at most 4096 with denominator at most 4096. Payload
+fixtures use at most eight blocks and three coordinates per field. Shortest
+paths use at most two labels, cost 18 and one million queue removals, with
+explicit failure on exhaustion. No recursion, dynamic code, subprocess,
+network access or write occurs in the verifier. Python dynamic allocations
+are a Power of Ten rule-3 deviation; these enforced finite domains bound
+live state. Warning-strict normal and optimized execution supplies interpreter
+diagnostics. There is no fixed-memory implementation or performance claim.
+
+## Open next questions
+
+1. Does one actual cyclic-equivariant caller permit shifted borrowed workspace
+   at a completed output observation? Pin one normalized block, its literal
+   inverse and the observer's read set, then charge every injection and route.
+   That missing physical boundary prevents applying the saving to a supplier.
+2. What is the optimum if cyclic normalization and source injection may be
+   interleaved inside the blocks? Begin with one literal child alphabet and
+   full observer contract. This theorem treats H_i as indivisible and supplies
+   no optimum for that changed alphabet.
+
+## Overlap and credit
+
+The source question is Nick Petalas's PR4860, published October 22, 2026.
+Live open PRs, recent account targets, handoff claims, local reservations,
+main README searches and merged formula/object searches were checked.
+No recent account target cited PR4860. Sparse local notes, unpublished work
+and arbitrary historical diffs remain coverage limits.
+
+The binary partial-output-observation model of commdata2338's PR2020 and
+PR5968 fixes drifting two-XOR children and hides a receiver row. This result
+observes the whole completed receiver after every update and uses normalized
+arbitrary signed linear blocks. Their adapter minima are not recomputed.
+PR3417 serializes independent roots with unobserved outputs; its boundary
+explicitly excludes intermediate observations. The Boolean multilinear
+dirty-input query theorem in PR6393 has one final output and another alphabet;
+it does not price these ordered completed observations.
+
+Credit Ross Richardson / PR1287 for cyclic batching and complete dirty echoes;
+Nick Petalas / PR4860 for the normalized observation question; Sagar Thakrar /
+PR1227, mightyOil / PR1203, Adam Gall / PR1205, Hanson Sun / PR1488, Cinna Davis /
+PR1391, and the retained restoration/echo lineage. Classical linearity and
+signed cancellation are used without a global mathematical-priority claim.
+Frozen predecessor files and their credit are unchanged. New work is
+Apache-2.0.

research/completed-partial-echo/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/cyclic-checkpoint-cost/README.md",
+      "usage": "input",
+      "git_blob": "00208eb7a03097e4b2f0d9cb25bfaa1d145d9b67",
+      "sha256": "f4249104e6418596846ad3d6f05067b83b06d021b20edb0c2961b8a50d46ff0e"
+    },
+    {
+      "path": "research/cyclic-output-restoration/README.md",
+      "usage": "input",
+      "git_blob": "2cb99db015f3b24a1fc31158013cf408b75b0225",
+      "sha256": "fc56e55e76a4d41d9da442ee1af63b4032eb41267a80500814f81027cc0fd087"
+    }
+  ]
+}