From f38ce4e79a14e71704e61ddaea4410c4bdedf88b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 22:54:03 +0100 Subject: [PATCH] feat(research): prove minimum weighted reversal rescaling --- .../weighted-reversal-rescaling/README.md | 218 +++++ .../weighted-reversal-rescaling/RESULT.json | 742 ++++++++++++++++++ .../weighted-reversal-rescaling/SOURCES.json | 42 + .../weighted-reversal-rescaling/TASK.json | 93 +++ .../weighted-reversal-rescaling/VERIFY.json | 34 + .../weighted-reversal-rescaling/verify.py | 261 ++++++ 6 files changed, 1390 insertions(+) create mode 100644 research/weighted-reversal-rescaling/README.md create mode 100644 research/weighted-reversal-rescaling/RESULT.json create mode 100644 research/weighted-reversal-rescaling/SOURCES.json create mode 100644 research/weighted-reversal-rescaling/TASK.json create mode 100644 research/weighted-reversal-rescaling/VERIFY.json create mode 100644 research/weighted-reversal-rescaling/verify.py diff --git a/research/weighted-reversal-rescaling/README.md b/research/weighted-reversal-rescaling/README.md new file mode 100644 index 0000000000..d192032d73 --- /dev/null +++ b/research/weighted-reversal-rescaling/README.md @@ -0,0 +1,218 @@ +# Minimum diagonal rescaling of weighted reversals + +**Claim type: scoped algebraic proof with exact finite corroboration. No new kappa.** +This contribution was produced by Nick Petalas. Apache-2.0. + +Every defective reversal orbit needs exactly two nonidentity output-coordinate +scales, counting both banks. This holds for every modulus M >= 2, every positive +length, and every list of unit weights. The theorem also counts all minimum +repairs and gives the complete support generating polynomial. It answers the +even-length gap in Wentao Li's [#4095](https://github.com/CrocSwap/integer-mult-bounds/pull/4095) +while allowing multiple defective pairs and a defective central coordinate. + +The new result is support optimality and its counting law for arbitrary weight +lists. The reciprocal-weight wrapper contract is Jerry Chen's +[#2950](https://github.com/CrocSwap/integer-mult-bounds/pull/2950). +The odd-length, one-defective-end dual-scale classifications are Wentao Li's +[#4070](https://github.com/CrocSwap/integer-mult-bounds/pull/4070), +[#4073](https://github.com/CrocSwap/integer-mult-bounds/pull/4073) and #4095. +Their results are cited inputs, not re-verification deliverables. + +## Exact boundary + +Work on G = (Z/MZ)^n, with reversal r(i) = n-1-i and unit weights a_i. +Let R_a x have coordinate a_i x_{r(i)}. The weighted callee is + +```text +F_a(H,D) = (R_a D, R_a^-1 H). +``` + +After this callee, multiply H coordinate i by u_i and D coordinate i by v_i, +where all u_i,v_i are units. A repair must make the resulting map exactly F_b +for some weighted reversal R_b satisfying R_b^2 = I. This is equality on every +arbitrary dirty H,D, with no input restriction or extra bank. + +Its support cost is the number of nonidentity coordinate scales on both banks, + +```text +c(u,v) = #{i : u_i != 1} + #{i : v_i != 1}. +``` + +These are algebraic coordinate operations. The cost is not a Boolean gate, +native call, tape-movement or recursive-child price. No physical scale circuit +or supplier invoice is assumed free. + +## The minimum and every attaining repair + +Call a reversal orbit defective when a_i a_{r(i)} != 1 modulo M. Let p be the +number of defective two-element orbits and c in {0,1} the number of defective +fixed orbits. Put U = (Z/MZ)^*, phi = |U|, and + +```text +rho = #{t in U : t^2 = 1 mod M}. +``` + +Then the exact minimum support is 2(p+c). There are exactly 2^p rho^c distinct +minimum repairs, counted as ordered pairs of diagonal maps (u,v). + +They are precisely the following choices, independently in each orbit. + +- A nondefective orbit has every u coordinate equal to 1. +- In a defective pair {i,j}, put d = a_i a_j. Set (u_i,u_j) to either + (d^-1,1) or (1,d^-1). +- At a defective center i, choose any t in U with t^2=1 and set u_i=t a_i^-1. +- In every case set v_{r(i)}=u_i^-1. This determines the entire second bank. + +In particular, even n with a=(a0,middles,1), a0 != 1 and reciprocal middles +has exactly two minimum repairs of support two. If another pair is defective, +two scales no longer suffice. An odd central defect is repairable with +independent scales, even though no shared scalar can repair it. + +### Proof + +The first bank fixes b_i=u_i a_i. The second bank coefficient at coordinate +r(i) is v_{r(i)} a_i^-1. Equality with R_b^-1 forces + +```text +v_{r(i)} = u_i^-1. (1) +``` + +This uses only that a_i and u_i are units. Thus the support cost is exactly +twice the number of nonidentity u coordinates. The condition R_b^2=I is + +```text +u_i u_{r(i)} = (a_i a_{r(i)})^-1. (2) +``` + +For a defective two-element orbit, at least one u coordinate differs from 1. +Exactly one suffices, and its value is forced by (2). There are two choices of +coordinate. A nondefective orbit needs none. + +At a fixed orbit, (2) says (a_i u_i)^2=1. Its solutions are exactly +u_i=t a_i^-1 for the rho involutory units t. If a_i^2!=1, none equals 1. +If a_i^2=1, the unique minimum choice is u_i=1. Every unit group contains 1, +so the required choices always exist. The orbits are disjoint, proving both +the lower bound, the construction and the stated count. No field cancellation +or odd-modulus assumption is needed. + +## Complete support polynomial + +Let Z_a(z) = sum z^{c(u,v)}, over all valid repairs. For each two-element +orbit use the corresponding factor below; include the center factor when n +is odd. Then Z_a is exactly their product. + +| Orbit | Nondefective | Defective | +|---|---|---| +| Two coordinates | 1 + (phi-1) z^4 | 2 z^2 + (phi-2) z^4 | +| Central coordinate | 1 + (rho-1) z^2 | rho z^2 | + +For a pair with product d, choose any u_i in U; (2) uniquely fixes +u_j=d^-1 u_i^-1. If d=1, one choice makes both 1 and the other phi-1 choices +make both nonidentity. If d!=1, exactly two choices make one coordinate 1; +the other phi-2 make both nonidentity. A defective pair requires phi>=2, +so the coefficient is nonnegative. The center factors follow from the proof +above. Equation (1) doubles the support. Multiplication is valid because +neither equation couples distinct reversal orbits. + +At z=1 the formula counts phi^{floor(n/2)} rho^{n mod 2} repairs, independently +of the weights. This follows from the explicit orbit enumeration, not from +an independence assumption about a physical producer. + +## One scalar shared by both output banks + +Now restrict all nonidentity scales on either bank to one common unit lambda; +the two banks' coordinate supports may be chosen separately. If any orbit is +defective, such a repair exists exactly when the center is nondefective and +all defective pair products equal one common lambda != 1 with lambda^2=1. +When it exists its minimum support is 2p, with exactly 2^p minimum repairs. +If no orbit is defective, the unique minimum repair is the identity. + +Indeed, (1) requires a nonidentity scale and its inverse on the opposite +bank. Both equal lambda, so lambda^2=1. In a pair, the product of selected +scales is either 1 or lambda; only one selected endpoint changes a defective +product, forcing d=lambda. At a center, multiplying a_i by lambda cannot +change a_i^2, so a central defect cannot be repaired. These conditions also +suffice by selecting one endpoint in each defective pair. This explains why +the independent-bank optimum need not be available under the shared-scalar +restriction. + +## Evidence and reproduction + +The verifier enumerates all unit-weight lists in 23 fixed modulus/length +domains. For each list it independently enumerates every ordered pair (u,v), +forms the two literal monomial bank maps, compares them and squares the first. +It compares the entire observed support histogram with Z_a, its first +coefficient with the optimum/count formula, and the common-scalar minimum +with the criterion above. The finite enumeration covers 319 weight lists and +622,195 ordered scale assignments. + +Six additional fixtures enumerate every constructed minimum repair, including +three defective pairs modulo 15 and a central defect. Literal execution of +the six-operation ordinary wrapper on 202 module-basis columns checks the +dirty-bank interchange. Linearity makes a module-basis check exact for these +finite maps; the quantified theorem is the written proof above. + +Ten controls cover invalid/nonunit inputs, an omitted second-bank scale, +incorrect reversal of its support, equal diagonal maps, the central shared- +scalar obstruction, an attaining common involution and differing defects. +The generated [RESULT.json](RESULT.json) binds every other package file by +SHA256. Typed receipt comparison distinguishes booleans from integers. +Normal verification writes no files. + +From the repository root, with CPython 3.12 and only the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/weighted-reversal-rescaling/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/weighted-reversal-rescaling/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/weighted-reversal-rescaling +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/weighted-reversal-rescaling --check-source-history +``` + +Any CPython 3.12 installation can replace that interpreter path. The standalone +verifier also works in a Git-free export. To regenerate evidence, pass +`--emit-to NEW_EXTERNAL_FILE`; this exclusively creates a fresh receipt. + +## Scope, provenance and limitations + +Base: canonical main 624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7. +The uniform-transfer-audit card is changed to this algebraic side question. +Its connection is the weighted ordinary-callee boundary, where the reciprocal +condition matters before any proposed normalizer can be priced. This package +does not claim an audit of #4100 or a new selected supplier. + +Exact main-tree provenance is recorded in [SOURCES.json](SOURCES.json). +No predecessor code or scientific receipt is imported or executed. The selected +source-binding baseline was run as orientation only. Live open PRs, recent +handoffs, merged searches and distinctive main-tree README searches were +checked; the local-note overlap inventory is sparse and incomplete. No +exhaustive novelty claim follows from those searches. + +This result permits arbitrary independently chosen diagonal unit scales and +keeps the weighted reversal and surrounding ordinary wrapper fixed. It gives +no optimum over changed wrappers, nondiagonal maps, nonunit weights, auxiliary +banks or input-dependent scales. The checker bounds its finite arithmetic +domain to M<=16 and n<=6; the proof has no such restriction. Its Python managed +allocation is a documented runtime deviation from fixed-allocation discipline. +Every loop is bounded by those finite domains and the per-list limit of 4,096 +scale assignments. There is no recursion or dynamic code generation. + +Physical scale preparation, access, restoration, storage, native implementation, +compiler, stock, precision/tape and analytic recovery obligations remain +unpriced. The support theorem is not a complete multiplication theorem. +No Lean, Docker, predecessor scientific replay or selected operator replay +was run. Independent human and formal proof-kernel review are unclaimed. + +Credit Jerry Chen for #2950's wrapper contract and precision-blind example; +Wentao Li for the dual-scale setting and restricted support classifications; +Nick Petalas for the earlier #2808 wrapper; David Arias for the retained +ordinary caller; Jose Manuel and the credited source lineage for its physical +composition. Their files, credit lines and source notices are unchanged. + +## Open next questions + +Can a concrete weighted callee realize one of these minimum-support repairs +at a favorable complete cost? Start with a literal source and charge each +scale, inverse, frame change, access and restoration. The blocker is a physical +implementation and its invoice, not algebraic existence. Coordinate prices +that depend on the scalar or location also need a different optimization +objective; support optimality alone cannot choose the cheapest physical repair. diff --git a/research/weighted-reversal-rescaling/RESULT.json b/research/weighted-reversal-rescaling/RESULT.json new file mode 100644 index 0000000000..ad3aee3c6f --- /dev/null +++ b/research/weighted-reversal-rescaling/RESULT.json @@ -0,0 +1,742 @@ +{ + "results": { + "controls": 10, + "enumeration": [ + { + "accepted_support_histogram": [ + 1, + 0, + 0 + ], + "length": 1, + "modulus": 2, + "weight_lists": 1 + }, + { + "accepted_support_histogram": [ + 1, + 0, + 0, + 0, + 0 + ], + "length": 2, + "modulus": 2, + "weight_lists": 1 + }, + { + "accepted_support_histogram": [ + 2, + 0, + 2 + ], + "length": 1, + "modulus": 3, + "weight_lists": 2 + }, + { + "accepted_support_histogram": [ + 2, + 0, + 4, + 0, + 2 + ], + "length": 2, + "modulus": 3, + "weight_lists": 4 + }, + { + "accepted_support_histogram": [ + 2, + 0, + 2 + ], + "length": 1, + "modulus": 4, + "weight_lists": 2 + }, + { + "accepted_support_histogram": [ + 2, + 0, + 4, + 0, + 2 + ], + "length": 2, + "modulus": 4, + "weight_lists": 4 + }, + { + "accepted_support_histogram": [ + 2, + 0, + 6 + ], + "length": 1, + "modulus": 5, + "weight_lists": 4 + }, + { + "accepted_support_histogram": [ + 4, + 0, + 24, + 0, + 36 + ], + "length": 2, + "modulus": 5, + "weight_lists": 16 + }, + { + "accepted_support_histogram": [ + 2, + 0, + 2 + ], + "length": 1, + "modulus": 6, + "weight_lists": 2 + }, + { + "accepted_support_histogram": [ + 2, + 0, + 4, + 0, + 2 + ], + "length": 2, + "modulus": 6, + "weight_lists": 4 + }, + { + "accepted_support_histogram": [ + 2, + 0, + 10 + ], + "length": 1, + "modulus": 7, + "weight_lists": 6 + }, + { + "accepted_support_histogram": [ + 6, + 0, + 60, + 0, + 150 + ], + "length": 2, + "modulus": 7, + "weight_lists": 36 + }, + { + "accepted_support_histogram": [ + 4, + 0, + 12 + ], + "length": 1, + "modulus": 8, + "weight_lists": 4 + }, + { + "accepted_support_histogram": [ + 4, + 0, + 24, + 0, + 36 + ], + "length": 2, + "modulus": 8, + "weight_lists": 16 + }, + { + "accepted_support_histogram": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "length": 3, + "modulus": 2, + "weight_lists": 1 + }, + { + "accepted_support_histogram": [ + 4, + 0, + 12, + 0, + 12, + 0, + 4 + ], + "length": 3, + "modulus": 3, + "weight_lists": 8 + }, + { + "accepted_support_histogram": [ + 4, + 0, + 12, + 0, + 12, + 0, + 4 + ], + "length": 3, + "modulus": 4, + "weight_lists": 8 + }, + { + "accepted_support_histogram": [ + 8, + 0, + 72, + 0, + 216, + 0, + 216 + ], + "length": 3, + "modulus": 5, + "weight_lists": 64 + }, + { + "accepted_support_histogram": [ + 4, + 0, + 12, + 0, + 12, + 0, + 4 + ], + "length": 3, + "modulus": 6, + "weight_lists": 8 + }, + { + "accepted_support_histogram": [ + 16, + 0, + 144, + 0, + 432, + 0, + 432 + ], + "length": 3, + "modulus": 8, + "weight_lists": 64 + }, + { + "accepted_support_histogram": [ + 4, + 0, + 16, + 0, + 24, + 0, + 16, + 0, + 4 + ], + "length": 4, + "modulus": 3, + "weight_lists": 16 + }, + { + "accepted_support_histogram": [ + 4, + 0, + 16, + 0, + 24, + 0, + 16, + 0, + 4 + ], + "length": 4, + "modulus": 4, + "weight_lists": 16 + }, + { + "accepted_support_histogram": [ + 8, + 0, + 40, + 0, + 80, + 0, + 80, + 0, + 40, + 0, + 8 + ], + "length": 5, + "modulus": 3, + "weight_lists": 32 + } + ], + "fixtures": [ + { + "common_minimum": [ + null, + 0 + ], + "minimum_support": 6, + "modulus": 15, + "repairs": [ + [ + [ + 8, + 8, + 8, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 2, + 2, + 2 + ] + ], + [ + [ + 8, + 8, + 1, + 8, + 1, + 1 + ], + [ + 1, + 1, + 2, + 1, + 2, + 2 + ] + ], + [ + [ + 8, + 1, + 8, + 1, + 8, + 1 + ], + [ + 1, + 2, + 1, + 2, + 1, + 2 + ] + ], + [ + [ + 8, + 1, + 1, + 8, + 8, + 1 + ], + [ + 1, + 2, + 2, + 1, + 1, + 2 + ] + ], + [ + [ + 1, + 8, + 8, + 1, + 1, + 8 + ], + [ + 2, + 1, + 1, + 2, + 2, + 1 + ] + ], + [ + [ + 1, + 8, + 1, + 8, + 1, + 8 + ], + [ + 2, + 1, + 2, + 1, + 2, + 1 + ] + ], + [ + [ + 1, + 1, + 8, + 1, + 8, + 8 + ], + [ + 2, + 2, + 1, + 2, + 1, + 1 + ] + ], + [ + [ + 1, + 1, + 1, + 8, + 8, + 8 + ], + [ + 2, + 2, + 2, + 1, + 1, + 1 + ] + ] + ], + "weights": [ + 2, + 2, + 2, + 1, + 1, + 1 + ] + }, + { + "common_minimum": [ + null, + 0 + ], + "minimum_support": 2, + "modulus": 15, + "repairs": [ + [ + [ + 1, + 8, + 1 + ], + [ + 1, + 2, + 1 + ] + ], + [ + [ + 1, + 2, + 1 + ], + [ + 1, + 8, + 1 + ] + ], + [ + [ + 1, + 13, + 1 + ], + [ + 1, + 7, + 1 + ] + ], + [ + [ + 1, + 7, + 1 + ], + [ + 1, + 13, + 1 + ] + ] + ], + "weights": [ + 1, + 2, + 1 + ] + }, + { + "common_minimum": [ + 4, + 4 + ], + "minimum_support": 4, + "modulus": 15, + "repairs": [ + [ + [ + 4, + 4, + 1, + 1 + ], + [ + 1, + 1, + 4, + 4 + ] + ], + [ + [ + 4, + 1, + 4, + 1 + ], + [ + 1, + 4, + 1, + 4 + ] + ], + [ + [ + 1, + 4, + 1, + 4 + ], + [ + 4, + 1, + 4, + 1 + ] + ], + [ + [ + 1, + 1, + 4, + 4 + ], + [ + 4, + 4, + 1, + 1 + ] + ] + ], + "weights": [ + 4, + 4, + 1, + 1 + ] + }, + { + "common_minimum": [ + null, + 0 + ], + "minimum_support": 4, + "modulus": 8, + "repairs": [ + [ + [ + 3, + 5, + 1, + 1 + ], + [ + 1, + 1, + 5, + 3 + ] + ], + [ + [ + 3, + 1, + 5, + 1 + ], + [ + 1, + 5, + 1, + 3 + ] + ], + [ + [ + 1, + 5, + 1, + 3 + ], + [ + 3, + 1, + 5, + 1 + ] + ], + [ + [ + 1, + 1, + 5, + 3 + ], + [ + 3, + 5, + 1, + 1 + ] + ] + ], + "weights": [ + 3, + 5, + 1, + 1 + ] + }, + { + "common_minimum": [ + null, + 0 + ], + "minimum_support": 2, + "modulus": 9, + "repairs": [ + [ + [ + 7, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 4 + ] + ], + [ + [ + 1, + 1, + 1, + 7 + ], + [ + 4, + 1, + 1, + 1 + ] + ] + ], + "weights": [ + 4, + 1, + 1, + 1 + ] + }, + { + "common_minimum": [ + 0, + 1 + ], + "minimum_support": 0, + "modulus": 2, + "repairs": [ + [ + [ + 1 + ], + [ + 1 + ] + ] + ], + "weights": [ + 1 + ] + } + ], + "scale_assignments": 622195, + "weight_lists": 319, + "wrapper_basis_columns": 202 + }, + "schema_version": 1, + "source_sha256": { + "README.md": "c455b51a41a4d217390c4286e6b310f0ac7fe802bf624eb83bf5e35868774308", + "SOURCES.json": "21e3155f02eafa65ad031e74d2ab8d1a6bd61d2802073d3930cd7f23c0b5e2a5", + "TASK.json": "84ff71dedb70ac86fbf2bb852337c7817fedd2c5c64e602e86b3259537f87717", + "VERIFY.json": "4b8cc6c999ef14ef279ceae931bdc5ba3eabad66e0b90022ea3bf48150346b81", + "verify.py": "dd8f86705509f77b4222295b88ad96906ad3160b45ae8ce82a827dd7bceae808" + } +} diff --git a/research/weighted-reversal-rescaling/SOURCES.json b/research/weighted-reversal-rescaling/SOURCES.json new file mode 100644 index 0000000000..7be4555d56 --- /dev/null +++ b/research/weighted-reversal-rescaling/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/weighted-wrapper-contract/README.md", + "usage": "provenance", + "git_blob": "f0a912efd96af3804f5663ba39323763bc0ed797", + "sha256": "e1565fb54651303258ef144f7b774e8ef1e7534d3b1129c516a6f88326408c71" + }, + { + "path": "research/precision-blind-composite-rigidity/README.md", + "usage": "provenance", + "git_blob": "59c94fe8ba5869585bf7c50dd14142ad6839d621", + "sha256": "2c56acddf78c1475279cded3539835b19c31926fe6f28525989e969bb166f547" + }, + { + "path": "research/precision-blind-composite-rigidity/PROOF.md", + "usage": "provenance", + "git_blob": "06933cb91e578ffbcf4940ffdfa0ce8efc1a059d", + "sha256": "96023dee12171183d5cda63d0fdb3bcd62c0ef2ac04d7a78b17e636a2eebccdc" + }, + { + "path": "research/precision-blind-odd-n-support/README.md", + "usage": "provenance", + "git_blob": "d83fe068f8b5a773385b41bfeca0a2199f41ea50", + "sha256": "30796d69372e442a9f33a205090dd6c74f4b6f847865be967d001ecb682e868c" + } + ] +} diff --git a/research/weighted-reversal-rescaling/TASK.json b/research/weighted-reversal-rescaling/TASK.json new file mode 100644 index 0000000000..7cd7c5da61 --- /dev/null +++ b/research/weighted-reversal-rescaling/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "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_status": "changed", + "actual_scope": "Minimum support, complete support polynomial and common-scalar feasibility for diagonal output rescaling of arbitrary unit-weighted reversals over Z/MZ.", + "scope_change_reason": "The live even-length question in Wentao Li PR4095 motivates a new support-optimal repair theorem, rather than an audit or a new grid of the earlier one-defect cases.", + "bottleneck_link": "Algebraic side result at the ordinary weighted-callee boundary. It identifies exactly how much coordinate rescaling a proposed normalization must implement; physical costs remain unpriced.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved minimum-rescaling result with exact finite corroboration; do not extend to physical implementations or a selected frontier.", + "outcome": "completed", + "evidence": "Written orbit proof in README.md; full two-bank scale enumeration and literal wrapper-basis execution in verify.py; generated source-bound RESULT.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a literal weighted callee implement a minimum-support repair with a favorable complete physical bill?", + "why_it_matters": "Algebraic support does not price a native scale, access, frame change or restoration.", + "first_step": "Pin one weighted producer and implement both inverse-related diagonal output maps with all reads, moves and restoration charged.", + "blocked_by": "No concrete physical producer or scale tariff is supplied here." + } + ], + "claim_type": "scoped algebraic proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133372", + "overlap": { + "canonical_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "open_prs": 367, + "open_prs_fetched_at": "2026-10-22T21:46:53.349587+00:00", + "discussion_records": 3821, + "discussions_fetched_at": "2026-10-22T21:47:40.155217+00:00", + "local_notes_searched": 117, + "local_notes_at_head": 6319, + "limitations": "Sparse local-note inventory, arbitrary diffs and unpublished work are outside coverage. Distinctive all-main README and merged-PR searches supplemented the cache.", + "nearest_predecessors": [ + 2950, + 4070, + 4073, + 4095 + ], + "related_open_pr": "PR2901 contains an incidental precision-blind phrase but studies rational decoder cancellation lines, not weighted callee normalization." + } +} diff --git a/research/weighted-reversal-rescaling/VERIFY.json b/research/weighted-reversal-rescaling/VERIFY.json new file mode 100644 index 0000000000..dbfa877186 --- /dev/null +++ b/research/weighted-reversal-rescaling/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": "Complete finite two-bank scale enumeration; full support polynomials; minimum and common-scalar laws; literal dirty wrapper and ten controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact enumeration and generated source-bound receipt with optimization enabled." + } + ] +} diff --git a/research/weighted-reversal-rescaling/verify.py b/research/weighted-reversal-rescaling/verify.py new file mode 100644 index 0000000000..4c7a126a44 --- /dev/null +++ b/research/weighted-reversal-rescaling/verify.py @@ -0,0 +1,261 @@ +#!/usr/bin/env python3 +"""Exact finite checks of minimum weighted-reversal rescaling. + +Produced by Nick Petalas. Apache-2.0. Python managed allocation is used. +""" +from __future__ import annotations + +import argparse +import hashlib +import itertools +import json +from math import gcd +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def units(modulus: int) -> tuple[int, ...]: + need(type(modulus) is int and 2 <= modulus <= 16, "finite modulus domain") + return tuple(x for x in range(modulus) if gcd(x, modulus) == 1) + + +def validate(weights: tuple[int, ...], modulus: int) -> tuple[int, ...]: + group = units(modulus) + need(1 <= len(weights) <= 6, "finite length domain") + need(all(type(x) is int and x in group for x in weights), "unit weights") + return group + + +def polynomial(weights: tuple[int, ...], modulus: int) -> list[int]: + """The exponent counts nonidentity scales on both output banks.""" + group = validate(weights, modulus) + phi = len(group) + rho = sum(x * x % modulus == 1 for x in group) + result = [1] + n = len(weights) + for i in range((n + 1) // 2): + j = n - 1 - i + good = weights[i] * weights[j] % modulus == 1 + if i == j: + factor = [1, 0, rho - 1] if good else [0, 0, rho] + else: + factor = [1, 0, 0, 0, phi - 1] if good else [0, 0, 2, 0, phi - 2] + combined = [0] * (len(result) + len(factor) - 1) + for a, value in enumerate(result): + for b, coefficient in enumerate(factor): + combined[a + b] += value * coefficient + result = combined + return result + [0] * (2 * n + 1 - len(result)) + + +def predicted_minimum(weights: tuple[int, ...], modulus: int) -> tuple[int, int]: + group = validate(weights, modulus) + rho = sum(x * x % modulus == 1 for x in group) + pairs = center = 0 + for i in range((len(weights) + 1) // 2): + j = len(weights) - 1 - i + if weights[i] * weights[j] % modulus != 1: + center += i == j + pairs += i != j + return 2 * (pairs + center), 2 ** pairs * rho ** center + + +def predicted_common(weights: tuple[int, ...], modulus: int) -> tuple[int | None, int]: + validate(weights, modulus) + defects = set() + pairs = 0 + for i in range((len(weights) + 1) // 2): + j = len(weights) - 1 - i + defect = weights[i] * weights[j] % modulus + if defect == 1: + continue + if i == j: + return None, 0 + defects.add(defect) + pairs += 1 + if not defects: + return 0, 1 + if len(defects) != 1: + return None, 0 + scalar = next(iter(defects)) + if scalar * scalar % modulus != 1: + return None, 0 + return 2 * pairs, 2 ** pairs + + +def literal_accepts(weights: tuple[int, ...], u: tuple[int, ...], + v: tuple[int, ...], modulus: int) -> bool: + """Compare actual monomial bank maps, then square the first bank map.""" + n = len(weights) + first = tuple(u[i] * weights[i] % modulus for i in range(n)) + second = tuple(v[i] * pow(weights[n - 1 - i], -1, modulus) % modulus + for i in range(n)) + return first == second and all(first[i] * first[n - 1 - i] % modulus == 1 + for i in range(n)) + + +def exhaustive(weights: tuple[int, ...], modulus: int) -> tuple[list[int], tuple[int | None, int], int]: + group = validate(weights, modulus) + n = len(weights) + need(len(group) ** (2 * n) <= 4096, "dual-scale enumeration cap") + candidates = tuple(itertools.product(group, repeat=n)) + histogram = [0] * (2 * n + 1) + common = [0] * (2 * n + 1) + for u in candidates: + for v in candidates: + if literal_accepts(weights, u, v, modulus): + support = sum(x != 1 for x in u + v) + histogram[support] += 1 + if len(set(u + v) - {1}) <= 1: + common[support] += 1 + minimum = next((i for i, value in enumerate(common) if value), None) + return histogram, (minimum, 0 if minimum is None else common[minimum]), len(candidates) ** 2 + + +def callee(h: tuple[int, ...], d: tuple[int, ...], weights: tuple[int, ...], + u: tuple[int, ...], v: tuple[int, ...], modulus: int) -> tuple[tuple[int, ...], tuple[int, ...]]: + n = len(weights) + first = tuple(u[i] * weights[i] * d[n - 1 - i] % modulus for i in range(n)) + second = tuple(v[i] * pow(weights[n - 1 - i], -1, modulus) + * h[n - 1 - i] % modulus for i in range(n)) + return first, second + + +def wrapper_basis(weights: tuple[int, ...], u: tuple[int, ...], + v: tuple[int, ...], modulus: int) -> int: + n = len(weights) + for column in range(2 * n): + original_h = tuple(int(i == column) for i in range(n)) + original_d = tuple(int(n + i == column) for i in range(n)) + h = original_h + d = tuple((original_d[i] - h[i]) % modulus for i in range(n)) + h, d = callee(h, d, weights, u, v, modulus) + d = tuple((d[i] + h[i]) % modulus for i in range(n)) + h, d = callee(h, d, weights, u, v, modulus) + d = tuple((-d[i] + h[i]) % modulus for i in range(n)) + need((h, d) == (original_d, original_h), "literal dirty wrapper") + return 2 * n + + +def minimum_repairs(weights: tuple[int, ...], modulus: int) -> list[tuple[tuple[int, ...], tuple[int, ...]]]: + group = validate(weights, modulus) + n = len(weights) + choices = [] + for i in range((n + 1) // 2): + j = n - 1 - i + defect = weights[i] * weights[j] % modulus + if defect == 1: + choices.append(((i, j, 1, 1),)) + elif i != j: + inverse = pow(defect, -1, modulus) + choices.append(((i, j, inverse, 1), (i, j, 1, inverse))) + else: + choices.append(tuple((i, j, root * pow(weights[i], -1, modulus) % modulus, + root * pow(weights[i], -1, modulus) % modulus) + for root in group if root * root % modulus == 1)) + repairs = [] + for selection in itertools.product(*choices): + u = [1] * n + for i, j, left, right in selection: + u[i], u[j] = left, right + v = tuple(pow(u[n - 1 - i], -1, modulus) for i in range(n)) + repairs.append((tuple(u), v)) + return repairs + + +def controls() -> int: + rejected = 0 + for weights, modulus in [((0, 1), 5), ((True,), 3), ((), 3), ((1,), 1)]: + try: + validate(weights, modulus) + except ValueError: + rejected += 1 + need(rejected == 4, "input controls") + weights, modulus = (2, 1), 15 + u, v = minimum_repairs(weights, modulus)[0] + need(literal_accepts(weights, u, v, modulus), "positive repair") + need(not literal_accepts(weights, u, (1, 1), modulus), "omitted D-bank scale") + need(not literal_accepts(weights, u, tuple(reversed(v)), modulus), "wrong D support") + need(not literal_accepts(weights, u, u, modulus), "equal diagonal maps") + need(predicted_common((2,), 15) == (None, 0), "central common-scale obstruction") + need(predicted_common((4, 1), 15) == (2, 2), "common involution attains") + need(predicted_common((4, 11, 1, 1), 15) == (None, 0), "different pair defects") + return rejected + 6 + + +def build() -> dict: + records = [] + cases = [(m, n) for m in range(2, 9) for n in (1, 2)] + cases += [(m, 3) for m in (2, 3, 4, 5, 6, 8)] + cases += [(3, 4), (4, 4), (3, 5)] + assignments = 0 + for modulus, n in cases: + group = units(modulus) + totals = [0] * (2 * n + 1) + for weights in itertools.product(group, repeat=n): + actual, common, checked = exhaustive(weights, modulus) + need(actual == polynomial(weights, modulus), "full support polynomial") + minimum = next(i for i, value in enumerate(actual) if value) + need((minimum, actual[minimum]) == predicted_minimum(weights, modulus), "minimum") + need(common == predicted_common(weights, modulus), "common-scalar criterion") + assignments += checked + totals = [a + b for a, b in zip(totals, actual)] + records.append({"modulus": modulus, "length": n, "weight_lists": len(group) ** n, + "accepted_support_histogram": totals}) + fixtures = [] + basis_columns = 0 + for modulus, weights in [(15, (2, 2, 2, 1, 1, 1)), (15, (1, 2, 1)), + (15, (4, 4, 1, 1)), (8, (3, 5, 1, 1)), + (9, (4, 1, 1, 1)), (2, (1,))]: + repairs = minimum_repairs(weights, modulus) + minimum, count = predicted_minimum(weights, modulus) + need(len(repairs) == len(set(repairs)) == count, "distinct minimum repairs") + for u, v in repairs: + need(literal_accepts(weights, u, v, modulus), "constructed endpoint") + need(sum(x != 1 for x in u + v) == minimum, "constructed minimum support") + basis_columns += wrapper_basis(weights, u, v, modulus) + fixtures.append({"modulus": modulus, "weights": weights, "minimum_support": minimum, + "repairs": repairs, "common_minimum": predicted_common(weights, modulus)}) + return {"enumeration": records, "scale_assignments": assignments, + "weight_lists": sum(row["weight_lists"] for row in records), "fixtures": fixtures, + "wrapper_basis_columns": basis_columns, "controls": controls()} + + +def serialized(value: object) -> str: + return json.dumps(value, indent=2, sort_keys=True) + "\n" + + +def receipt() -> dict: + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() for name in names} + return {"schema_version": 1, "source_sha256": hashes, "results": build()} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-to", type=Path, help="exclusive-create a fresh external receipt") + args = parser.parse_args() + fresh = receipt() + if args.emit_to is not None: + destination = args.emit_to.resolve() + need(not destination.is_relative_to(HERE), "emit outside package") + with destination.open("x", encoding="utf-8") as stream: + stream.write(serialized(fresh)) + else: + stored = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + need(serialized(stored) == serialized(fresh), "typed receipt/source mismatch") + result = fresh["results"] + print("PASS_WEIGHTED_REVERSAL_RESCALING", "weights=" + str(result["weight_lists"]), + "assignments=" + str(result["scale_assignments"]), + "wrapper_columns=" + str(result["wrapper_basis_columns"]), + "controls=" + str(result["controls"]), "no_new_kappa") + + +if __name__ == "__main__": + main()