[petalas]

Summary

Scoped proof with exact finite corroboration. Answer the rounded-child question left by Hanson Sun / bbMisk in PR1526 for its two dyadic conjugations and displayed B0 repair.

refined H B D: z -> z + Q_h(2 Bx), sharp error h/2
complete B0 repair: z_final - z_initial = Q_h(2 Bx) - 2 Q_h(Bx)
                                                   in {-h, 0, h}

Here Q_h(t)=h floor(t/h+1/2), scales are exact, and signed queries apply their sign after rounding. One additional root fractional bit halves the local source-query error, but can break the complete dirty-root boundary. All three residual values occur. Coarse rounding preserves cancellation; a final ternary correction also restores the root and requires its own paid implementation. The output conjugation D A H has sharp h/2 error and restores its root.

The new result was produced by Nick Petalas. Credit Hanson Sun / bbMisk for PR1526's exact word and question, Ross Richardson / PR944, martinxxx9 / PR1088 and the retained signed-connector lineage. The predecessor optimum is cited, not replayed. Classical nearest rounding is not claimed new. Independent human and formal proof-kernel review are unclaimed.

Evidence

• Before: the exact-arithmetic conjugations have no rounded-child guarantee. The explicit refined extension leaves root error 1 at h=1, B0=1/8, x0=3.
• After: the written proof gives the exact residual formula, its complete three-interval classification, sharp local bounds and two root-boundary repairs. The verifier enumerates 3,402 source intervals, 1,050 output intervals, 102 complete rounded-word fixtures and eight controls. Full literal inverses pass.
• CPython 3.12.15, Darwin arm64. Both registered commands passed locally, timed separately at 0.099 s normal and 0.105 s optimized. These are check durations, not a speedup claim. The registered runner passed in 0.580 s. Later metadata-only source-head recording changes receipt hashes but no scientific code; the final committed package replay also passed.
• Committed bytes/source history pass for seven files. Official export integrity and its one declared input pass. Normal and optimized read-only Git-free export runs pass with empty PATH. An actual corrupted source export is rejected. Receipts are generated from execution and bind all six package file hashes.

From the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-dyadic-conjugation
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rounded-dyadic-conjugation/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rounded-dyadic-conjugation/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-dyadic-conjugation --check-source-history

Other machines can replace the interpreter path with their CPython 3.12 executable. No dependencies beyond the standard library are required. Direct success marker: PASS_ROUNDED_DYADIC_CONJUGATION; registered success marker: PASS_REGISTERED_RESEARCH_PACKAGE.

Limitations

This is one specified deterministic additive rounding contract and one displayed B0 repair. Exact H/D, source independence, tie handling and the literal inverse convention are hypotheses. A complete connector output-error budget, actual recursive/native child, correction evaluation/delivery cost, physical invoice, compiler, stock, precision/tape and outer recovery remain unproved. No selected cold replay, Lean, Docker, native admission, new kappa or selected-frontier change is claimed. All five selected framework assumptions remain.

Open next questions

• Price a native B child and the source-only ternary repair, including both root scans, coefficient evaluation, routing and restoration. Determine whether the removed-child allowance survives.
• Propagate the repaired word's complete output errors under a specified native norm and caller allowance. Root restoration and a local radius do not supply that budget.

Related open work

The completion refresh inspected all 112 account open PRs, including fifteen created since the advance CLAIM and fourteen other than this PR. None reports a competing value for PR1526's rounded B0 repair or its root-carry quantity. No additional scientific computations checked those contributions.

• PR6561 proves equivariant rounding radii for integer frame groups. Its simultaneous group-equivariance contract differs from this fixed scalar query and dirty-root restoration contract; no competing value for either contract is computed here.
• PR6566 proves read-set dominance for exact joint connector synthesis. Its binary search-state and read-cost quantities differ from this deterministic rounded dyadic carry.
• PR6568 constructs exact unsigned finite-characteristic connector words from balanced closed walks. It does not study rounded root carries or this characteristic-zero signed B0 repair.

PR1556's merged unit-phase tariff and PR1770's merged binary five-source invoice concern different exact interfaces. Sparse notes, unpublished work and arbitrary historical diffs remain overlap limits.

Advance claim. Canonical base: 7c49fe32c55de02c2c873655c804b16e4c3fef0a; source PR1526 head: 1fb85dc6813b88483f4f0a359ccd722376acd292.

CI notes

Both hosted checks passed at exact head 983c2cebd7946c26a1251c07ea7dabff601d5243 in run 41609885089: plan and replay (research/rounded-dyadic-conjugation).

The completed checks were read once. Separate run metadata confirms completed success and the matching head. Hosted replay executes both registered warning-strict normal and optimized commands. Package validation, direct and registered finite checks, committed-byte/source-history checks, export integrity/input coverage and both read-only Git-free export modes also passed locally. No required package check remains unrun. Hosted execution certifies the bounded registered checks, not independent human or formal proof-kernel acceptance of the universal argument. The stated physical and full-output obligations remain open.

Merge Danger

Door: two-way.

Blast Radius: package.

Only the isolated research package is added. It registers two bounded verification commands and one immutable predecessor README input.