From 44a7d2c1b53597c3a79e01698f8d9d11533367fd Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 19:40:22 +0000 Subject: [PATCH 1/2] feat(research): construct a corrected two-guard reciprocal --- .../reciprocal-two-guard-correction/PROOF.md | 144 ++++++++++++++ .../reciprocal-two-guard-correction/README.md | 114 +++++++++++ .../SOURCES.json | 30 +++ .../reciprocal-two-guard-correction/TASK.json | 111 +++++++++++ .../VERIFY.json | 35 ++++ .../reciprocal.py | 67 +++++++ .../reciprocal-two-guard-correction/verify.py | 179 ++++++++++++++++++ 7 files changed, 680 insertions(+) create mode 100644 research/reciprocal-two-guard-correction/PROOF.md create mode 100644 research/reciprocal-two-guard-correction/README.md create mode 100644 research/reciprocal-two-guard-correction/SOURCES.json create mode 100644 research/reciprocal-two-guard-correction/TASK.json create mode 100644 research/reciprocal-two-guard-correction/VERIFY.json create mode 100644 research/reciprocal-two-guard-correction/reciprocal.py create mode 100644 research/reciprocal-two-guard-correction/verify.py diff --git a/research/reciprocal-two-guard-correction/PROOF.md b/research/reciprocal-two-guard-correction/PROOF.md new file mode 100644 index 0000000000..6e77cf00fe --- /dev/null +++ b/research/reciprocal-two-guard-correction/PROOF.md @@ -0,0 +1,144 @@ +# A two-guard reciprocal with a bounded correction + +For every real `1 <= c < 2` and positive integer `p`, the algorithm below +returns a dyadic `y` with `|1-cy| < 2^(-p-1)`. Every Newton step uses two +fractional guard bits relative to its stage index. The unchanged warm-up +uses six fractional bits. The maximum rounded precision is `max(6,p+2)`. +Exact intermediate products remain required, as in the predecessor interface. + +## Algorithm + +Write `R_t(z)=floor(2^t z)/2^t`. Define + +```text +N_t(x) = R_t(x * (2 - R_t(R_t(c) * x))). +x = N_6(5/8); m = 2 +while m < p: + m = min(2*m-1,p) + x = N_(m+2)(x) +t = p+2; S = 2^t +n = floor(S*x); C = floor(S*c) +J = {j in Z : n-6 <= j <= n+6 and S/2 <= j <= S} +choose the smallest j minimizing |S^2-C*j| over J +return y = j/S +``` + +An incoming iterate retains its stored precision, including when the first +Newton step uses fewer than six bits. No reciprocal or division by `c` is +used by the correction. It tests at most thirteen integer products. Reading +a binary prefix, exact products and floor rounding are the stipulated +arithmetic operations; no physical tape implementation is inferred. + +## Stage invariant + +The directed-error identity from ToikY's PR #1638 is useful here. Put +`e=1-cx`, `delta=2^-t`, `h=c-R_t(c)`, +`a=R_t(c)*x-R_t(R_t(c)*x)` and `b=x*(2-u)-N_t(x)`, where +`u=R_t(R_t(c)*x)`. Each of `h,a,b` belongs to `[0,delta)`, and expansion gives + +```math +e_+ = e^2-c h x^2-c x a+c b. +``` + +At the seed `x=5/8`, `|e|<=3/8`, `cx<5/4` and `cx^2<25/32`. +Thus the six-bit warm-up satisfies + +```math +-65/2048 < e_+ < 11/64 < 1/4. +``` + +The upper bound uses `e^2<=9/64` and `cb<2/64`; the lower bound discards +`e^2` and uses `(25/32+5/4)/64=65/2048`. This establishes the invariant +`|e|<2^-m` at `m=2`. Both signs and positivity of the warm-up output follow. + +Suppose `m>=2` and `|e|<2^-m`. Then `x>0`, `cx<5/4`, and +`cx^2=(cx)^2/c<25/16`. At the next stage `m'<=2m-1` with +`delta=2^(-m'-2)`, the same identity implies + +```math +e_+ > -(25/16+5/4)delta = -(45/64)2^{-m'} > -2^{-m'}, +``` + +```math +e_+ < 2^{-2m}+2delta <= (1/2+1/2)2^{-m'} = 2^{-m'}. +``` + +So the invariant is preserved for every real normalized input. The stage +index strictly increases, since `2m-1>m` for `m>=2`. For `p>=2`, it reaches +`p` in exactly `L=ceil(log2(p-1))` updates: before capping, `m_k=2^k+1`. +For `p=1` no update is needed and the warm-up already satisfies +`|e|<2^-p`. Consequently the iterate before correction satisfies + +```math +|x-1/c| < 2^{-p}/c <= 4 delta, +``` + +now with `t=p+2` and `delta=2^-t`. + +## Why thirteen candidates suffice + +Set `q=R_t(c)`. Then `1<=q<2` and `0<=c-q0` and the tie rule agrees. In particular, `J` is nonempty. +The true residual satisfies + +```math +|1-cz| <= |1-qz|+(c-q)z + <= q delta/2+(c-q)z + < delta+delta = 2^{-p-1}. +``` + +This strict inequality proves the claimed all-real-input residual contract. +It does not assert correct rounding of `1/c`. + +## Arithmetic bill and scope + +Put `L=0` for `p=1`, and `L=ceil(log2(p-1))` otherwise. The construction +uses `L+1` Newton updates, hence exactly `2(L+1)` exact products in those +updates. The correction enumerates at most thirteen candidates, uses one +integer product per candidate, and at most twelve score comparisons. Its +products satisfy `0<=Cj<2^(2t+1)` and therefore need at most `2t+1` bits. +Prefix extraction, shifts, subtractions, absolute values and loop control +remain additional operations. At most `L+2` prefix reads suffice without +reusing the last one. This is an arithmetic count, not a bit-time or tape bill. + +For `p>=4` the largest rounded fractional precision is `p+2`, one bit below +the credited three-guard routine's `p+3`. The extra correction products prevent +any runtime comparison from this fact alone. For small targets the fixed +six-bit warm-up dominates. Optimality of two guards and of the thirteen-point +window is unclaimed. The finite implementation caps `p` at 4096 and rational +input numerator/denominator lengths at 16384 bits; the mathematical argument +above has neither cap. + +This is a changed schedule and output correction, so it does not contradict +Charles Bethin's PR #1655 lower bound for the unchanged schedule. The numerical +reciprocal is a downstream arithmetic corollary, not the selected multiplication +supplier. No selected assumption, physical caller, complete multiplication +theorem or new kappa is established. + +## Credit + +This proof was produced by Nick Petalas. Credit Charles Bethin / cbethin, +PR #1655, for the changed-schedule question and fixed-schedule boundary; +ToikY, PR #1638, for the directed-error identity and three-guard theorem; +Hanson Sun / bbMisk, PR #1528, and the retained manuscript and classical +Brent/Newton lineage. Binary rounding and nearest-grid correction are +classical. The contribution is the stated schedule, bounded correction, +all-input guarantee and explicit arithmetic bill. Apache-2.0. diff --git a/research/reciprocal-two-guard-correction/README.md b/research/reciprocal-two-guard-correction/README.md new file mode 100644 index 0000000000..50cbcecc4c --- /dev/null +++ b/research/reciprocal-two-guard-correction/README.md @@ -0,0 +1,114 @@ +# A two-guard reciprocal with thirteen-candidate correction + +A changed seeded reciprocal routine satisfies `|1-cy| < 2^(-p-1)` for every +real `1 <= c < 2` and positive integer `p`, with two fractional guard bits +per Newton stage and a final correction using at most thirteen products. +The fixed six-bit warm-up remains. For `p>=4`, the maximum rounded precision +falls from the credited three-guard routine's `p+3` to `p+2`. + +Claim type: a scoped written mathematical proof and explicit numerical +construction, corroborated by exact finite enumeration. No runtime or kappa +improvement is claimed. Extra products, exact intermediate products, physical +tape costs and caller integration remain payable. + +The stage index starts at two and advances to `min(2m-1,p)`. Its weaker +invariant `|1-cx|<2^-m` permits two guard bits. The last correction searches +thirteen adjacent grid positions against the truncated input. [PROOF.md](PROOF.md) +proves that this window contains the nearest reciprocal of that prefix and +that its true-input residual meets the required strict bound. It also counts +the complete arithmetic operations of this new numerical interface. + +This answers the changed-schedule question in Charles Bethin / cbethin's +[PR #1655](https://github.com/CrocSwap/integer-mult-bounds/pull/1655). +Its unchanged-schedule lower bound, ToikY's +[PR #1638](https://github.com/CrocSwap/integer-mult-bounds/pull/1638) +upper theorem and Ross Richardson's +[PR #1678](https://github.com/CrocSwap/integer-mult-bounds/pull/1678) +failure-locus census are cited context. They are not replayed or audited. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226175) +records the delivered scope. + +## Evidence + +The verifier covers every real input by prefix cells for targets 1 through 12: +32,896 half-open cells, checking both residual endpoints. A separate integer +significand implementation checks each Newton trace, and an exact-division +oracle checks final selection without importing the construction's helpers. +There are also 95 cases through target 4096, including inputs near both +normalization endpoints, and twelve rejecting input/result controls. + +For example, at `c=127379/65536`, `p=15`, the new routine returns +`16859/32768`, with residual `1087/2147483648 < 2^-16`. +This is the new routine's output, not a recheck of the predecessor execution. +The all-target theorem rests on the written induction, not the finite census. + +The Python implementation supports rational inputs and targets through 4096, +with a 16384-bit input-size cap. The proof permits arbitrary positive targets +and real inputs, interpreted through finite binary prefixes. It assumes exact +products before floor rounding. No correctly rounded reciprocal, sharp guard +minimum, independent human review or proof-kernel acceptance is claimed. + +## Reproduce + +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/reciprocal-two-guard-correction +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/reciprocal-two-guard-correction/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/reciprocal-two-guard-correction --check-source-history +``` + +The scientific marker is `PASS_TWO_GUARD_RECIPROCAL`; the registered launcher +must report `PASS_REGISTERED_RESEARCH_PACKAGE`. Both warning-strict normal and +optimized checks are registered. `verify.py --receipt /absolute/new/path.json` +optionally generates an exclusive-create receipt bound to every package file +and live source hash. Default replay writes no files. + +## Scope, sources and credit + +Base main is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +[SOURCES.json](SOURCES.json) binds the exact predecessor documentation, task +catalogue and selected record. The source documentation is authenticated before +the new checks; predecessor executables are never imported. Overlap checks +included live open PRs and Discussions, this account's recent work, merged PR +searches and main's reciprocal/guard/correction terminology. These searches +establish bounded text coverage, not exhaustive novelty. + +The original `uniform-transfer-audit` card is explicitly changed to a numerical +side result. This downstream reciprocal corollary is outside the selected +supplier. The five selected assumptions remain; the selected frontier is +unchanged. No complete root/recovery caller, physical rounder, fixed-tape +machine or multiplication algorithm is built. + +The construction, proof and verifier were produced by Nick Petalas. +Credit Charles Bethin / cbethin #1655 for the open question, ToikY #1638 +for the directed-rounding framework, Hanson Sun / bbMisk #1528, the retained +manuscript and classical Brent/Newton lineage. Ross Richardson #1678 supplies +separate fixed-schedule context. Source files and their credit lines remain +unchanged. New work is Apache-2.0. Independent human and formal proof-kernel +review are unclaimed. + +The Investigation playbook shaped the bounded question. Build the Lever +produced the reusable exact verifier; Prove It Works required literal +prefix-cell endpoints and a separate arithmetic oracle. Power of Ten is +applied with a managed-Python allocation deviation: input caps bound integer +sizes, loops are bounded, functions remain below sixty lines, and normal and +optimized executions retain explicit failure checks. No recursion or hidden +background work is used. Python and Fraction necessarily allocate dynamically; +no allocation-free claim is made. + +## Open next questions + +- Can the final window be reduced or its search replaced by fewer products? + This matters to a real cost comparison. First prove a sharper signed + pre-correction bound, then test the reduced window. No optimality proof is + currently supplied. +- Can one guard bit work with another correction or input-prefix contract? + First derive a true-input interval invariant and state the additional prefix + precision explicitly. This theorem proves sufficiency of two only. +- Can this exact arithmetic routine replace the numerical call in the retained + root/recovery algorithm? First bind its prefix reads, full product widths, + correction and storage to that caller. Physical tape and complete bit-time + costs are unproved. + +Structured questions and blockers are in [TASK.json](TASK.json). diff --git a/research/reciprocal-two-guard-correction/SOURCES.json b/research/reciprocal-two-guard-correction/SOURCES.json new file mode 100644 index 0000000000..61ccfc7e6a --- /dev/null +++ b/research/reciprocal-two-guard-correction/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/reciprocal-directed-guards/README.md", + "usage": "input", + "git_blob": "648f25fd805c6d86dbcf37d0094c59e48b5eef17", + "sha256": "ab3dacefe101f07f2b6a9989a3ff3591328ae5b87b64e247a194ab2dbc5a0cae" + }, + { + "path": "research/reciprocal-seeded-guard-boundary/README.md", + "usage": "input", + "git_blob": "d19981d5fd17b268b9601cadad11e00e56616460", + "sha256": "c287b4add9bda7323b426faf7e0e5aa156ec14dfe0de1cfe2898dfd149bf6aa2" + } + ] +} diff --git a/research/reciprocal-two-guard-correction/TASK.json b/research/reciprocal-two-guard-correction/TASK.json new file mode 100644 index 0000000000..717d2d3bce --- /dev/null +++ b/research/reciprocal-two-guard-correction/TASK.json @@ -0,0 +1,111 @@ +{ + "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": "Construct a changed seeded reciprocal schedule and bounded correction satisfying the all-real residual contract with two fractional guard bits.", + "scope_change_reason": "Take the explicit changed-schedule question in cbethin PR1655. This downstream numerical corollary is a side result, not an attempt to discharge a selected supplier assumption.", + "bottleneck_link": "Side result in numerical precision: removes one rounded fractional bit for p>=4, while adding at most thirteen correction products. No selected supplier or kappa improvement follows.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved and exactly corroborated two-guard construction. Do not optimize the correction window or target a further result.", + "outcome": "completed", + "evidence": "PROOF.md all-real-input induction and correction theorem; 32896 exhaustive prefix cells at p=1..12; 95 large cases through p=4096; separate integer and division oracles; twelve rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the correction window or product count be reduced?", + "why_it_matters": "Correction products can dominate any benefit of one fewer fractional bit.", + "first_step": "Prove a sharper signed iterate error and derive a smaller attaining window.", + "blocked_by": "No optimal window or cost comparison is supplied." + }, + { + "question": "Can one guard work under a changed correction or input-prefix contract?", + "why_it_matters": "Two is a sufficient allowance, not a proved minimum.", + "first_step": "Derive a true-input interval bound with explicitly charged prefix precision.", + "blocked_by": "No one-guard invariant is proved." + }, + { + "question": "Can the new numerical interface be installed in the retained root/recovery caller?", + "why_it_matters": "The arithmetic theorem is not a physical implementation or selected supplier.", + "first_step": "Bind every prefix read, product, correction and stored field to the actual caller.", + "blocked_by": "Physical tape, storage and complete bit-time accounting are absent." + } + ], + "source_question": { + "pr": 1655, + "author": "cbethin", + "question": "Does a modified final capped stage permit a two-guard schedule with a separately proved residual contract?" + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226175", + "upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "checked_at_utc": "2026-10-27T19:33:09Z" + }, + "implementation_limits": { + "maximum_target": 4096, + "maximum_input_bits": 16384, + "proof_target_limit": null + } +} diff --git a/research/reciprocal-two-guard-correction/VERIFY.json b/research/reciprocal-two-guard-correction/VERIFY.json new file mode 100644 index 0000000000..eebccc22f4 --- /dev/null +++ b/research/reciprocal-two-guard-correction/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/reciprocal-directed-guards/README.md", + "research/reciprocal-seeded-guard-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 32896 real-input prefix cells, two arithmetic representations, exact nearest-grid oracle, 95 high-precision cases and 12 rejecting controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same semantic coverage with assertions disabled." + } + ] +} diff --git a/research/reciprocal-two-guard-correction/reciprocal.py b/research/reciprocal-two-guard-correction/reciprocal.py new file mode 100644 index 0000000000..631d0cd1ec --- /dev/null +++ b/research/reciprocal-two-guard-correction/reciprocal.py @@ -0,0 +1,67 @@ +"""Two-guard reciprocal construction; see PROOF.md for the real-input theorem.""" + +from dataclasses import dataclass +from fractions import Fraction + +MAX_TARGET = 4096 + + +@dataclass(frozen=True) +class Result: + value: Fraction + stages: tuple[tuple[int, int, Fraction], ...] + center: int + selected: int + candidates: int + + +def floor_grid(value: Fraction, bits: int) -> Fraction: + if not 0 <= bits <= MAX_TARGET + 2: + raise ValueError("unsupported grid precision") + scale = 1 << bits + return Fraction((value.numerator << bits) // value.denominator, scale) + + +def newton_step(c: Fraction, x: Fraction, bits: int) -> Fraction: + prefix = floor_grid(c, bits) + product = floor_grid(prefix * x, bits) + return floor_grid(x * (2 - product), bits) + + +def evaluate(c: Fraction, target: int) -> Result: + """Use two fractional guard bits and a bounded final correction. + + This research implementation caps targets at 4096. The written arithmetic + proof covers every positive integer target. No division by c is used. + """ + if type(target) is not int or not 1 <= target <= MAX_TARGET: + raise ValueError("target must be an integer in 1..4096") + if not isinstance(c, Fraction) or not 1 <= c < 2: + raise ValueError("input must be a rational in [1,2)") + if max(c.numerator.bit_length(), c.denominator.bit_length()) > 16384: + raise ValueError("rational input exceeds the research bit budget") + x = newton_step(c, Fraction(5, 8), 6) + m = 2 + stages = [(m, 6, x)] + for _ in range(max(0, target - 2)): + if m >= target: + break + m = min(2 * m - 1, target) + x = newton_step(c, x, m + 2) + stages.append((m, m + 2, x)) + scale = 1 << (target + 2) + center = (x.numerator << (target + 2)) // x.denominator + prefix = (c.numerator << (target + 2)) // c.denominator + candidates = tuple(j for j in range(center - 6, center + 7) + if scale // 2 <= j <= scale) + if not candidates: + raise ArithmeticError("empty correction window") + unit = 1 << (2 * (target + 2)) + selected = candidates[0] + best = abs(unit - prefix * selected) + for j in candidates[1:]: + score = abs(unit - prefix * j) + if score < best: + selected, best = j, score + return Result(Fraction(selected, scale), tuple(stages), center, + selected, len(candidates)) diff --git a/research/reciprocal-two-guard-correction/verify.py b/research/reciprocal-two-guard-correction/verify.py new file mode 100644 index 0000000000..677a35c9a9 --- /dev/null +++ b/research/reciprocal-two-guard-correction/verify.py @@ -0,0 +1,179 @@ +"""Bounded exact checks of the new construction, not predecessor replays.""" + +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +import json +from pathlib import Path +import platform + +from reciprocal import MAX_TARGET, Result, evaluate, floor_grid + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ArithmeticError(message) + + +def authenticate() -> dict[str, str]: + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + hashes = {} + for row in sources["files"]: + if row["usage"] == "input": + digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + require(digest == row["sha256"], "source digest: " + row["path"]) + hashes[row["path"]] = digest + return hashes + + +def integer_oracle(c: Fraction, target: int) -> tuple[Fraction, list[Fraction]]: + """Separate dyadic-significand traversal and division-based final oracle.""" + numerator, denominator = c.numerator, c.denominator + x, stored = 5, 3 + values = [] + steps = (target - 2).bit_length() if target >= 2 else 0 + for index in range(steps + 1): + bits = 6 if index == 0 else min((1 << index) + 1, target) + 2 + prefix = (numerator << bits) // denominator + u = prefix * x // (1 << stored) + x = x * ((2 << bits) - u) // (1 << stored) + stored = bits + values.append(Fraction(x, 1 << stored)) + scale = 1 << (target + 2) + prefix = numerator * scale // denominator + quotient, remainder = divmod(scale * scale, prefix) + nearest = quotient + int(2 * remainder > prefix) + return Fraction(nearest, scale), values + + +def check_result(c: Fraction, target: int, result: Result) -> None: + oracle, stages = integer_oracle(c, target) + require(result.value == oracle, "nearest-prefix inverse disagreement") + require([r[2] for r in result.stages] == stages, "integer trace disagreement") + require(1 <= result.candidates <= 13, "candidate count") + require(abs(result.selected - result.center) <= 6, "correction radius") + require(result.value == Fraction(result.selected, 1 << (target + 2)), + "selected grid coordinate") + scale = 1 << (target + 2) + require(result.center == (result.stages[-1][2] * scale).__floor__(), + "correction center") + eligible = [j for j in range(result.center - 6, result.center + 7) + if scale // 2 <= j <= scale] + require(result.candidates == len(eligible), "enumerated candidate count") + require(result.selected in eligible, "eligible selected coordinate") + incoming, m = Fraction(5, 8), 2 + for index, (stage, bits, outgoing) in enumerate(result.stages): + if index: + m = min(2 * m - 1, target) + require(stage == m and bits == (m + 2 if index else 6), "schedule") + scale = 1 << bits + prefix = Fraction(c.numerator * scale // c.denominator, scale) + u = Fraction((prefix * incoming * scale).__floor__(), scale) + raw = incoming * (2 - u) + require(0 <= raw - outgoing < Fraction(1, scale), "output floor") + require(0 <= prefix * incoming - u < Fraction(1, scale), "product floor") + require(abs(1 - c * outgoing) < Fraction(1, 1 << m), "stage invariant") + incoming = outgoing + require(abs(1 - c * result.value) < Fraction(1, 1 << (target + 1)), + "target residual") + + +def prefix_cells() -> dict[str, object]: + counts = Counter() + offsets = Counter() + for target in range(1, 13): + bits = max(6, target + 2) + scale = 1 << bits + bound = Fraction(1, 1 << (target + 1)) + for cell in range(scale, 2 * scale): + low = Fraction(cell, scale) + high = Fraction(cell + 1, scale) + result = evaluate(low, target) + check_result(low, target, result) + # Prefixes are constant on [low,high); the residual is affine. + require(abs(1 - high * result.value) <= bound, "open cell endpoint") + counts[target] += 1 + offsets[result.selected - result.center] += 1 + return {"cells_by_target": dict(counts), "cells": sum(counts.values()), + "selected_offsets": dict(sorted(offsets.items()))} + + +def large_cases() -> int: + count = 0 + for target in (13, 15, 16, 17, 31, 32, 33, 63, 64, 65, 127, 128, + 129, 255, 256, 257, 511, 512, 4096): + for c in (Fraction(1), Fraction(3, 2), Fraction(127379, 65536), + 2 - Fraction(1, 1 << (target + 4)), + 1 + Fraction(1, 1 << (target + 4))): + check_result(c, target, evaluate(c, target)) + count += 1 + return count + + +def rejection_controls() -> int: + count = 0 + for c, target in ((Fraction(0), 3), (Fraction(2), 3), (Fraction(1), 0), + (Fraction(1), MAX_TARGET + 1), (Fraction(1), True), + (Fraction((1 << 16385) + 1, 1 << 16385), 3)): + try: + evaluate(c, target) + except ValueError: + count += 1 + else: + raise ArithmeticError("accepted invalid input") + for bits in (-1, MAX_TARGET + 3): + try: + floor_grid(Fraction(1), bits) + except ValueError: + count += 1 + else: + raise ArithmeticError("accepted invalid grid") + c, target = Fraction(127379, 65536), 15 + result = evaluate(c, target) + mutants = ( + Result(result.value + Fraction(1, 2), result.stages, result.center, + result.selected, result.candidates), + Result(result.value, result.stages[:-1], result.center, + result.selected, result.candidates), + Result(result.value, result.stages, result.center + 20, + result.selected, result.candidates), + Result(result.value, result.stages, result.center, result.selected, 14), + ) + for mutant in mutants: + try: + check_result(c, target, mutant) + except ArithmeticError: + count += 1 + else: + raise ArithmeticError("accepted corrupt result") + return count + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + sources = authenticate() + cells = prefix_cells() + large = large_cases() + controls = rejection_controls() + witness = evaluate(Fraction(127379, 65536), 15) + residual = 1 - Fraction(127379, 65536) * witness.value + result = {"status": "PASS_TWO_GUARD_RECIPROCAL", "python": platform.python_version(), + **cells, "large_cases": large, "rejections": controls, + "witness_output": str(witness.value), "witness_residual": str(residual), + "sources": sources, "package_sha256": { + p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(PACKAGE.iterdir()) if p.is_file()}} + if args.receipt: + with args.receipt.open("x") as output: + output.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() From cd0caac542b147743f273d6e3377a0eec3e4b6e4 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 19:41:29 +0000 Subject: [PATCH 2/2] docs(research): keep reciprocal notes focused on the result --- research/reciprocal-two-guard-correction/README.md | 9 --------- research/reciprocal-two-guard-correction/TASK.json | 3 ++- 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/research/reciprocal-two-guard-correction/README.md b/research/reciprocal-two-guard-correction/README.md index 50cbcecc4c..80b48b30d5 100644 --- a/research/reciprocal-two-guard-correction/README.md +++ b/research/reciprocal-two-guard-correction/README.md @@ -88,15 +88,6 @@ separate fixed-schedule context. Source files and their credit lines remain unchanged. New work is Apache-2.0. Independent human and formal proof-kernel review are unclaimed. -The Investigation playbook shaped the bounded question. Build the Lever -produced the reusable exact verifier; Prove It Works required literal -prefix-cell endpoints and a separate arithmetic oracle. Power of Ten is -applied with a managed-Python allocation deviation: input caps bound integer -sizes, loops are bounded, functions remain below sixty lines, and normal and -optimized executions retain explicit failure checks. No recursion or hidden -background work is used. Python and Fraction necessarily allocate dynamically; -no allocation-free claim is made. - ## Open next questions - Can the final window be reduced or its search replaced by fewer products? diff --git a/research/reciprocal-two-guard-correction/TASK.json b/research/reciprocal-two-guard-correction/TASK.json index 717d2d3bce..13fb21e0b8 100644 --- a/research/reciprocal-two-guard-correction/TASK.json +++ b/research/reciprocal-two-guard-correction/TASK.json @@ -106,6 +106,7 @@ "implementation_limits": { "maximum_target": 4096, "maximum_input_bits": 16384, - "proof_target_limit": null + "proof_target_limit": null, + "allocation_deviation": "Managed Python and Fraction allocate dynamically. Input caps bound integer lengths; finite target ranges and a thirteen-candidate window bound loops and live collections. No allocation-free guarantee is claimed." } }