From dbaa509654065721bd4acaddc316ffb5421be7c0 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 22:00:02 +0000 Subject: [PATCH] feat(research): count fixed-weight packed-bit repair exactly --- research/packed-fixed-weight-repair/PROOF.md | 174 ++++++++++++++++++ research/packed-fixed-weight-repair/README.md | 112 +++++++++++ .../packed-fixed-weight-repair/RESULT.json | 44 +++++ .../packed-fixed-weight-repair/SOURCES.json | 25 +++ research/packed-fixed-weight-repair/TASK.json | 95 ++++++++++ .../packed-fixed-weight-repair/VERIFY.json | 34 ++++ research/packed-fixed-weight-repair/verify.py | 161 ++++++++++++++++ 7 files changed, 645 insertions(+) create mode 100644 research/packed-fixed-weight-repair/PROOF.md create mode 100644 research/packed-fixed-weight-repair/README.md create mode 100644 research/packed-fixed-weight-repair/RESULT.json create mode 100644 research/packed-fixed-weight-repair/SOURCES.json create mode 100644 research/packed-fixed-weight-repair/TASK.json create mode 100644 research/packed-fixed-weight-repair/VERIFY.json create mode 100644 research/packed-fixed-weight-repair/verify.py diff --git a/research/packed-fixed-weight-repair/PROOF.md b/research/packed-fixed-weight-repair/PROOF.md new file mode 100644 index 0000000000..2369b23058 --- /dev/null +++ b/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=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. diff --git a/research/packed-fixed-weight-repair/README.md b/research/packed-fixed-weight-repair/README.md new file mode 100644 index 0000000000..630acbcf2a --- /dev/null +++ b/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. diff --git a/research/packed-fixed-weight-repair/RESULT.json b/research/packed-fixed-weight-repair/RESULT.json new file mode 100644 index 0000000000..afd31d048c --- /dev/null +++ b/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" + } +} diff --git a/research/packed-fixed-weight-repair/SOURCES.json b/research/packed-fixed-weight-repair/SOURCES.json new file mode 100644 index 0000000000..721f885a8a --- /dev/null +++ b/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." +} diff --git a/research/packed-fixed-weight-repair/TASK.json b/research/packed-fixed-weight-repair/TASK.json new file mode 100644 index 0000000000..2a31dc1639 --- /dev/null +++ b/research/packed-fixed-weight-repair/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact mean packed-bit repair density on uniform fixed-Hamming-weight source slices, conditional on the cited per-source gap product.", + "scope_change_reason": "The source-restricted caller left open by PR1245 first needs an exact source-mixture count. This supplies that count as a side result, rather than auditing a predecessor or discharging a selected assumption.", + "bottleneck_link": "A source-restricted paid caller needs its true correction fraction. The new coefficient formula supplies one accounting input but leaves its layout and full cost open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified fixed-weight aggregation identity; package it without pursuing a caller or further asymptotics.", + "outcome": "completed", + "evidence": "PROOF.md gives the quantified derivation; RESULT.json records exhaustive aggregation checks and source hashes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a physical caller supply uniform fixed-weight source slices while preserving complete dirty fields?", + "why_it_matters": "Only a paid admissible caller can turn the exact fraction into a physical improvement.", + "first_step": "Trace one full invocation, including source partition descriptors, movement, correction and return.", + "blocked_by": "No such source-restricted physical layout and complete bill are supplied." + }, + { + "question": "What is the sparse-weight asymptotic of the exact slice fraction?", + "why_it_matters": "It could quantify how much repair work a sparse source caller might avoid.", + "first_step": "Extract fixed-w coefficients and study increasing source length.", + "blocked_by": "Intentionally deferred after the first exact result; does not itself supply a caller." + } + ], + "environment": { + "implementation": "CPython", + "version": "3.12.15", + "interpreter": "~/git/integer-mult-bounds/.venv/bin/python3.12", + "dependencies": "standard library only" + } +} diff --git a/research/packed-fixed-weight-repair/VERIFY.json b/research/packed-fixed-weight-repair/VERIFY.json new file mode 100644 index 0000000000..f52c8f9902 --- /dev/null +++ b/research/packed-fixed-weight-repair/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive source-product aggregation through length 14, all boundary rows through 128, three wrong-aggregation and seven invalid-input controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact receipt and explicit failure checks under optimized Python." + } + ] +} diff --git a/research/packed-fixed-weight-repair/verify.py b/research/packed-fixed-weight-repair/verify.py new file mode 100644 index 0000000000..fb2dfbd2b1 --- /dev/null +++ b/research/packed-fixed-weight-repair/verify.py @@ -0,0 +1,161 @@ +#!/usr/bin/env python3 +"""Exact fixed-weight aggregation of the cited packed-bit gap product.""" + +import argparse +from fractions import Fraction +import hashlib +from itertools import combinations +import json +from math import comb +from pathlib import Path + + +MAX_LENGTH = 128 +MAX_RADIX = 65536 +EXHAUSTIVE_LENGTH = 14 +RADICES = (4, 6, 64, 128) +PACKAGE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def agreement_rows(length, radix): + """Return S[m,w] = B**max(m-1,0) times the total agreement.""" + require(type(length) is int and 0 <= length <= MAX_LENGTH, + "length must be an integer in [0,128]") + require(type(radix) is int and 4 <= radix <= MAX_RADIX and radix % 2 == 0, + "radix must be an even integer in [4,65536]") + rows = [[0] * (length + 1) for _ in range(length + 1)] + rows[0][0] = 1 + if length >= 1: + rows[1][0:2] = [1, 1] + if length >= 2: + rows[2][0:3] = [radix, 2 * radix, radix - 2] + for m in range(3, length + 1): + for w in range(m + 1): + value = (radix + 1) * rows[m - 1][w] - radix * rows[m - 2][w] + if w: + value += ((radix - 2) * rows[m - 1][w - 1] + + radix * rows[m - 2][w - 1]) + require(value >= 0, "negative agreement count") + rows[m][w] = value + return rows + + +def pattern_total(length, weight, radix): + """Enumerate the predecessor's product, without its code or automaton.""" + total = 0 + patterns = 0 + for positions in combinations(range(length), weight): + product = 1 + span = 0 + for index in range(1, weight): + gap = positions[index] - positions[index - 1] + product *= radix ** gap - 2 + span += gap + total += product * radix ** (max(length - 1, 0) - span) + patterns += 1 + require(patterns == comb(length, weight), "incomplete source enumeration") + return total, patterns + + +def density(rows, length, weight, radix): + require(0 <= weight <= length < len(rows), "invalid slice") + denominator = radix ** max(length - 1, 0) * comb(length, weight) + return 1 - Fraction(rows[length][weight], denominator) + + +def exhaustive_check(): + patterns = 0 + slices = 0 + for radix in RADICES: + rows = agreement_rows(EXHAUSTIVE_LENGTH, radix) + for length in range(EXHAUSTIVE_LENGTH + 1): + for weight in range(length + 1): + total, count = pattern_total(length, weight, radix) + require(total == rows[length][weight], + f"coefficient mismatch at B={radix},m={length},w={weight}") + patterns += count + slices += 1 + return {"enumerated_source_patterns": patterns, "checked_slices": slices, + "radices": list(RADICES), "maximum_enumerated_length": EXHAUSTIVE_LENGTH} + + +def boundary_check(): + cases = 0 + for radix in RADICES: + rows = agreement_rows(MAX_LENGTH, radix) + for length in range(MAX_LENGTH + 1): + scale = radix ** max(length - 1, 0) + require(rows[length][0] == scale, "zero-weight boundary") + if length: + require(rows[length][1] == length * scale, "one-bit boundary") + require(rows[length][length] == (radix - 2) ** (length - 1), + "all-ones boundary") + require(sum(rows[length]) == 2 * (2 * radix - 1) ** (length - 1), + "unrestricted-source marginal") + cases += 1 + return cases + + +def controls(): + rows = agreement_rows(10, 64) + delta = density(rows, 3, 2, 64) + require(delta == Fraction(43, 2048), "three-pattern hand calculation") + require(delta != 1 - Fraction(127, 128) ** 2, + "unrestricted average cannot replace a slice average") + require(delta != Fraction(1, 32), "fixed-weight maximum is not its mean") + require(delta != 1 - Fraction(rows[3][2], 64 ** 2), + "normalization must include the binomial source count") + rejected = 0 + for length, radix in ((-1, 64), (129, 64), (1, 3), (1, 5), + (1, 65538), (True, 64), (1, True)): + try: + agreement_rows(length, radix) + except ValueError: + rejected += 1 + require(rejected == 7, "invalid-domain controls must reject") + return 3 + rejected + + +def evidence(): + result = exhaustive_check() + result["boundary_rows"] = boundary_check() + result["negative_controls"] = controls() + rows = agreement_rows(10, 64) + result["examples_B64"] = [ + {"m": m, "w": w, "failure_density": str(density(rows, m, w, 64))} + for m, w in ((3, 2), (10, 2), (10, 5), (10, 10)) + ] + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + result["sha256"] = { + name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in names + } + result["claim_type"] = "scoped proof conditional on the cited gap-product theorem" + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="create a new receipt; never overwrite") + args = parser.parse_args() + result = evidence() + encoded = (json.dumps(result, sort_keys=True, indent=2) + "\n").encode("utf-8") + if args.write is not None: + with args.write.open("xb") as output: + require(output.write(encoded) == len(encoded), "incomplete receipt write") + else: + require((PACKAGE / "RESULT.json").read_bytes() == encoded, + "receipt or source bytes differ; regenerate outside the checkout") + print("PASS_PACKED_FIXED_WEIGHT_REPAIR " + f"patterns={result['enumerated_source_patterns']} " + f"slices={result['checked_slices']} controls={result['negative_controls']}") + + +if __name__ == "__main__": + main()