From b07ae963075920c46a1662b6d1297dbfa3e6dc16 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 23:12:36 +0000 Subject: [PATCH] feat(research): construct optimal unbiased reversible phase rounding --- research/unbiased-periodic-rotation/PROOF.md | 168 ++++++ research/unbiased-periodic-rotation/README.md | 132 +++++ .../unbiased-periodic-rotation/SOURCES.json | 18 + .../unbiased-periodic-rotation/TABLE.json | 515 ++++++++++++++++++ research/unbiased-periodic-rotation/TASK.json | 89 +++ .../unbiased-periodic-rotation/VERIFY.json | 34 ++ .../unbiased-periodic-rotation/construct.py | 99 ++++ research/unbiased-periodic-rotation/verify.py | 225 ++++++++ 8 files changed, 1280 insertions(+) create mode 100644 research/unbiased-periodic-rotation/PROOF.md create mode 100644 research/unbiased-periodic-rotation/README.md create mode 100644 research/unbiased-periodic-rotation/SOURCES.json create mode 100644 research/unbiased-periodic-rotation/TABLE.json create mode 100644 research/unbiased-periodic-rotation/TASK.json create mode 100644 research/unbiased-periodic-rotation/VERIFY.json create mode 100644 research/unbiased-periodic-rotation/construct.py create mode 100644 research/unbiased-periodic-rotation/verify.py diff --git a/research/unbiased-periodic-rotation/PROOF.md b/research/unbiased-periodic-rotation/PROOF.md new file mode 100644 index 0000000000..d8d4038cce --- /dev/null +++ b/research/unbiased-periodic-rotation/PROOF.md @@ -0,0 +1,168 @@ +# An unbiased reversible lattice rotation + +This contribution was produced by Nick Petalas. Apache-2.0. + +Put + +```text +B = [[3,-4],[4,3]], A = B/5. +``` + +Thus A is multiplication by the unit complex number (3+4i)/5. The input and +output lattices are both Z^2. A seed is supplied uniformly from five states, +independently of the input. The seed is retained for inversion. + +## The statement + +There are five bijections F_s:Z^2 -> Z^2, for 0 <= s < 5, such that for every +x in Z^2: + +1. F_s(x+5z)=F_s(x)+Bz for every integer z. +2. E_s F_s(x)=Ax. +3. If Ax is integral, F_s(x)=Ax for every seed. Otherwise + E_s ||F_s(x)-Ax||_2^2=2/5. +4. For every individual seed and input, ||F_s(x)-Ax||_2^2 <= 4/5. + +The expected squared error in item 3 is the smallest possible at each x +among all unbiased integer-valued random outputs, even without requiring +reversibility. In particular the worst-input expected squared error 2/5 is +optimal for the declared unbiased contract. The last item's deterministic +bound is an attained bound of this construction; no new optimum for a +single deterministic bijection is asserted. + +The witness is TABLE.json. Its five tables each have 25 pairs. Row i=5r+t +corresponds to the residue (r,t), with 0 <= r,t < 5. Write o_s(r,t) for that +pair. Define, using coordinatewise Euclidean division, + +```text +x = 5q + (r,t), F_s(x) = Bq + o_s(r,t). +``` + +This is a definition on the entire unbounded lattice, including negative +inputs. No clipping, saturation, inward norm constraint or bounded entrance +domain is imposed. + +## A finite certificate for each all-lattice bijection + +For y=(u,v), define + +```text +K(y) = (3u+4v mod 25, -4u+3v mod 25). +``` + +Two integer points y,y' have the same K exactly when y-y' belongs to BZ^2. +Indeed B^(-1)=[[3,4],[-4,3]]/25, so equality of the two residues is exactly +integrality of B^(-1)(y-y'). The group Z^2/BZ^2 has order |det B|=25. This +also follows by enumerating K on the 25-by-25 residue square, since 25Z^2 +is contained in BZ^2. + +For each seed, the 25 table outputs have distinct K values. This is one +finite exact certificate obligation. They consequently represent all 25 +cosets. Given any y, there is exactly one row (r,t) with +K(o_s(r,t))=K(y). Its unique inverse is + +```text +q = B^(-1)(y-o_s(r,t)), x = 5q+(r,t). +``` + +The coset test proves that q is integral. Substitution proves both inverse +identities, hence bijectivity and surjectivity on the full lattice. The +covariance in item 1 follows directly from Euclidean division. + +## Unbiasedness and the error + +The checker verifies, for every one of the 25 rows, + +```text +sum_s o_s(r,t) = B(r,t). +``` + +Taking the uniform average in the defining formula proves E F_s(x)=Ax for +all q as well as every residue. Errors are unchanged by x -> x+5z. + +For each row and seed, both coordinates of o_s(r,t) lie between the floor +and ceiling of the corresponding coordinate of A(r,t). The checker verifies +that condition, the first moment above, and the exact sums of squared +residual numerators. Those sums are zero at five rows and 50 at the other +twenty rows. Since the residual numerators are 5o_s-B(r,t), the expected +squared error is 50/(5*25)=2/5 at the latter rows. The largest individual +squared residual numerator is 20, giving 20/25=4/5. The checker enumerates +all 125 row/seed entries; neither conclusion comes from a sampled input. + +The optimality can also be derived without those squared-error sums. For +a scalar mean mu=k+f with k an integer and 0<=f<1, any integer-valued random +variable Y with finite second moment satisfies + +```text +(Y-k)(Y-k-1) >= 0, +E (Y-mu)^2 >= f(1-f) whenever E Y=mu. +``` + +Expansion and E(Y-k)=f prove the inequality. Equality holds exactly when +Y is supported on {k,k+1}, apart from the integral case where it is constant. +If the second moment is infinite, the lower bound still holds. Adding the +two coordinate inequalities gives the pointwise bound for Euclidean squared +error, without any independence assumption between coordinates. + +Set a=(3r-4t) mod 5 and b=(4r+3t) mod 5. Then b=3a mod 5. When a=0 both +coordinates of A(r,t) are integral. Otherwise (a,b) is one of +(1,3),(2,1),(3,4),(4,2), and + +```text +[a(5-a)+b(5-b)]/25 = 10/25 = 2/5. +``` + +Our unbiased nearest-cell outputs attain this lower bound in both +coordinates simultaneously. Requiring each seeded map to be a bijection +therefore costs no additional mean squared error for this rotation. + +## How the witness is constructed + +The retained constructor is an exact integer algorithm. For one input row, +let u,v be the two coordinate floors and let a,b be their fractional +numerators modulo five. In units of 1/5 put + +```text +c = min(a,b) if a is 1 or 4, +c = max(0,a+b-5) otherwise. + +weight(u, v ) = 5-a-b+c, +weight(u+1,v ) = a-c, +weight(u, v+1) = b-c, +weight(u+1,v+1) = c. +``` + +These weights are nonnegative and give total weight five and the required +two coordinate means. Group the output points by K. The constructor checks +all 25 input and 25 output degrees equal five, obtaining a five-regular +bipartite multigraph. It extracts five perfect matchings and uses their +literal output points as the five tables. Matching existence is the standard +regular bipartite graph argument: a set of input vertices has 5|S| incident +edges, whose neighbors can receive at most 5|N(S)|, so Hall's inequality +holds. The implemented bounded augmentation routine constructs each matching; +removing it leaves a regular graph of one smaller degree. + +This is dependent coordinate rounding. Independent stochastic rounding has +the same scalar means and minimum error but its output coset capacities +are not all one in this quotient. The checker rejects that control. Thus +unbiased scalar rounding by itself does not certify the reversible ensemble. +The independent checker of the table only needs coset coverage, means and +nearest-cell membership; it does not trust how the weights were discovered. +No optimizer or floating-point result is a mathematical premise. + +## Scope + +Multiplying the input and output lattices by h>0 multiplies the squared +error bounds by h^2. This follows by conjugating each map by scalar scaling. +It does not price changes of representation or precision. + +The contract is for a fresh uniform seed independent of the current input. +An adversary who selects inputs after observing the seed can obtain a bias; +no adaptive seed-reuse or inverse-unbiasedness theorem is claimed. Exact +return requires the seed or an equivalent record. No seed sampler, entropy +recovery, physical instruction table, fixed-tape routing, bounded-word +implementation or reversible workspace bill is supplied. The rational phase +is not bound to a selected supplier root or caller. Those costs and the five +selected framework assumptions remain open. This is a scoped mathematical +construction with a finite exact certificate, not a complete multiplication +theorem or a new kappa. diff --git a/research/unbiased-periodic-rotation/README.md b/research/unbiased-periodic-rotation/README.md new file mode 100644 index 0000000000..dade07cfa9 --- /dev/null +++ b/research/unbiased-periodic-rotation/README.md @@ -0,0 +1,132 @@ +# Optimal unbiased rounding by five reversible lattice maps + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +**Claim type: scoped all-lattice construction and proof with a finite exact +certificate.** For A=[[3,-4],[4,3]]/5, five explicit bijections of Z^2 have +uniform average Ax at every integer input. Retaining the seed gives an exact +two-sided inverse. Their expected squared error is zero when Ax is integral +and 2/5 otherwise. This is the pointwise minimum among all unbiased +integer-valued random outputs, including irreversible ones. Each seed also +has squared error at most 4/5. Grid spacing h scales these bounds by h^2. +No new kappa or selected-frontier change is claimed. + +The construction attains the ordinary stochastic-rounding error optimum +while preserving exact reversibility for each seed. It uses dependent +coordinate rounding and a finite matching, rather than treating independently +rounded coordinates as a permutation. No physical sampler or execution-cost +claim follows from this mathematical interface. + +[PROOF.md](PROOF.md) gives the universal argument. +[TABLE.json](TABLE.json) gives the five 25-row transversals, and +[construct.py](construct.py) regenerates them by bounded integer matching. +For x=5q+r, the map is Bq+table_s[r], where B=5A. Its inverse locates the +unique table output in y's coset modulo BZ^2, subtracts it and applies B^-1. +Every certificate condition has only 25 rows per seed; translation covariance +then supplies all integer inputs, including negative and arbitrarily large +ones. The exact verifier needs only the Python standard library. + +## Reproduce + +From the repository root, with CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/unbiased-periodic-rotation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/unbiased-periodic-rotation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/unbiased-periodic-rotation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/unbiased-periodic-rotation --check-source-history +``` + +Any CPython 3.12 path may replace that absolute path. Expected scientific +marker: `PASS_UNBIASED_PERIODIC_ROTATION`. Every direct run emits its computed +counts and a receipt bound to all eight package-file hashes. No receipt is +handwritten. Registered commands have a 120-second timeout and write no +replay outputs into the checkout. To regenerate the certificate, run +`python3.12 -I -B research/unbiased-periodic-rotation/construct.py` and compare +its stdout with TABLE.json. + +The finite replay checks all 125 seed/residue entries, 16,810 signed two-sided +roundtrips, 3,750 images on four larger quotients and 1,250 signed translation +cases through 1,024-bit coordinates. Five controls distinguish a transversal +from an unbiased nearest-cell ensemble, require retention of the seed, reject +a fixed-seed unbiasedness claim, and reject independent coordinate rounding's +wrong output capacities. Finite tests corroborate the written argument; the +proof's covariance and inverse formulas supply the universal quantifiers. + +## Scope and related work + +The original `uniform-transfer-audit` card is explicitly changed to a new +precision-interface side result. It does not discharge an assumption at its +actual selected caller. Canonical base is +7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision eight; the selected +record remains PR6030, conditional kappa 0.003125804. + +The question and matching construction are original to this contribution. +Classical scalar rounding variance, lattice quotient and regular bipartite +matching arguments retain their classical status. No general literature +priority is claimed for those methods. The rational phase also occurs in +ywz65's [PR2589](https://github.com/CrocSwap/integer-mult-bounds/pull/2589) +and Nick Petalas's [PR6304](https://github.com/CrocSwap/integer-mult-bounds/pull/6304). +Their deterministic lifting and norm/error results are context, not premises +or audit targets. The present question changes the contract to an unbiased +random ensemble with the pointwise stochastic error optimum. It does not +improve or generalize the four-tie deterministic optimum of PR6304, and its +individual-map 4/5 bound is not claimed as a new deterministic threshold. + +[PR6418](https://github.com/CrocSwap/integer-mult-bounds/pull/6418) studies +adaptive bias from reusing a rounding seed. This construction requires an +independent seed for the stated expectation and supplies no reuse guarantee. +The same selected precision/native/compiler, ownership and analytic lineage +keeps its existing credit. No predecessor scientific replay was run. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362318). +Live open/account PRs, handoffs, active Discussions, local reservations, main +README terms and distinctive merged searches were checked. Sparse local +notes, arbitrary historical code and unpublished work remain coverage limits. + +## Limitations + +The seed is an externally supplied uniform five-state variable. Exact return +retains it. Sampling it, storing it, reclaiming its entropy and implementing +the quotient lookup with reversible scratch remain unpriced. The construction +allows outward norm movement and covers one rational planar rotation. There +is no inverse-unbiasedness, adaptive seed, repeated-word error, selected-root +or caller-binding theorem. Native/physical cost, precision/storage/tape costs, +supplier admission and a complete signed recursive invoice remain open. +All five framework assumptions remain. Selected cold replay, native builds, +Lean, Docker, independent human review and formal proof-kernel review are +unrun or unclaimed. + +## Open next questions + +- Bind a phase actually used by a supplier, its lattice, seed ownership and + outward headroom. Start with an exact producer/consumer contract and price + quotient lookup, seed sampling/retention and restoration before judging the + complete invoice. The missing physical caller is the blocker. +- Can a finite matching with unbiased nearest-cell outputs be constructed for + another rational orthogonal operator? Start with its integral period matrix + and exact output-coset capacities. A favorable scalar error bound alone + does not provide such an ensemble. No extension is reserved here. + +Structured first steps and blockers are in [TASK.json](TASK.json). + +## Code constraints + +The constructor uses no recursion or optimizer. At most five matchings each +have 25 augmentations, each scanning at most 25 rows and 25 columns; each +alternating path has at most 25 links. The verifier's finite domains are +explicit in the counts above. Functions fit within sixty physical lines. +Explicit exception checks remain active under optimized Python. The only +package import is the adjacent constructor. File reads are bounded to eight +regular files of at most one MiB each; the table is limited to 64 KiB and +its coordinate shapes/ranges are checked before computation. + +Power of Ten rule 3 deviation: CPython allocates integers and collections +during this bounded offline computation. The graph has 625 capacity entries +and 625 optional output entries, the certificate 125 points, and the largest +oracle image set 400 points. Large-coordinate tests use at most 1,030-bit +integers. Runtime allocation internals are not instrumented. Warning-strict +normal/optimized execution and in-memory syntax checks provide diagnostics; +no external type checker or linter was run. This is not an allocation-free or +bounded-word runtime implementation. diff --git a/research/unbiased-periodic-rotation/SOURCES.json b/research/unbiased-periodic-rotation/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/unbiased-periodic-rotation/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/unbiased-periodic-rotation/TABLE.json b/research/unbiased-periodic-rotation/TABLE.json new file mode 100644 index 0000000000..b223eb5742 --- /dev/null +++ b/research/unbiased-periodic-rotation/TABLE.json @@ -0,0 +1,515 @@ +{ + "schema_version": 1, + "tables": [ + [ + [ + 0, + 0 + ], + [ + -1, + 1 + ], + [ + -2, + 2 + ], + [ + -2, + 1 + ], + [ + -3, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + -1, + 2 + ], + [ + -2, + 3 + ], + [ + -3, + 4 + ], + [ + 1, + 2 + ], + [ + 0, + 3 + ], + [ + -1, + 3 + ], + [ + -1, + 4 + ], + [ + -2, + 4 + ], + [ + 2, + 3 + ], + [ + 1, + 3 + ], + [ + 0, + 4 + ], + [ + -1, + 5 + ], + [ + -2, + 5 + ], + [ + 3, + 3 + ], + [ + 2, + 4 + ], + [ + 1, + 4 + ], + [ + 0, + 5 + ], + [ + 0, + 6 + ] + ], + [ + [ + 0, + 0 + ], + [ + -1, + 1 + ], + [ + -2, + 1 + ], + [ + -2, + 2 + ], + [ + -3, + 2 + ], + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + -1, + 2 + ], + [ + -2, + 3 + ], + [ + -3, + 3 + ], + [ + 1, + 1 + ], + [ + 1, + 2 + ], + [ + -1, + 3 + ], + [ + -1, + 4 + ], + [ + -2, + 4 + ], + [ + 2, + 2 + ], + [ + 1, + 3 + ], + [ + 0, + 3 + ], + [ + 0, + 4 + ], + [ + -1, + 5 + ], + [ + 2, + 3 + ], + [ + 2, + 4 + ], + [ + 1, + 4 + ], + [ + 0, + 5 + ], + [ + -1, + 6 + ] + ], + [ + [ + 0, + 0 + ], + [ + 0, + 1 + ], + [ + -2, + 1 + ], + [ + -2, + 2 + ], + [ + -3, + 2 + ], + [ + 1, + 1 + ], + [ + -1, + 1 + ], + [ + -1, + 2 + ], + [ + -1, + 3 + ], + [ + -3, + 3 + ], + [ + 1, + 2 + ], + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + -2, + 3 + ], + [ + -2, + 4 + ], + [ + 2, + 2 + ], + [ + 1, + 3 + ], + [ + 1, + 4 + ], + [ + -1, + 4 + ], + [ + -1, + 5 + ], + [ + 2, + 4 + ], + [ + 2, + 3 + ], + [ + 0, + 4 + ], + [ + 0, + 5 + ], + [ + -1, + 6 + ] + ], + [ + [ + 0, + 0 + ], + [ + -1, + 0 + ], + [ + -1, + 1 + ], + [ + -3, + 2 + ], + [ + -4, + 2 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ], + [ + -1, + 2 + ], + [ + -2, + 2 + ], + [ + -2, + 3 + ], + [ + 1, + 1 + ], + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + -1, + 3 + ], + [ + -2, + 4 + ], + [ + 1, + 2 + ], + [ + 1, + 3 + ], + [ + 0, + 4 + ], + [ + -1, + 4 + ], + [ + -2, + 5 + ], + [ + 2, + 3 + ], + [ + 1, + 4 + ], + [ + 1, + 5 + ], + [ + 0, + 5 + ], + [ + -1, + 5 + ] + ], + [ + [ + 0, + 0 + ], + [ + -1, + 0 + ], + [ + -1, + 1 + ], + [ + -3, + 2 + ], + [ + -3, + 3 + ], + [ + 1, + 1 + ], + [ + 0, + 1 + ], + [ + -1, + 2 + ], + [ + -2, + 2 + ], + [ + -2, + 3 + ], + [ + 2, + 2 + ], + [ + 1, + 2 + ], + [ + 0, + 2 + ], + [ + -1, + 3 + ], + [ + -2, + 4 + ], + [ + 2, + 3 + ], + [ + 1, + 3 + ], + [ + 0, + 3 + ], + [ + 0, + 4 + ], + [ + -1, + 4 + ], + [ + 3, + 3 + ], + [ + 1, + 4 + ], + [ + 1, + 5 + ], + [ + 0, + 5 + ], + [ + -1, + 5 + ] + ] + ] +} diff --git a/research/unbiased-periodic-rotation/TASK.json b/research/unbiased-periodic-rotation/TASK.json new file mode 100644 index 0000000000..426bf0bcd5 --- /dev/null +++ b/research/unbiased-periodic-rotation/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Construct an unbiased seed-reversible periodic lattice rotation with pointwise minimum stochastic squared error.", + "scope_change_reason": "Original generic precision-interface construction rather than a selected-caller assumption discharge. Unbiased random ensembles change the numerical contract.", + "bottleneck_link": "Side result toward precision_tape and owned return: unbiased rounding can preserve a per-seed exact inverse without extra stochastic error, but seed and physical costs remain unpriced.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified construction or certified obstruction; do not extend the phase family.", + "outcome": "completed", + "evidence": "Exact five-table certificate and all-lattice written proof; verifier computes all 125 entries, two-sided signed return, larger quotients, large translations and rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can this interface be priced at one actual supplier phase call?", + "why_it_matters": "A mathematical ensemble alone does not reduce the paid supplier bill.", + "first_step": "Pin the phase, lattice and seed ownership; price sampling, quotient lookup and reversible restoration.", + "blocked_by": "An actual physical producer/consumer and complete invoice." + }, + { + "question": "Which other rational orthogonal operators admit unbiased nearest-cell periodic bijection ensembles?", + "why_it_matters": "The present certificate covers only one phase.", + "first_step": "Build the exact input/output lattice quotient and test its moment/capacity constraints.", + "blocked_by": "A new finite matching certificate or obstruction; no general existence claim is made." + } + ] +} diff --git a/research/unbiased-periodic-rotation/VERIFY.json b/research/unbiased-periodic-rotation/VERIFY.json new file mode 100644 index 0000000000..08bb25a4b6 --- /dev/null +++ b/research/unbiased-periodic-rotation/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": "Exact finite matching certificate, all residue moments and transversals, signed return and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact finite matching certificate, all residue moments and transversals, signed return and semantic rejection controls." + } + ] +} diff --git a/research/unbiased-periodic-rotation/construct.py b/research/unbiased-periodic-rotation/construct.py new file mode 100644 index 0000000000..4efc36e55f --- /dev/null +++ b/research/unbiased-periodic-rotation/construct.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python3 +"""Construct five exact periodic lattice rotation tables. Apache-2.0.""" +import json + + +def coset(point): + """Class in Z^2 / [[3,-4],[4,3]] Z^2.""" + x, y = point + return ((3 * x + 4 * y) % 25, (-4 * x + 3 * y) % 25) + + +def weighted_edges(): + """Return a five-regular bipartite multigraph and its literal outputs.""" + keys = sorted({coset((x, y)) for x in range(25) for y in range(25)}) + if len(keys) != 25: + raise ValueError("incorrect quotient size") + weights = [[0] * 25 for _ in range(25)] + outputs = [[None] * 25 for _ in range(25)] + for i in range(25): + x, y = divmod(i, 5) + u, a = divmod(3 * x - 4 * y, 5) + v, b = divmod(4 * x + 3 * y, 5) + both = min(a, b) if a in (1, 4) else max(0, a + b - 5) + counts = ((0, 0, 5 - a - b + both), (1, 0, a - both), + (0, 1, b - both), (1, 1, both)) + for dx, dy, count in counts: + if count > 0: + point = (u + dx, v + dy) + j = keys.index(coset(point)) + if outputs[i][j] is not None: + raise ValueError("two outputs alias in one row") + weights[i][j] = count + outputs[i][j] = point + if any(sum(row) != 5 for row in weights): + raise ValueError("incorrect input degree") + if any(sum(weights[i][j] for i in range(25)) != 5 for j in range(25)): + raise ValueError("incorrect output degree") + return weights, outputs + + +def matching(weights): + """Find one perfect matching by at most 25 bounded augmentations.""" + owners = [-1] * 25 + assigned = [-1] * 25 + for root in range(25): + queue = [root] + seen = {root} + parent = [-1] * 25 + free = -1 + for step in range(25): + if step == len(queue) or free >= 0: + break + row = queue[step] + for col in range(25): + if weights[row][col] == 0 or parent[col] >= 0: + continue + parent[col] = row + if owners[col] < 0: + free = col + break + other = owners[col] + if other not in seen: + seen.add(other) + queue.append(other) + if free < 0: + raise ValueError("regular graph has no augmenting path") + for _ in range(25): + row = parent[free] + previous = assigned[row] + assigned[row], owners[free] = free, row + if previous < 0: + break + free = previous + else: + raise ValueError("augmentation exceeds row count") + if sorted(assigned) != list(range(25)): + raise ValueError("matching is not a permutation") + return assigned + + +def construct(): + weights, outputs = weighted_edges() + tables = [] + for _ in range(5): + permutation = matching(weights) + table = [] + for i, j in enumerate(permutation): + if weights[i][j] <= 0 or outputs[i][j] is None: + raise ValueError("matching selected an absent edge") + weights[i][j] -= 1 + table.append(list(outputs[i][j])) + tables.append(table) + if any(value != 0 for row in weights for value in row): + raise ValueError("decomposition left an edge") + return {"schema_version": 1, "tables": tables} + + +if __name__ == "__main__": + print(json.dumps(construct(), indent=2)) diff --git a/research/unbiased-periodic-rotation/verify.py b/research/unbiased-periodic-rotation/verify.py new file mode 100644 index 0000000000..7226207252 --- /dev/null +++ b/research/unbiased-periodic-rotation/verify.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Exact finite certificate for an unbiased reversible rotation. Apache-2.0.""" +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from construct import construct + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def class_key(point, scale=1): + x, y = point + return ((3 * x + 4 * y) % (25 * scale), + (3 * y - 4 * x) % (25 * scale)) + + +def read_tables(): + path = HERE / "TABLE.json" + require(not path.is_symlink() and path.stat().st_size <= 65536, + "table input is linked or oversized") + document = json.loads(path.read_text(encoding="utf-8")) + require(set(document) == {"schema_version", "tables"}, "table keys") + require(type(document["schema_version"]) is int and + document["schema_version"] == 1, "table schema") + tables = document["tables"] + require(type(tables) is list and len(tables) == 5, "seed count") + for table in tables: + require(type(table) is list and len(table) == 25, "table size") + for point in table: + require(type(point) is list and len(point) == 2, "point shape") + require(all(type(v) is int and -16 <= v <= 16 for v in point), + "point coordinate") + require(document == construct(), "table differs from exact constructor") + return tables + + +def quotient_check(tables): + keys = {class_key((x, y)) for x in range(25) for y in range(25)} + require(len(keys) == 25, "incorrect quotient order") + for table in tables: + require({class_key(point) for point in table} == keys, + "outputs are not a quotient transversal") + + +def moment_check(tables): + nonintegral = 0 + worst = 0 + for i in range(25): + x, y = divmod(i, 5) + a, b = 3 * x - 4 * y, 4 * x + 3 * y + require(sum(table[i][0] for table in tables) == a, "first moment x") + require(sum(table[i][1] for table in tables) == b, "first moment y") + total = 0 + for table in tables: + u, v = table[i] + require(a // 5 <= u <= -((-a) // 5), "x outside nearest cell") + require(b // 5 <= v <= -((-b) // 5), "y outside nearest cell") + residual = (5 * u - a) ** 2 + (5 * v - b) ** 2 + total += residual + worst = max(worst, residual) + fractional = bool(a % 5 or b % 5) + nonintegral += fractional + require(total == (50 if fractional else 0), "squared error moment") + require(nonintegral == 20 and worst == 20, "error census") + return nonintegral, worst + + +def forward(point, table): + x, y = point + q, r = divmod(x, 5) + s, t = divmod(y, 5) + u, v = table[5 * r + t] + return (3 * q - 4 * s + u, 4 * q + 3 * s + v) + + +def inverse(point, table, lookup): + i = lookup[class_key(point)] + x, y = divmod(i, 5) + u, v = table[i] + a, b = point[0] - u, point[1] - v + q, r = divmod(3 * a + 4 * b, 25) + s, t = divmod(3 * b - 4 * a, 25) + require(r == 0 and t == 0, "inverse lattice membership") + return (5 * q + x, 5 * s + y) + + +def literal_checks(tables): + roundtrips = 0 + for table in tables: + lookup = {class_key(point): i for i, point in enumerate(table)} + for x in range(-20, 21): + for y in range(-20, 21): + point = (x, y) + require(inverse(forward(point, table), table, lookup) == point, + "left inverse") + require(forward(inverse(point, table, lookup), table) == point, + "right inverse") + roundtrips += 2 + return roundtrips + + +def quotient_oracle(tables): + """Independent direct formula on four larger lattice quotients.""" + cases = 0 + for scale in range(1, 5): + for table in tables: + images = set() + for x in range(5 * scale): + for y in range(5 * scale): + q, s = x // 5, y // 5 + u, v = table[(x % 5) * 5 + y % 5] + point = (3 * q - 4 * s + u, 4 * q + 3 * s + v) + images.add(class_key(point, scale)) + cases += 1 + require(len(images) == 25 * scale * scale, "larger quotient alias") + return cases + + +def large_checks(tables): + cases = 0 + for bits in (1, 17, 64, 256, 1024): + for sign in (-1, 1): + shift = (sign * (1 << bits), -sign * ((1 << bits) + 3)) + for table in tables: + lookup = {class_key(point): i for i, point in enumerate(table)} + for i in range(25): + r, t = divmod(i, 5) + point = (5 * shift[0] + r, 5 * shift[1] + t) + result = forward(point, table) + u, v = table[i] + require(result == (3 * shift[0] - 4 * shift[1] + u, + 4 * shift[0] + 3 * shift[1] + v), + "signed covariance") + require(inverse(result, table, lookup) == point, + "large inverse") + cases += 1 + return cases + + +def rejection_controls(tables): + controls = 0 + broken = [[list(point) for point in table] for table in tables] + broken[0][1] = list(broken[0][0]) + try: + quotient_check(broken) + except ValueError: + controls += 1 + else: + raise ValueError("duplicate-output mutant accepted") + broken = [[list(point) for point in table] for table in tables] + broken[0][0][0] += 3 + broken[0][0][1] += 4 + quotient_check(broken) # Same coset, so bijection alone cannot check the mean. + try: + moment_check(broken) + except ValueError: + controls += 1 + else: + raise ValueError("biased-transversal mutant accepted") + require(any(inverse(forward((x, y), tables[0]), tables[1], + {class_key(p): i for i, p in enumerate(tables[1])}) != (x, y) + for x in range(5) for y in range(5)), "forgotten seed control") + controls += 1 + require(5 * tables[0][5][0] != 3 or 5 * tables[0][5][1] != 4, + "fixed seed incorrectly claimed unbiased") + return controls + 1 + + +def independent_rounding_control(): + """Independent coordinate rounding has the right mean but wrong capacity.""" + columns = {} + for x in range(5): + for y in range(5): + u, a = divmod(3 * x - 4 * y, 5) + v, b = divmod(4 * x + 3 * y, 5) + for dx in range(2): + for dy in range(2): + weight = (a if dx else 5 - a) * (b if dy else 5 - b) + key = class_key((u + dx, v + dy)) + columns[key] = columns.get(key, 0) + weight + require(sum(columns.values()) == 625, "independent rounding row mass") + require(any(value != 25 for value in columns.values()), + "independent rounding unexpectedly preserves output capacity") + return 1 + + +def receipt(): + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "construct.py", "verify.py", "TABLE.json") + hashes = {} + for name in names: + path = HERE / name + require(not path.is_symlink() and path.stat().st_size <= 1048576, + "linked or oversized package file") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return hashes + + +def main(): + require(len(sys.argv) == 1, "no command arguments are supported") + tables = read_tables() + quotient_check(tables) + nonintegral, worst = moment_check(tables) + result = {"seed_count": 5, "residue_classes": 25, + "nonintegral_classes": nonintegral, + "nonintegral_minimum_squared_error": "2/5", + "maximum_squared_error": f"{worst}/25", + "two_sided_roundtrips": literal_checks(tables), + "larger_quotient_images": quotient_oracle(tables), + "large_signed_cases": large_checks(tables), + "controls": rejection_controls(tables) + independent_rounding_control(), + "sha256": receipt()} + print(json.dumps(result, sort_keys=True)) + print("PASS_UNBIASED_PERIODIC_ROTATION") + + +if __name__ == "__main__": + main()