Prove modular normalization metrics and a paid query completion (no new κ)

research/modular-normalization-boundary/PROOF.md

@@ -0,0 +1,205 @@
+# Exact metric constants and a paid modular query calibration
+
+This is a scoped written proof. Exact finite checks support it. They do not
+replace its quantifiers or establish a multiplication theorem.
+
+## 1. Three domains give two different optimal constants
+
+Let N=2^b, b>=1, and let p be odd. Put a=p^(-1) mod N, with 1<=a<N,
+and m=min(a,N-a). On C_N=Z/NZ use the cycle distance
+
+    d_N(x,y)=min((x-y) mod N,(y-x) mod N).
+
+The map A(x)=ax mod N has exact Lipschitz constant m from C_N to C_N.
+Each adjacent input pair has output distance m. Every shortest input path
+has d_N(x,y) edges. The triangle inequality gives the upper bound
+m*d_N(x,y); adjacent inputs give equality.
+
+For an integer-line lift F:Z->Z with F(t)=at mod N, use the usual absolute
+distance on both copies of Z. Every adjacent difference F(t+1)-F(t) is
+congruent to a. Its absolute value is at least m. Thus every such lift has
+Lipschitz constant at least m. Choose the shortest signed representative
+s of a and set F(t)=st. This attains m on the entire line. The lift is
+not periodic.
+
+For a periodic integer lift G:C_N->Z with G(x)=ax mod N, use d_N on the
+domain and absolute distance on the target. Its exact minimum Lipschitz
+constant is N-m. To prove the lower bound, orient all N cycle edges and
+put Delta_x=G(x+1)-G(x), with x+1 interpreted modulo N. Each Delta_x is
+congruent to a, and their sum is zero. Since 0<a<N, no Delta_x is zero.
+There must be positive and negative increments. A positive increment is
+at least a; a negative increment has absolute value at least N-a.
+Therefore some edge has absolute increment at least max(a,N-a)=N-m.
+The canonical representative G(x)=ax mod N in [0,N-1] has increments
+a or a-N, and attains this lower bound. Edge bounds extend to all pairs
+by a shortest cycle path.
+
+The lift class must be named. For N=8 and p=3, m=3. The integer-line lift
+F(t)=3t attains 3, but its values at representatives 7 and 0 differ by 21
+across a cycle edge. A periodic lift can do better than that particular
+choice, but its exact minimum is 5, not 3.
+
+## 2. Fixed odd normalization and numerical ambiguity
+
+Assume 1<p<N. The shortest signed representative s obeys ps=1+kN.
+Here k is nonzero: p>1 cannot divide 1 in Z. Thus
+
+    p*m = |ps| >= N-1,           m >= (N-1)/p.
+
+For p=3 the exact value is
+
+    m=(2^b-(-1)^b)/3.
+
+If b is even, N=1 mod 3 and s=(1-N)/3. If b is odd, N=2 mod 3 and
+s=(1+N)/3. These are the shortest representatives.
+
+Rescale the residue cycle to circumference one, with spacing 1/N.
+Its inverse-normalization Lipschitz constant remains m. Inputs 0 and
+1/N can produce the same uncertain real observation 1/(2N) when the
+allowed input error is 1/(2N). Their normalized outputs have circle
+distance m/N. Any common numerical output has error at least m/(2N)
+on one of the two inputs, by the triangle inequality.
+
+For fixed p this output ambiguity does not tend to zero: its lower bound
+is (N-1)/(2pN). This statement concerns an unrestricted numerical
+interface with that input uncertainty. Exact digital residues have no
+such uncertainty. A separated reachable set can also exclude the two
+inputs. This is not an extra-bit lower bound for an exact modular
+backend, and it does not refute modular borrowed-port echoes.
+
+## 3. The released three-coordinate cut
+
+The following coordinates are payload vectors of any common finite width d.
+Scalar operations act componentwise. Use the ordinary prefix
+
+    x += z
+    y -= z
+    z += x
+    z += x
+    z -= y.
+
+Its integer matrix is
+
+    B = [1  0  1]
+        [0  1 -1]
+        [2 -1  4],            det(B)=1.
+
+Let E be the first two coordinates. A supported column c=(u,v,0) has
+B*c supported on E exactly when 2u-v=0. Its full column module is
+generated by c0=(1,2,0). A supported row r=(u,v,0) has r*B supported
+on E exactly when u-v=0. Its full row module is generated by
+r0=(1,1,0). Both generators are fixed by B, so using B^-1 gives the
+same modules. Their pairing is r0*c0=3.
+
+Over Z[1/2], all eligible pairings are 3uv. None equals one, since 3
+is not a unit. Modulo 2^b, 3 is a unit and a=3^(-1) supplies a normalized
+pair. This is an algebraic change of boundary. It does not supply a
+cheap physical native operator.
+
+## 4. Literal completion, arbitrary dirt and inverse
+
+On E, four instructions implement S(x,y)=(x+y,2x-y):
+
+    y += x
+    x *= 3
+    x -= y
+    SWAP(x,y).
+
+The inverse is
+
+    SWAP(x,y)
+    x += y
+    x *= a
+    y -= x.
+
+Each instruction uses exact residues modulo N. Apply the prefix B,
+then S, then one supplied invertible linear query Q to the first payload,
+then S^-1 and the literal inverse of B. This is 5+4+1+4+5=19 instructions.
+
+Put delta=a*(Q-I)(x+y). The complete endpoint is
+
+    x' = x+delta,
+    y' = y+2*delta,
+    z' = z.
+
+Indeed S^-1= a*S and the changed part is
+a*c0*(Q-I)*r0. Because B*c0=c0 and r0*B=r0, conjugation by B leaves
+this changed part unchanged. All formulas hold for arbitrary correlated
+payloads and arbitrary dirty z. The reverse word, with inverse scalar
+coefficients and Q^-1, restores every input exactly.
+
+For d=2 and Q the payload swap, start at x=z=0 and y=(1,0).
+The second entry of x' is a. Thus the modular-inverse expansion survives
+the complete query endpoint. It is not removed by the dirty-coordinate
+restoration. This is a lower-bound witness for the full endpoint, not a
+claim that its exact global operator norm is m.
+
+## 5. Correct ordinary alphabet and complete direct costs
+
+A SWAP of two scalar registers cannot equal any product of signed elementary
+ADDs modulo N>=4: each ADD has determinant one, while that SWAP has
+determinant minus one. The vector instructions here repeat the same scalar
+word on each payload entry. This argument does not exclude other words
+that mix payload entries or swap an even number of scalar pairs together.
+The three familiar ADDs produce a signed swap:
+
+    x += y
+    y -= x
+    x += y                 # endpoint (old_y, -old_x).
+
+One additional paid negation of y gives the actual swap. This four-step
+identity holds over every commutative ring. Replacing both SWAPs gives
+25 instructions, not the incorrect three-ADD price.
+
+| Program | ADD/SUB | SCALE | SWAP | NEGATE | Supplied query |
+|---|---:|---:|---:|---:|---:|
+| Literal | 14 | 2 | 2 | 0 | 1 |
+| Expanded | 20 | 2 | 0 | 2 | 1 |
+
+These are vector instructions. For payload width d the literal word uses
+14d scalar additions/subtractions, 2d scalar multiplications, 16d explicit
+reductions, and 6d assignments for the two swaps. The expanded word uses
+20d additions/subtractions, 2d multiplications, 2d negations and 24d
+reductions. The query's own arithmetic, reductions, scratch and inverse
+are separate paid terms; the verifier's dense matrix evaluator is an oracle
+implementation, not a free physical query.
+
+Stored values have b bits. ADD needs b+1 unsigned bits; SUB needs b+1
+signed bits. NEGATE also fits in b+1 signed bits.
+The two fixed-coefficient products fit in 2b unsigned bits. With
+schoolbook multiplication, direct scalar work outside the query is
+O(d*b^2) bit work. Add inverse-coefficient preparation, query execution,
+conversion, access, layout, recovery and any physical routing costs.
+The reference uses O(db) payload/copy bits plus query storage, loop
+indices and O(b) scalar scratch. Its Python allocations are not a
+fixed-tape implementation or a tight workspace claim.
+
+No supplied coefficient, modular reduction, input/output conversion or
+query is claimed free. The 19/25 counts are constructive upper bounds,
+not shortest-word optima. No favorable complete recursive invoice is
+provided. Native realization, numerical conversion, exact recovery and
+the full supplier boundary remain open.
+
+## 6. Attribution and limits
+
+Nick Petalas's [released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363231)
+supplies the quotient/line candidate, pairing-three prefix and proposed
+19-instruction calibration. It also reports the three-ADD SWAP cost error.
+This continuation independently reconstructs and checks the word, repairs
+the paid expansion, distinguishes periodic lifts and supplies a public proof
+and registered finite evidence. It does not claim priority for the released
+ideas or general modular metric arguments.
+
+Gareth Davidson / @bitplane's [PR #1159](https://github.com/CrocSwap/integer-mult-bounds/pull/1159)
+supplies the exact quotient-valued borrowed-port context. Its own
+[scope](https://github.com/CrocSwap/integer-mult-bounds/blob/7c49fe32c55de02c2c873655c804b16e4c3fef0a/research/modular-port-borrowing/README.md)
+excludes rounded and general dyadic leaves. We do not audit that backend
+or transfer this numerical obstruction to it. Retain shhxera, androolloyd,
+Sagar Thakrar, Chafik Boukhalfa and the classical register lineage credited
+in that unchanged source.
+
+All selected assumptions and the selected frontier remain unchanged.
+Independent human review, proof-kernel formalization, production native
+execution and complete multiplication admission are unrun.
+Prepared by Ali Romman with substantial OpenAI Codex assistance.
+New work is Apache-2.0.

research/modular-normalization-boundary/README.md

@@ -0,0 +1,86 @@
+# Modular inverse normalization: exact metric boundary and paid query word
+
+**Scoped proof and scalar construction; no new kappa.** This completes
+[Nick Petalas's released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363231).
+It distinguishes three lift domains and corrects the stated SWAP cost error.
+The [proof](PROOF.md) gives all quantifiers, the full word, prices and credit.
+The [receipt](RESULT.json) records exact finite evidence.
+
+Let N=2^b, a=p^(-1) mod N for odd p, and m=min(a,N-a).
+
+| Boundary | Exact optimal Lipschitz constant |
+|---|---:|
+| Residue cycle to residue cycle | m |
+| Integer-line lift, ordinary distance | m |
+| Periodic integer lift from the residue cycle | N-m |
+
+For fixed 1<p<N, m>=(N-1)/p. For p=3 the exact value is
+`(2^b-(-1)^b)/3`. Thus an unrestricted numerical conversion can have
+nonvanishing output ambiguity even when its input error is half a grid unit.
+Exact digital residue arithmetic and restricted reachable domains are outside
+this obstruction. The periodic lift distinction is necessary: at N=8,p=3,
+the first two constants are 3 and the third is 5.
+
+The handoff's pairing-three cut has a literal 19-instruction completion
+with one supplied invertible payload query. It restores the outside dirty
+coordinate exactly. A payload-swap query retains the inverse-normalization
+expansion at the full endpoint. Two separately paid SWAPs are present.
+Replacing each by three ADDs and one NEGATE gives a verified 25-instruction
+word. Three ADDs alone give a signed swap and cannot implement a SWAP
+modulo N>=4. Both words retain all scaling and reduction costs.
+
+This is an indexed scalar calibration. The query, coefficient preparation,
+conversion, physical access/routing, recovery and compiler costs are separate
+paid obligations. No favorable complete recursive bill, native Gaussian
+implementation, selected assumption discharge or frontier change is claimed.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+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
+```
+
+Expected markers are `PASS_MODULAR_NORMALIZATION_BOUNDARY`,
+`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`.
+The registered runner checks both normal and optimized execution.
+The default verifier compares the stored receipt without changing it.
+`--output NEW_FILE` writes a separate receipt and refuses to overwrite a file.
+
+Finite evidence covers 63 metric contexts and all 73,533 unordered pairs,
+8,805 independently enumerated 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 exhaustive binary dirty cases
+and 30 wider cases through 257 bits. Every one of the 19 and 25 instruction
+omissions is detected at modulus 32. Additional controls cover the signed
+swap, lift-domain confusion, full-endpoint amplification, numerical ambiguity,
+nonunit inversion and confusion with real division.
+
+No predecessor scientific suite, selected cold replay, Lean, Docker,
+independent human review or proof-kernel verification is claimed. The
+finite enumeration supports the written all-size proof; it does not replace it.
+Sources in [SOURCES.json](SOURCES.json) are provenance, not imported code.
+The verifier is standalone and has no runtime source dependencies.
+
+## Open next questions
+
+Can one actual native producer stay in exact residue arithmetic with paid
+conversion and exact recovery, or prove a restricted reachable domain?
+First export one complete producer/query/consumer boundary and its full
+invoice. The present obstruction does not decide those alternatives.
+
+## Credit
+
+Nick Petalas supplied the released metric candidate, pairing-three prefix,
+19-instruction completion proposal and disclosed cost error. This work
+reconstructs the completion, repairs and tests the paid expansion, distinguishes
+periodic lifts, and publishes the exact proof and executable evidence.
+Gareth Davidson / @bitplane supplied the exact quotient backend and its scope
+in [PR #1159](https://github.com/CrocSwap/integer-mult-bounds/pull/1159).
+Its unchanged source retains shhxera, androolloyd, Sagar Thakrar, Chafik
+Boukhalfa and the classical register lineage. General congruences, cycle
+metrics and two-point ambiguity arguments are classical; no global literature
+priority is claimed. Prepared by Ali Romman with substantial OpenAI Codex
+assistance. New work is Apache-2.0.