Give exact fixed-weight packed-bit repair counts (no new κ)

research/packed-fixed-weight-repair/PROOF.md

@@ -0,0 +1,174 @@
+# A rational series for fixed-weight agreement
+
+## Cited premise and the new claim
+
+Use the original packed selected-bit primitive with `B=2^K`, `K>=6`,
+`m=f-1` used source bits and `0<=rho<K`. Fix the source pattern
+`c=(c_0,...,c_(m-1))`. Both dirty fields range over their complete sets.
+Hanson Sun / bbMisk's PR #1245 proves that if the one positions are
+`j_1<...<j_w`, the agreement fraction is
+
+\[
+ a(c)=\prod_{t=1}^{w-1}(1-2B^{-(j_{t+1}-j_t)}).
+\]
+
+For `w<=1` this is an empty product, equal to one. That theorem, including
+its dirty restoration and inactive-suffix statements, is a dependency.
+It is not proved or replayed here. The new claim concerns the sum
+
+\[
+ A_{m,w}=\sum_{c\in\{0,1\}^m,\ |c|=w} a(c).
+\]
+
+For any real `B>=4`, these numbers have formal generating function
+
+\[
+ F(z,u)=\sum_{m\ge0}\sum_{w=0}^m A_{m,w}z^m u^w
+ =\frac{B+(2u-1)z}
+ {B-(B+1+(B-2)u)z+(1-u)z^2}.                 \tag{1}
+\]
+
+The formal-series argument works over the rational functions in `B` as
+well. For the binary gadget, the exact forward failure density, and also
+the density of its correction-permutation support on the union of these
+complete fibers, is
+
+\[
+ \delta_{m,w}=1-\frac{A_{m,w}}{\binom mw}.     \tag{2}
+\]
+
+Every source pattern has the same number of dirty-field values, so uniform
+sampling of source patterns makes their fractions average with equal
+weights. The predecessor's support-permutation argument acts within each
+source fiber and gives the same correction-support fraction. Unused source
+bits, inactive suffixes and spectators must have equal multiplicities for
+these fibers, or the source weights must be specified separately.
+
+## Unique decomposition by gaps
+
+There is exactly one all-zero word of every length, contributing
+`1/(1-z)` to `F`. A word with `w>=1` has a unique decomposition into:
+
+* a nonnegative number of leading zeros;
+* its first one;
+* `w-1` gaps of lengths `d>=1` from one to the next;
+* a nonnegative number of trailing zeros.
+
+A gap of length `d` accounts for `d-1` zeros and the next one, so it
+contributes length `d` and agreement factor `1-2B^-d`. Define
+
+\[
+ G(z)=\sum_{d\ge1}(1-2B^{-d})z^d
+ =\frac{z}{1-z}-\frac{2z}{B-z}
+ =\frac{z(B-2+z)}{(1-z)(B-z)}.
+\]
+
+Leading and trailing zeros contribute two factors `1/(1-z)`. The first
+one contributes `uz`, and each subsequent gap contributes `uG(z)`. Thus
+
+\[
+ F(z,u)=\frac1{1-z}
+       +\frac{uz}{(1-z)^2}\sum_{k\ge0}(uG(z))^k
+ =\frac1{1-z}+\frac{uz}{(1-z)^2(1-uG(z))}.    \tag{3}
+\]
+
+Each coefficient has finitely many decompositions, so all products and
+the geometric series are legitimate formal power series. Substituting
+`G` into (3) gives numerator
+
+\[
+ (1-z)(B-z)-uz(B-2+z)+uz(B-z)
+ =(1-z)(B-z+2uz).
+\]
+
+Cancel the formal unit `1-z` and expand the denominator. This gives (1).
+No source independence assumption, random gap approximation or numerical
+interpolation enters this identity.
+
+## Coefficients, recurrence and exact finite counts
+
+The length-zero and length-one polynomials are `A_0(u)=1` and
+`A_1(u)=1+u`. Multiplying (1) by its denominator and comparing every
+coefficient of length `m>=2` gives
+
+\[
+ B A_{m,w}=(B+1)A_{m-1,w}+(B-2)A_{m-1,w-1}
+             -A_{m-2,w}+A_{m-2,w-1}.         \tag{4}
+\]
+
+Entries outside `0<=w<=m` are zero. This proves the recurrence at every
+length and weight. At fixed length `m`, (4) needs only the two previous
+rows and at most a quadratic number of arithmetic operations to produce
+all rows up to `m`. This is an arithmetic-operation count, not a bit-time
+bound for physical execution.
+
+For an integer radix, put `S_0=[1]` and, for `m>=1`,
+`S[m,w]=B^(m-1) A[m,w]`. These are integers. Indeed the gap-product
+denominator for one pattern is `B^(j_w-j_1)`, and its span is at most
+`m-1`. The initial rows are
+
+```text
+S_1 = [1,1],    S_2 = [B,2B,B-2].
+```
+
+For `m>=3`, multiply (4) by `B^(m-2)` to obtain the integer recurrence
+
+```text
+S[m,w] = (B+1)S[m-1,w] + (B-2)S[m-1,w-1]
+         - B S[m-2,w] + B S[m-2,w-1].
+```
+
+In the binary gadget, there are `B^(2m)` pairs of active dirty digits per
+source pattern. Their total agreeing count at weight `w` is therefore
+`B^(m+1) S[m,w]` for `m>=1`; for `m=0` it is one. Spectator multiplicities
+multiply agreement and total size equally. This converts the fractions
+into actual finite address counts whenever the declared complete-fiber
+domain is supplied.
+
+At `m=3,w=2`, the patterns `110,011,101`, written low bit first, have
+agreement `1-2/B`, `1-2/B`, `1-2/B^2`. Hence
+
+\[
+ \delta_{3,2}=\frac{4/B+2/B^2}{3}.
+\]
+
+For `B=64`, this is `43/2048`, distinct from both the unrestricted mean
+and the fixed-weight worst case. This is a new exact aggregation of the
+predecessor's formula; its per-pattern values are inherited.
+
+## Verification boundary and implementation bounds
+
+The verifier compares the new integer recurrence with direct enumeration
+of the cited gap product at every weight through length 14 and radices
+`4,6,64,128`. It also checks empty, zero-weight, one-bit, all-ones and
+unrestricted-source marginal identities through length 128. These checks
+corroborate (1), and do not audit the eight-gate program or prove its
+gap-product premise. The written unique-decomposition argument supplies
+the all-parameter conclusion. The complete multiplier, physical layout,
+native delivery, uniform compiler, precision/tape and recovery remain
+outside scope. There is no new kappa or selected-frontier update.
+
+All verifier loops have fixed finite bounds. The arithmetic API accepts
+only even integer radices from 4 to 65536 and lengths at most 128; the
+enumeration uses at most `2^14` patterns per length and radix. Every
+function is shorter than 60 lines, calls are direct, there is no recursion
+or dynamic code, and checks use explicit exceptions under both normal and
+optimized Python. No compiler or external library is needed; registered
+commands enable warning errors. Python runtime allocation is a deviation
+from fixed-allocation execution: at most `129^2` integer table cells are
+live per recurrence, their values have at most 2177 bits since
+`0<=S[m,w]<=2^m B^(m-1)`, and enumerated patterns are consumed one at a
+time. This does not bound the interpreter's internal allocator overhead.
+If these API limits are raised, the capacity and replay-time bounds must
+be reconsidered. The package has no steady-state or constant-allocation
+claim.
+
+The default verifier only reads its six named source files and receipt.
+The explicit receipt writer creates one new path exclusively, refuses an
+existing path, checks the write length and closes the handle on all exits.
+No file, network or process lifetime is hidden in the arithmetic routines.
+
+The gap-product theorem and classical generating-series operations retain
+their authors' credit. The new fixed-weight series and recurrence were
+produced by Nick Petalas. Independent human and formal proof-kernel review
+are unclaimed.

research/packed-fixed-weight-repair/README.md

@@ -0,0 +1,112 @@
+# Exact fixed-weight packed-bit repair counts
+
+This scoped proof gives the exact mean repair density of the original
+eight-rotation packed-bit gadget when its `m` used source bits are uniform
+among the `binom(m,w)` patterns of weight `w`. Both dirty fields must remain
+complete and independent of that source choice. No new kappa is claimed.
+
+Let `A[m,w]` be the sum of the agreement fractions over those source patterns.
+The new bivariate generating function is
+
+```text
+sum A[m,w] z^m u^w
+    = (B + (2u-1)z) / (B - (B+1+(B-2)u)z + (1-u)z^2).
+```
+
+Consequently the exact slice failure density is
+`1 - A[m,w]/binom(m,w)`. The initial polynomials are `A[0](u)=1` and
+`A[1](u)=1+u`. For `m>=2`, with out-of-range indices interpreted as zero,
+
+```text
+B A[m,w] = (B+1) A[m-1,w] + (B-2) A[m-1,w-1]
+           - A[m-2,w] + A[m-2,w-1].
+```
+
+At `B=64,m=3,w=2`, the three patterns give mean failure `43/2048`.
+The predecessor's fixed-weight worst case is `1/32`, and its unrestricted
+source average is `255/16384`. Neither equals this slice mean. At
+`B=64,m=10,w=2`, the exact mean is `57087705027109/9007199254740992`.
+These are address fractions, not measured runtime improvements.
+
+[PROOF.md](PROOF.md) derives the rational function by summing the cited
+gap product over leading zeros, trailing zeros and consecutive-one gaps.
+The algebraic identity holds for real `B>=4`; the inherited binary gadget
+uses `B=2^K`, `K>=6`, `m=f-1` and its allowed offset. The proof handles
+`m=w=0` and weights zero and one.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/packed-fixed-weight-repair
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/packed-fixed-weight-repair --check-source-history
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/packed-fixed-weight-repair/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/packed-fixed-weight-repair/verify.py
+```
+
+Expected markers are `PASS_PACKED_FIXED_WEIGHT_REPAIR` and
+`PASS_REGISTERED_RESEARCH_PACKAGE`. The standalone verifier enumerates
+every source pattern through length 14 at `B=4,6,64,128`, and compares each
+weight total with the new recurrence. It checks the boundary rows through
+length 128 and three wrong aggregation shortcuts. Seven invalid inputs
+must also reject. The nonbinary radices are algebraic controls, not new
+binary gadget parameters. [RESULT.json](RESULT.json) is a generated
+receipt bound to the proof, code and metadata hashes. Default replay writes
+nothing and works without Git or any predecessor package.
+
+The universal claim rests on the written combinatorial proof, conditional
+on the cited predecessor theorem. The finite enumeration checks the new
+aggregation, not the predecessor's digit program, transition table or
+mathematical correctness. No predecessor verifier is run or imported.
+
+## Scope and sources
+
+Canonical base `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8.
+The `uniform-transfer-audit` card changes scope to this exact source-mixture
+side result. It does not discharge one of the selected five assumptions.
+The selected baseline source-binding check passed after materializing its
+omitted inputs. No selected supplier cold replay was run.
+
+Hanson Sun / bbMisk's [PR #1245](https://github.com/CrocSwap/integer-mult-bounds/pull/1245)
+already proves each source's gap-product law, the fixed-weight extrema and
+the unrestricted average. Those are cited premises. This package adds the
+exact fixed-weight mean and its coefficient recurrence. Precious / Kyu's
+[#773](https://github.com/CrocSwap/integer-mult-bounds/pull/773) supplies the
+matching-prefix approach and complete-rectangle count; Aryan Sudhir's
+[#735](https://github.com/CrocSwap/integer-mult-bounds/pull/735) supplies the
+earlier sufficient guard envelope. Their retained manuscript and primitive
+lineage stay credited. [SOURCES.json](SOURCES.json) binds the cited README
+as historical provenance, with no live executable dependency.
+
+This supplies a count for a proposed source-restricted caller, not that
+caller. Restricted dirty fields, nonuniform sampling within a weight slice,
+or source-dependent dirty layouts do not meet the count's hypotheses.
+Source access, layout admission, all scans, correction sorting, reinsertion,
+restoration, precision and the complete physical bill remain obligations.
+No finite certificate or scoped proof here establishes a complete
+multiplication theorem or changes the selected frontier.
+
+Live claims, open PRs, merged PRs and main README searches were checked
+before reservation and publication. The overlap helper also reports its
+sparse local-note coverage; no-match searches are not novelty certificates.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228368)
+states this scope. The first verified identity ended the research.
+
+## Open next questions
+
+1. Can an actual paid caller preserve complete dirty fields while supplying
+   uniform fixed-weight source slices? Trace one invocation and include the
+   source partition, address descriptors and all movement costs. No such
+   physical layout is supplied here; its cost can outweigh the repair saving.
+2. What is the sparse-weight asymptotic of this exact count? Start with the
+   coefficient formula at fixed `w` and increasing `m`. This could quantify
+   the possible benefit of a source-restricted caller, but it would still
+   leave that caller and its complete bill open.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Apache-2.0. Credit Hanson
+Sun, Precious Oyetunji and Aryan Sudhir for the predecessor results above,
+and the original manuscript authors for the eight-rotation gadget.
+Independent human and formal proof-kernel review are unclaimed.

research/packed-fixed-weight-repair/RESULT.json

@@ -0,0 +1,44 @@
+{
+  "boundary_rows": 516,
+  "checked_slices": 480,
+  "claim_type": "scoped proof conditional on the cited gap-product theorem",
+  "enumerated_source_patterns": 131068,
+  "examples_B64": [
+    {
+      "failure_density": "43/2048",
+      "m": 3,
+      "w": 2
+    },
+    {
+      "failure_density": "57087705027109/9007199254740992",
+      "m": 10,
+      "w": 2
+    },
+    {
+      "failure_density": "34750585028775/562949953421312",
+      "m": 10,
+      "w": 5
+    },
+    {
+      "failure_density": "8744749928161/35184372088832",
+      "m": 10,
+      "w": 10
+    }
+  ],
+  "maximum_enumerated_length": 14,
+  "negative_controls": 10,
+  "radices": [
+    4,
+    6,
+    64,
+    128
+  ],
+  "sha256": {
+    "PROOF.md": "10f1dbe7d2cb0200ec7e523843d08a22ee6902fbef458ab3a21024bd9e4133d9",
+    "README.md": "60973d9671dd6c5437a44ee111242d86c596e8e9fb02f1f9c6b197103795c0af",
+    "SOURCES.json": "df199d21e9923501e530e8c56fb8e002f363d538023b6cb406ed64f0649767b4",
+    "TASK.json": "9035f2e0f135b3edbe85b233d7da3b71aec7e82bcc97f301abcd22060b23988b",
+    "VERIFY.json": "f4537982f2389078593d8e81f6a3e898a8d246f99d2fdae476e6483af9d932a4",
+    "verify.py": "fb8b9d0c48ea9ce01780534d1b87ae1404adc64de423d7cfe94c8b0d96efc816"
+  }
+}

research/packed-fixed-weight-repair/SOURCES.json

@@ -0,0 +1,25 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/packed-source-fibers-seed62/README.md",
+      "usage": "provenance",
+      "git_blob": "ada24b542ef4d52bf6dbca84b97cca966e2fbd09",
+      "sha256": "b950f845d8f09f282c25429fd39dc22c512d15975203304fef9a1ce75b3c1cc5"
+    }
+  ],
+  "dependency_note": "The PR1245 README states the gap-product theorem used as a mathematical premise. No predecessor code is executed or imported."
+}