[aliromman]

This scoped proof and scalar construction completes Nick Petalas's released modular-normalization handoff. It gives exact metric constants for three explicitly different domains, reconstructs the complete dirty-state query calibration, and repairs the disclosed SWAP cost error. No new κ or selected-frontier change is claimed.

Read the proof and complete direct cost, exact receipt, verifier, and source manifest. The result is pinned to 3d9dab36c3cc58d3a160f06e5f24185bb7fa0d4a, based on canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a.

For N=2^b, odd p, a=p^(-1) mod N, and m=min(a,N-a), the exact constants are:

Domain and target	Optimal Lipschitz constant
Residue cycle to residue cycle	m
Integer-line lift with ordinary distance	m
Periodic integer lift from the residue cycle to integer values	N-m

At N=8,p=3, these are 3, 3 and 5. The periodic lift cannot use the signed affine line lift without paying for its closing edge. For fixed 1<p<N, m >= (N-1)/p; for p=3, m=(2^b-(-1)^b)/3. A half-grid numerical input uncertainty therefore permits nonvanishing output ambiguity. This does not apply to exact digital residue arithmetic or automatically to a restricted reachable domain.

The pairing-three cut has a literal 19-instruction completion: fourteen ADD/SUBs, two SCALEs, two SWAPs and one supplied invertible payload query. The outside dirty coordinate is restored exactly. A payload-swap query retains the inverse-normalization expansion at the full endpoint. Each scalar SWAP expands into three ADDs plus one paid NEGATE, giving a verified 25-instruction version. The determinant argument concerns scalar registers and this componentwise word; it does not exclude joint words that mix payload entries. Counts are constructive upper bounds, not optima. All modular reductions are charged. Query cost, coefficient preparation, conversion, physical access/routing and exact recovery remain separate paid obligations.

Validation on CPython 3.12.13, standard library:

python3.12 -B scripts/research_package.py --package research/modular-normalization-boundary
python3.12 -B scripts/check_research_commit.py --package research/modular-normalization-boundary --check-source-history

Normal and optimized registered runs pass. Each covers 63 metric contexts and 73,533 unordered pairs, 8,805 periodic lifts, 255 inverse-three precision formulas, all 1,638 invertible two-by-two query matrices modulo 2,4,8, 19,656 full basis forward/inverse checks, 768 binary dirty cases and 30 wider cases through 257 bits. All 44 instruction-omission controls reject. Other controls cover signed swaps, lift-domain confusion, full-endpoint expansion, numerical ambiguity, nonunit inversion and real-division confusion.

PASS_MODULAR_NORMALIZATION_BOUNDARY 63 metric contexts; 1638 complete invertible queries; 44 instruction controls
PASS_REGISTERED_RESEARCH_PACKAGE research/modular-normalization-boundary outcome=completed
PASS_RESEARCH_COMMIT_BYTES

Metadata, seven committed files, source ancestry and the official standalone export's integrity/input coverage pass. The mathematical proof supplies the all-size claims; finite checks support it. Hosted CI is pending at publication. No predecessor scientific replay, selected cold replay, Lean, Docker, independent human review or proof-kernel review ran.

Credit Nick Petalas for the released metric candidate, prefix, completion proposal and disclosed cost error. No priority is claimed for those ideas. Gareth Davidson / @bitplane supplied the exact quotient-valued backend context in PR #1159; its source scope explicitly separates rounded/general dyadic leaves. That source is provenance, not imported code. Its register and borrowing lineage remains credited. Congruences, cycle metrics and two-point ambiguity arguments are classical; global literature priority is unclaimed.

The next useful question is an actual native producer that stays in exact residues with paid conversion/recovery, or a proved restricted reachable domain. This package does not supply either, a favorable full supplier invoice or discharge of any selected framework assumption. Scoped coordination claim. Prepared by Ali Romman with substantial OpenAI Codex assistance. New work is Apache-2.0.