[roger-sato]

Summary

The historical PR49 arithmetic checker tests supplier moments at bit.saving and complex.saving without binding them to assembly.parameters.a_bit and a_complex. This scoped audit reconstructs authenticated historical sources and demonstrates a concrete positive-domain input that prints the ordinary arithmetic PASS at 717/20000000, while its unchanged assembly consumes 717/10000000. A separate exact rational lower-bound computation proves that the same supplied complex profile has moment greater than 1 + 4/10^10 at the consumed saving.

The counterexample increases the rank-756 multiplicity by five and halves only complex.saving. Counts are arithmetic inputs, not claimed to be producer-realizable. The original certificate passes its original fixed receipt. The existing --check receipt already rejects mutated bytes, so this is not a CI bypass or a counterexample to the original witness. No selected result, production helper, frozen consumer, or source archive changes.

The new package includes an opt-in guard for the two rational equalities, a proof of the independent lower bound, and actual CLI controls. The guard accepts equivalent rational spellings and a consistently bound noncontracting profile; the latter is then rejected by the historical arithmetic checker. Binding success alone is not mathematical validation. Production adoption remains an explicitly open next question because existing historical packages bind the live helper bytes.

Task and overlap

• Base: 20ecf2891d80b5acf18d980b2164fb44ea7faa90; priority revision 6.
• Task: portable-replay, scope refined from its proof-relevant field-comparison method to supplier/assembly saving comparison. This is a verifier side result, not an environment repair or new construction.
• The seven source rows are historical Git provenance, reconstructed from the immutable base, with VERIFY.json inputs: []. Future changes to the current helper do not have to preserve historical acceptance of the counterexample.
• Nearest related work: PR49 is the original candidate; PR1329 addresses retained PR589 supplier identity and COPY deficit, not these PR49 saving equalities. Current handoff/open+closed PR scans found no equivalent audit; this is not a universal novelty claim.

Test plan

Python 3.12.14 on macOS arm64, standard library only:

• python3.12 -B scripts/research_package.py --package research/followup-supplier-binding-audit --check-only
• python3.12 -B scripts/research_package.py --package research/followup-supplier-binding-audit
• Registered replay runs the complete verifier normally and with -O; both print PASS_FOLLOWUP_SUPPLIER_BINDING_AUDIT_ONLY.
• Ten actual child CLI invocations per mode cover original fixed-receipt success; standalone mutant acceptance; fixed-receipt mutant rejection; bit and complex mismatch rejection by the optional guard; equivalent-fraction success; and consistent noncontracting rejection by the original arithmetic checker.
• Independent exact atanh-series/dyadic-reduction/positive exponential-polynomial lower bound exceeds 1 + 4/10^10; no historical numerical routine is imported for this proof.
• python3.12 -B scripts/check_research_commit.py --package research/followup-supplier-binding-audit --ref HEAD --check-source-history passed for all seven committed files in a fresh full-history filtered clone of canonical main with the publication commit fetched locally.

No finite-count producers, all-package historical suites, Lean, or selected cold replay were run. Source history and arithmetic-input scope are explicit in the README. The package's TASK.json and README describe the smallest production-integration follow-up and its frozen-consumer constraint.

Credit

Rohan Arun's PR49 candidate at f95d2910e027495983b53cae1693cf535abf2569, building on PR48, retains its attribution and original fixed receipt. The historical independent arithmetic checker and PR39 enclosure dependency retain Douglas Colkitt's attribution. Audit and opt-in guard by roger-sato with substantial OpenAI Codex assistance in diagnosis, implementation, exact arithmetic, review, and documentation. Apache-2.0.