[petalas]

Summary

Scoped proof and arithmetic construction, with exact finite corroboration. After one base-p digit split, compute both remainders modulo p+1 and p+2 with two shared correction comparisons on the sharp prefix 0<=x<p(p+2), p>=2.

d=r-a, e=d-a
d<0: e<-(p+2) selects (1,2) or (1,1)
d>=0: e<0 selects (0,1) or (0,0)

Separate constant-correction trees need three comparisons in the worst case; the joint tree needs two. Four explicit correction pairs prove optimality. At x=p(p+2), a fifth pair proves that no two-comparison tree in this model covers a larger initial interval.

This contribution was produced by Nick Petalas. Classical radix division, quotient correction, CRT and binary-tree leaf counting retain their ordinary credit. Independent human and formal proof-kernel review are unclaimed.

Evidence

• Before: independent correction trees attain the proved worst-case minimum of three comparisons.
• After: the complete four-leaf tree uses exactly two, with two subtractions and at most two additions after prepared constants and the digit split.
• Warning-strict normal and optimized checks pass: 93,597 complete inputs for p=2..64, 315 sharpness witnesses, 176 large-radix boundary cases and eighteen rejection controls.
• Committed-byte, source-history and executable-mode checks pass at 645c3492273627df4daaa926d9df9cc686dccc86.
• CPython 3.12.15, macOS arm64. Local timeout-budget observations: 0.06 seconds normal, 0.07 seconds optimized. These are not runtime-saving measurements.

Exact reproduction from the repository root:

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

Replace the interpreter path elsewhere. Direct checks use only the standard library and write no files.

Limitations and unrun obligations

The lower bound covers binary trees with constant correction pairs at leaves. It does not cover every arithmetic, lookup or bitwise remainder algorithm. Wrapper validation is outside the trusted-core count; preparation and splitting are separately charged in the README.

The proof covers all integer p>=2; implementation radix length is capped at 4096 bits. The prefix omits the top p+2 full-CRT representatives. No selected caller or complete encoded movement/control-history/restoration bill is supplied. No physical CRT implementation, supplier admission, new kappa or selected-frontier change is claimed. All five framework assumptions remain. Lean, Docker and the selected cold replay were not run.

Open next questions

1. Bind the core to an encoded recovery caller with these moduli and a proved prefix bound; price preparation, splitting, validation, arithmetic, movement, control history and restoration.
2. Classify correction pairs and construct an optimal tree on the complete CRT interval, starting with the omitted top p+2 inputs.

Related open work

Completion refresh inspected the fifteen other open account PRs created since the advance CLAIM. None studies this modulus pair or correction-comparison quantity. No conflicting same-instance number was found, and no additional computation was run to check another contribution.

• PR Audit conditional CRT last-K two-slice streaming tariff #4187 studies a conditional CRT last-K payload-streaming tariff; it supplies no adjacent-modulus correction tree. No numerical result is compared.
• PR Eliminate 11,470 Gaussian setup exponential calls (no κ) #6413 reduces Gaussian coefficient-setup work in a different arithmetic stage; it supplies no quotient-correction tree. No numerical result is compared.

CI notes

Both hosted checks passed at exact head 645c3492273627df4daaa926d9df9cc686dccc86 in run 41528748136: plan and replay (research/joint-adjacent-remainders). The completed checks were read once; the run metadata also confirms successful completion at that head.

Hosted replay certifies the registered normal and optimized checks at this commit. The local exhaustive/boundary/rejection checks and committed-byte/source-history/mode validation listed above also passed. CI is not an independent human review or proof-kernel verification of the universal theorem. No CI failure remains; all stated physical-caller and framework limitations remain.

Merge Danger

Door: two-way. Six new files in one opt-in research package.

Blast Radius: isolated. Shared code, frozen evidence and the selected frontier remain unchanged.