Prove the exact shared atom-power crossover with 24 carry states

research/shared-atom-crossover/PROOF.md

@@ -0,0 +1,173 @@
+# Exact crossover at fixed total exponent
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## 1. Contract and cited premise
+
+Fix integers I>=1 and w>=1. Three distinct owned Count outputs have borrowed,
+canonical, unsigned I-bit exponents e_0,e_1,e_2, each in [0,2^I-1]. The fixed
+radix is q and the admitted modulus is q^w. Compare the original and shared
+atom-power methods of Tekalign / tekuuu's PR4077, at
+90b658330f0357975337b41d67927ae84b72c851. Their successful-input equivalence,
+blank-counter lifecycle and complete source-action difference in PROOF.md
+sections 3 and 4 are cited premises. This proof does not verify those premises.
+
+An action here is one record, residue-Word or index-Word read, write or unit
+move, with unit weight for each of those nine kinds. Let rho be the sum of
+one complete radix validator's residue actions, including its cleanup. It is
+an input to the theorem, not an estimated or newly measured source cost.
+No physical exchange rate among the action kinds is assumed.
+
+Write E=sum e_j, k=#{j:e_j>0}, S=sum popcount(e_j), and
+B=sum bitlength(e_j), using bitlength(0)=0. The main theorem concerns E>=2;
+sections 2 and 4 also treat E=0 and E=1.
+
+## 2. Complete scalar cost identity
+
+For a positive exponent e with b=bitlength(e), the cited construction tariff
+J, rundown R, probe P and index-copy C have the following scalar totals:
+
+```
+J(e,I) = 9I - 4b + 8,
+R(e,I) = 15e - 5 popcount(e) + 9I + 29,
+P(e,I) = 9I + b + 20,
+C(I)   = 5I + 7.
+```
+
+These follow by adding the three components of each cited vector. In R,
+the +4b from the decrement sum cancels the -4b in J. A positive probe
+closes its unconsumed counter, with scalar cost 5b+12. For e=0, the cited
+R(0,I)=P(0,I), so the original rundown and new probe cancel exactly.
+
+For E>0, PR4077 section 4 therefore gives the exact old-minus-new scalar
+saving
+
+```
+Delta = (E-1) rho - H(e_0,e_1,e_2;I,w),
+H     = 15(w-1)E - 5(w-1)S + B + k(14wI + 36w - 9).       (1)
+```
+
+Indeed the non-radix overhead is
+sum_(e_j>0) [(w-1)R(e_j,I) + P(e_j,I) + w C(I)]. Substitution yields (1).
+This retains every negative savings lane in the original difference before
+summing. Output Count operations cancel by the cited successful-input
+contract. The identity adds no uncharged runtime selector.
+
+For E=0 both methods have the same probes/rundowns, no radix traversal and
+no new index copies, hence Delta=0. Formula (1)'s (E-1)rho term must not be
+used in that case. For E=1, exactly one exponent is one, and
+H=14wI+46w-18>0; Delta=-H. Strict saving is impossible in both cases.
+
+## 3. An exact maximum with at most 24 states per bit
+
+Let H_max(I,w,E) maximize H over all ordered I-bit triples with sum E.
+Every integer E in [0,3(2^I-1)] has such a triple. Put
+
+```
+C = 14wI + 36w - 9,
+Q(e) = B - 5(w-1)S + Ck.
+```
+
+The first term 15(w-1)E in H is fixed. The following maximum-weight
+binary carry calculation computes max Q and one attaining triple.
+
+Process bit positions i=I-1,...,0 from most significant to least
+significant. A state is (c,A), where c in {0,1,2} is the outgoing carry
+from bit i to bit i+1, and A is the three-bit mask of exponents with an
+already nonzero higher prefix. Start at (floor(E/2^I),0), with score zero.
+For each proposed operand-bit mask u in {0,...,7}, put
+
+```
+c' = E_i + 2c - popcount(u),
+A' = A OR u.
+```
+
+Discard c' outside {0,1,2}. Otherwise move to (c',A') with added score
+
+```
+popcount(A') - 5(w-1)popcount(u)
+  + C [popcount(A')-popcount(A)].                         (2)
+```
+
+Keep the largest score per new state and an attaining prefix. After the
+last bit accept only carry zero; maximize over its active masks. Add
+15(w-1)E to obtain H_max. Ties may retain any attaining prefix.
+
+To prove the arithmetic constraint, ordinary column addition says
+popcount(u)+c'=E_i+2c. The initial high carry and final zero low carry
+make these equations equivalent to the exact unreduced sum of the three
+I-bit operands. Conversely, every such triple supplies a unique path of
+bit masks and carries. Thus this procedure omits no triple and adds none.
+
+For each operand e, its active flag after processing bit i is one exactly
+when e>=2^i. Summing that flag over all I positions gives bitlength(e).
+The bit-mask populations sum to S. Newly active flags telescope to k.
+Consequently the total of (2) is exactly Q(e).
+
+Two prefixes with the same (c,A) have the same legal suffixes and the
+same additional scores. Keeping only the larger prefix score therefore
+preserves a global optimum. Induction on the processed positions proves
+exactness. The stored witness attains it. There are at most 3*8=24 states
+and at most 8 proposed masks per state at every bit, so at most 192I mask
+trials suffice. This is an arithmetic-operation bound. Integer bit costs,
+witness storage and execution of the encoded source caller are separate.
+The reference retains at most two state layers, each with 24 records and
+three I-bit witness integers per record.
+
+## 4. Sharp uniform affordability criterion
+
+For E>=2, the shared method strictly saves scalar source actions for
+EVERY ordered I-bit exponent triple of sum E if and only if
+
+```
+(E-1)rho > H_max(I,w,E).                                (3)
+```
+
+Sufficiency follows from (1) and the maximum. Necessity follows by
+substituting its attaining triple. In particular, for integral rho the
+least admissible threshold is
+
+```
+rho_min = floor(H_max(I,w,E)/(E-1)) + 1.                 (4)
+```
+
+Equality in (3) is not strict saving. The theorem is parametric in rho;
+it does not assert that every small integer rho is realized by an actual
+radix validator.
+
+The actual child-extent exponents of PR4077 section 5 are
+(a,b-a-c,2n-b-c), whose sum is E=2(n-c). When all three fit I bits,
+substituting this E into (3) gives a uniform sufficient condition without
+knowing their placement. Its necessity is over ALL sum-E triples. Actual
+Layout guards, the external gap and native child placements can restrict
+that set, so no sharpness claim for those narrower geometries follows.
+
+## 5. First explicit strict improvement
+
+At I=4,w=1,E=10, formula (1) reduces to H=B+83k. If k<=2, then H<=174.
+For k=3, having B>=9 would require either lengths at least (3,3,3),
+(4,3,2), or (4,4,1), up to order. Their minimum positive sums are 12,
+14 and 17 respectively. All exceed 10. Thus B<=8. The triple (4,4,2)
+has B=8,k=3, so H_max=257. Equation (4) gives rho_min=29.
+
+At rho=29 the minimum saving is 9*29-257=4 actions. At rho=28 the same
+witness loses five actions. The elementary separate bounds k<=3 and
+B<=3I instead give H<=261 and only certify integral rho>=30. The exact
+sum constraint therefore certifies the additional value rho=29. That
+coarse comparison is derived here; it is not a previously published
+PR4077 threshold or a newly measured physical speedup.
+
+## 6. Scope and next obligations
+
+The new result is the exact sum-conditioned cost maximum and crossover,
+conditional on the cited lane tariffs. Classical binary digit dynamic
+programming supplies the method. Finite checks corroborate its new maximum;
+they neither audit PR4077's implementation nor replace this all-size proof.
+
+A runtime guard would have to obtain or encode rho and pay for selection.
+A physical tariff would have to price the nine action kinds. A complete
+caller still needs Context/directory composition, storage and backing,
+source admission, payload, control, precision and restoration obligations.
+All five selected framework assumptions remain. No complete multiplication
+theorem, supplier admission or new kappa is claimed. Independent human and
+formal proof-kernel review are unclaimed.

research/shared-atom-crossover/README.md

@@ -0,0 +1,132 @@
+# Exact affordability of shared atom powers at fixed total exponent
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written cost proof with exact finite corroboration.
+No new kappa or selected-frontier change is claimed.
+
+For Tekalign / tekuuu's [PR4077](https://github.com/CrocSwap/integer-mult-bounds/pull/4077)
+shared atom-power interface, the total exponent alone can certify that every
+placement saves source actions. The new result computes the sharp threshold
+for all three equal-width exponents with that total. It answers the package's
+open parameter-region question using its exact tariffs as cited premises.
+No predecessor executable or scientific replay is run.
+
+For I-bit exponents, radix width w, sum E>0, positive count k, total binary
+population S and total bitlength B, the exact old-minus-new scalar saving is
+
+```
+Delta = (E-1)rho - H,
+H = 15(w-1)E - 5(w-1)S + B + k(14wI+36w-9).
+```
+
+Here rho is the complete residue read/write/move total of one radix traversal.
+Every record, residue and index action has unit weight. For E>=2, a binary
+carry maximum with at most 24 states per bit computes H_max and an attaining
+triple. Strict saving for every sum-E triple holds exactly when
+`rho > H_max/(E-1)`. The all-zero case ties, and total one always loses.
+[PROOF.md](PROOF.md) establishes the uniform theorem, carry invariant and
+strict endpoint. The operation count is at most 192I mask trials, with
+integer arithmetic and witness costs stated separately.
+
+The first explicit case has I=4,w=1,E=10. Its exact maximum is 257, attained
+by (4,4,2), so integral rho>=29 suffices and is sharp. The simpler separate
+bounds on k and B only certify rho>=30. At rho=29 every such triple saves
+at least four actions; at rho=28 the attaining triple loses five. These are
+parametric tariffs, not claims that a validator of cost 29 was executed.
+
+For actual child extents, E=2(n-c), where n is the parent width and c is
+the child width. The theorem supplies a sufficient condition for every
+admitted placement fitting I bits. Exact necessity concerns the larger
+sum-conditioned triple domain; actual source geometry may exclude a witness.
+No runtime dispatch, physical action exchange rate or full caller improvement
+is supplied. Count output work cancels by the cited source contract.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/shared-atom-crossover
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/shared-atom-crossover/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/shared-atom-crossover/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/shared-atom-crossover --check-source-history
+```
+
+Any CPython 3.12 executable can replace the absolute interpreter path. Expected
+markers are `PASS_SHARED_ATOM_CROSSOVER`, `PASS_REGISTERED_RESEARCH_PACKAGE`
+and `PASS_RESEARCH_COMMIT_BYTES`. The final command needs committed bytes and
+full Git history. The direct checker also works in a Git-free package export.
+It writes nothing and prints a freshly generated receipt bound to all seven
+package source/metadata files. No success receipt is handwritten.
+
+The new carry algorithm is compared with direct tariff maximization over all
+149,792 ordered triples at I=1..5 and w in {1,2,3,7}. All 704 maxima, including
+zero totals, agree. `oracle.py` applies the cited vector costs directly,
+without importing the new carry algorithm. These checks establish agreement
+on the stated finite domain, not independent review of the inherited tariffs.
+The sharp strict boundary, E=0/E=1, an undercut maximum, an unattainable
+combination of separate bounds, larger-width attaining witnesses and twelve
+invalid arguments are checked. Explicit exceptions retain every check under
+optimized Python. The written proof supplies the universal quantifiers.
+
+## Scope, sources and credit
+
+Canonical base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8,
+selected PR6030 at kappa .003125804. The selected source-binding orientation
+passed; it is metadata orientation, not a scientific selected replay.
+The formal-interface-lemma card explicitly changes to this written cost
+criterion rather than a proof-assistant theorem or discharge of a selected
+assumption. [TASK.json](TASK.json) records that change.
+
+Credit Tekalign / tekuuu for PR4077's shared encoded atom powers, actual
+child-extents adapter, exact vector tariffs and open affordability question.
+David Arias / PR2753, Jose Manuel / jmbarrancoml, ToikY / PR4025,
+ywz65 / PR2590, Chris R / Clear1nsight / PR4062 and their retained caller,
+record and source contributors retain credit. Binary digit dynamic programming
+and scalar tariff algebra are classical; no global literature-priority claim
+is made. The new result is this exact sum-conditioned maximum and its sharp
+application to the stated interface.
+
+[SOURCES.json](SOURCES.json) binds the unchanged main-tree predecessor proof
+and README as historical provenance. They are not executable dependencies.
+[Advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371189).
+Live open/account PRs, handoffs, active Discussions, main-tree object/formula
+searches and merged searches were checked. The broader cache covered 521 open
+PRs and 6,530 Discussion records, while local notes were sparse. Unpublished
+work, arbitrary historical diffs and global literature priority remain outside
+that coverage. Search absence is not a novelty certificate.
+
+The theorem is conditional on the cited successful-input source tariffs.
+Physical allocator/control costs, an encoded selector, actual validator
+prices, full Context/payload composition, stock, precision and supplier/outer
+admission are unrun obligations. No predecessor audit, selected cold replay,
+Lean or Docker run is part of this contribution. All five selected assumptions
+remain. Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Can actual source geometry reduce the sum-conditioned maximum further?
+  Start with one pinned native child family, its legal placements and external
+  gap constraints. The present attaining triple need not be a legal child.
+- Can an encoded caller use the crossover without spending its gain on
+  selection? Start with a source-bound lower bound for rho and a fixed
+  parameter region. A host calculation of the threshold is not a paid
+  runtime decision or a complete physical caller.
+
+## Code bounds
+
+The mathematical proof permits all positive I,w; the reference API caps I at
+4096 and w below 2^64. The exhaustive oracle caps I at five and four fixed w
+values. Carry layers have at most 24 records and at most 192 transitions per
+bit; each record holds three bounded-width witness integers. Source reads are
+capped at 128 KiB per file. Functions are below 60 lines. There is no recursion,
+subprocess, network, dynamic code generation or mutable shared state. The
+checker uses normal and optimized warning-strict execution as its available
+Python diagnostics; no separate type checker is claimed as run.
+
+Power-of-Ten rule 3 deviation: Python and its standard library allocate managed
+integers, tuples, dictionaries and JSON. The fixed API limits, two bounded state
+layers, a 94-entry oracle maximum table and streamed triple enumeration bound
+live collections. This is not a fixed-pool, allocator-internals or real-time
+claim. Larger domains must revise those caps before use. Standard-library
+iterator and JSON dispatch have fixed targets; the code defines no callbacks.

research/shared-atom-crossover/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/encoded-child-spectators/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "0e4bbcf04f1a2502bae7f47d5376a72de74fb36a",
+      "sha256": "cf439a2ffe2bc8521377225400306df7c829af194dc6d8614a4383c7741616a2"
+    },
+    {
+      "path": "research/encoded-child-spectators/README.md",
+      "usage": "provenance",
+      "git_blob": "c4373db5f3f22b91f51a13df62a0a5329580cc83",
+      "sha256": "05ab321b1ec220375115ca28fc1113edafd530d4e147e09e8534b7172661df77"
+    }
+  ]
+}