Construct a corrected two-guard reciprocal (no new κ)

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-q<delta`, so
+
+```math
+0 <= 1/q-1/c = (c-q)/(cq) < delta.
+```
+
+Let `z` be the nearest point to `1/q` on the `delta` grid, with ties rounded
+down. Since `1/2<1/q<=1`, we have `1/2<=z<=1` and
+`|z-1/q|<=delta/2`. Also `0<=x-n delta<delta`. The triangle inequality gives
+
+```math
+|z-n delta| < (1/2+1+4+1)delta = (13/2)delta.
+```
+
+Both `z/delta` and `n` are integers. Their difference therefore has absolute
+value at most six. Thus `z` is among the candidates `J`, including when
+`p=1` or `p=2` and the warm-up was stored on a finer grid.
+
+Minimizing `|S^2-Cj|` is exactly minimizing `|1-q(j/S)|`. It chooses `z`,
+because `q>0` 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.

research/reciprocal-two-guard-correction/README.md

@@ -0,0 +1,105 @@
+# 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.
+
+## 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).

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"
+    }
+  ]
+}

research/reciprocal-two-guard-correction/TASK.json

@@ -0,0 +1,112 @@
+{
+  "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,
+    "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."
+  }
+}