Prove exact lattice closure for rational rounded shears (no κ)

research/rounded-shear-lattice-closure/PROOF.md

@@ -0,0 +1,154 @@
+# Exact stagewise lattice closure for rounded shears
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped mathematical proof. The executable supplies finite
+corroboration, not a proof-kernel formalization.
+
+## Model and statement
+
+Write R(t)=floor(t+1/2), including for negative t. For rational a,b define
+
+    U_a(x,y) = (x, y + R(a x)),
+    V_b(x,y) = (x + R(b y), y).
+
+Both are bijections of Z^2. Their inverses subtract the same rounded
+increment. In particular U_a^-1 need not be U_(-a) at ties.
+
+Let L be any full-rank additive sublattice of Z^2. Its unique column
+Hermite form can be written
+
+    L = { (h n, r n + k m) : n,m in Z },
+    h,k >= 1, 0 <= r < k.
+
+Set g=gcd(r,k) and ell=hk/g. Then the exact closure conditions are
+
+    U_a(L)=L  iff  k=1 or a h / k is an integer,
+    V_b(L)=L  iff  ell=1 or b g / ell is an integer.       (1)
+
+Consequently, if a and b are both nonintegral, a proper full-rank L
+preserved by both maps exists if and only if ab is an integer. If such
+an L exists, both rounded maps equal their ideal linear shears on L.
+
+For sufficiency, if a=p/q in lowest terms, q>=2, the explicit lattice
+
+    L = q Z x |p| Z                                      (2)
+
+works whenever ab is an integer. Its index q|p| is greater than one.
+These statements include negative slopes and arbitrary lattice index.
+
+## Scalar lemma
+
+For rational c and integer d>=2,
+
+    R(c n) belongs to d Z for every n in Z
+        iff c belongs to d Z.                           (3)
+
+The reverse implication follows because rounding fixes integers.
+For necessity, integral c gives R(c)=c, so d divides c.
+
+Otherwise write c=t+s/q with t an integer, 1<=s<q, q>=2.
+For n=0,...,q-1 the successive differences
+
+    delta_n = R(c(n+1)) - R(c n)
+
+are each t or t+1. This follows by writing R(cn) as a floor: adding
+t+s/q changes a floor by t or t+1, including at ties. Their sum is
+R(cq)-R(0)=tq+s. Therefore exactly s of the differences equal t+1
+and q-s equal t. If all R(cn) belonged to dZ, all differences would
+belong to dZ. The consecutive integers t and t+1 cannot both be
+divisible by d>=2. This proves (3), using only n=0,...,q in the
+nonintegral case. The d=1 exception is essential.
+
+## Proof of the closure criterion
+
+The x-coordinate projection of L is hZ. Its vertical fiber is
+
+    L intersect ({0} x Z) = {0} x kZ.
+
+At a point with x=hn, U_a changes only y by R(ahn). Thus U_a(L)
+is contained in L exactly when all these increments belong to kZ.
+For k=1 this is automatic; for k>=2 apply (3) with c=ah and d=k.
+The same increment can be subtracted, so containment also implies
+equality and closure under the literal inverse.
+
+The y-coordinate projection is gZ because rZ+kZ=gZ. A horizontal
+vector (x,0) belongs to L precisely when x=hn and k divides rn.
+The least positive such x is ell=hk/g. Therefore the horizontal
+fiber is ellZ x {0}. Apply the same argument to V_b, now with
+c=bg and d=ell. This proves both equivalences in (1), without
+assuming that L is rectangular or that the shears are linear.
+
+## Proof of the integer-product equivalence
+
+Suppose L is proper and both slopes are nonintegral.
+If k=1, then r=0, g=1, ell=h and properness gives h>1.
+Closure under V_b would force b/h to be an integer, contradicting
+nonintegrality of b. Hence k>1.
+
+If ell=1, the positive integers h and k/g must both equal one.
+Then g=k, r=0, h=1 and properness gives k>1. Closure under U_a
+would force a/k to be an integer, another contradiction. Thus ell>1.
+
+By (1), there are integers m,n with
+
+    ah = km,  bg = ell n.
+
+Put t=k/g, a positive integer. Since ell=ht, multiplication gives
+
+    ab = (km/h)(ell n/g) = t^2 mn,                      (4)
+
+an integer. Moreover every source x lies in hZ and every source y
+lies in gZ; ah and bg are integers. No rounding occurs on L.
+
+Conversely let ab=N be an integer and a=p/q be reduced, q>=2.
+Since a is nonintegral, p is nonzero. For x=qz and y=|p|w,
+
+    ax = pz belongs to |p|Z,
+    by = sign(p) N q w belongs to qZ.
+
+Both increments are already integers in the required fibers of (2).
+Both shears and their literal inverses preserve this proper lattice.
+This proves sufficiency and the complete equivalence.
+
+## A precision-domain obstruction
+
+For a=1/2 and b=-4/5, ab=-2/5 is not integral. Therefore Z^2 is
+the only full-rank additive sublattice of Z^2 invariant under both
+rounded directions. These are the two slopes in the familiar lifting
+factorization of the rotation with cosine 3/5 and sine 4/5:
+
+    [[1,1/2],[0,1]] [[1,0],[-4/5,1]] [[1,1/2],[0,1]]
+        = [[3/5,4/5],[-4/5,3/5]].
+
+Requiring one proper additive entrance lattice to survive every
+rounded substep cannot support a correlated precision policy for
+this lifting pair. This is a scoped closure obstruction. It says
+nothing about changing the domain between stages, affine cosets,
+nonadditive domains, a whole-word exactness domain, or periodic
+translation-equivariance lattices. It does not assert any violation
+of a selected caller's contract.
+
+## Why the finite oracle is complete for each tested lattice
+
+Fix one slope a=p/q and lattice index D=hk. D Z^2 is contained in L.
+Take M=qD. Translating an input coordinate by M changes a rounded
+increment by pD, because R(t+j)=R(t)+j for integer j. Both the input
+translation and the resulting output changes lie in D Z^2, hence L.
+Membership after either shear consequently depends only on the input
+modulo M Z^2. This is a periodicity argument, not an assumption that
+the rounded shear preserves M Z^2.
+
+All representatives in L modulo M Z^2 are enumerated exactly once by
+
+    0 <= u < M/h, 0 <= v < M/k,
+    x=hu, y=(ru+kv) mod M.
+
+There are (M/h)(M/k)=q^2D representatives. The oracle literally
+applies both rounded updates to each one and tests HNF membership.
+It uses neither projected spacings nor (1) to decide closure. Thus
+each finite one-shear verdict is exhaustive for that entire tested
+lattice, even though the lattice has infinitely many points.
+
+The universal claims above rest on the written scalar and fiber
+proofs. The finite range of lattice parameters and slopes is not
+used to extrapolate a universal result.

research/rounded-shear-lattice-closure/README.md

@@ -0,0 +1,140 @@
+# Exact invariant lattices for rational rounded shears
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped mathematical proof with exact finite corroboration.
+No new kappa or supplier admission is claimed.
+
+For half-up nearest rounding R(t)=floor(t+1/2), consider
+
+    U_a(x,y) = (x, y + R(a x)),
+    V_b(x,y) = (x + R(b y), y).
+
+If both rational slopes a,b are nonintegral, a proper full-rank additive
+sublattice of Z^2 preserved by both maps exists **if and only if ab is an
+integer**. Both updates are then exact linear shears on that lattice.
+When a=p/q is reduced, the explicit lattice qZ x |p|Z attains the positive
+direction. This is an all-rational theorem, not a bounded search conclusion.
+
+The more general exact criterion covers every rational slope and every
+full-rank lattice, including skew lattices. In Hermite coordinates
+
+    L = { (hn, rn+km) : n,m in Z }, h,k>=1, 0<=r<k,
+    g = gcd(r,k), ell = hk/g,
+
+    U_a(L)=L iff k=1 or ah/k is an integer,
+    V_b(L)=L iff ell=1 or bg/ell is an integer.
+
+[PROOF.md](PROOF.md) proves the criterion by identifying the source
+projections and the target fibers. The scalar step is that, for d>=2,
+R(cn) can belong to dZ for every integer n only when c belongs to dZ.
+No predecessor numerical result is needed in the proof.
+
+For the lifting slopes a=1/2,b=-4/5 of the rational rotation with
+cosine 3/5 and sine 4/5, the product is -2/5. Thus no proper additive
+integer lattice survives both directions at every substep. A correlated
+precision policy using one fixed proper lattice cannot pass that closure
+gate. This does not exclude an interface whose domain changes between stages.
+
+## Evidence and reproduction
+
+From the repository root, using standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rounded-shear-lattice-closure/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/rounded-shear-lattice-closure/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-shear-lattice-closure
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-shear-lattice-closure --check-source-history
+```
+
+Substitute another CPython 3.12 executable on another machine. Run the final
+command after committing. The direct checker prints
+`PASS_ROUNDED_SHEAR_LATTICE_CLOSURE` in a generated JSON stdout receipt
+bound to the six package file hashes. It writes no files. The registered
+runner executes both modes and reports `PASS_REGISTERED_RESEARCH_PACKAGE`.
+
+The checker covers all 75 Hermite lattices with 1<=h,k<=5 and 0<=r<k,
+and all 39 distinct reduced slopes p/q with -5<=p<=5, 1<=q<=5.
+It compares 5,850 one-shear closure verdicts with 664,950 literal point
+updates over complete residue periods. The periodic reduction has its own
+proof and does not use the closure criterion to decide the oracle verdict.
+
+It also checks all 784 ordered pairs of nonintegral slopes in that set.
+The 56 integer-product pairs have literal constructive replays, comprising
+40,800 additional point updates; the other 728 pairs have no proper
+invariant lattice in the enumerated family. That bounded absence corroborates
+the universal written theorem and does not replace it. Ten semantic controls
+cover unit fibers, integral-slope exceptions, skew lattices, signed ties,
+the positive construction, single-direction closure and completed-word
+closure. Ten invalid-input cases reject explicitly, including under `-O`.
+
+## Source, credit and scope
+
+Credit woklerx's [PR1848](https://github.com/CrocSwap/integer-mult-bounds/pull/1848),
+head `d975e19e7e931fc2b45792a4f7140ac13759a7da`, for its explicit
+intervening-update lattice-closure question and affine-lattice precision
+interface. Its cancellation theorem is a cited predecessor, not an audit
+target. The new step is the classification for separately rounded planar
+shears and its integer-product obstruction. Hermite normal form, floor
+increments and rational lifting factorizations are classical; no general
+literature-priority claim is intended. Gareth Davidson, Chafik Boukhalfa
+and Ali Romman retain the mixed-precision and dirty-restoration lineage
+credited by that predecessor.
+
+Adam Gall's [PR1908](https://github.com/CrocSwap/integer-mult-bounds/pull/1908)
+already supplies an actual rounded-leaf counterexample to transferring
+ideal lattice closure. It is separate context, with no replay here. The
+present result gives a quantified criterion for a different explicit
+nonlinear update model. Linear Gaussian-module classifications and
+equivariant frame rounders are different contracts as well.
+
+[SOURCES.json](SOURCES.json) pins the source question, original catalogue
+and selected record as historical provenance. No predecessor executable,
+pending Git object, network service or external library is a runtime input.
+[TASK.json](TASK.json) records the change from `formal-interface-lemma`
+to this written precision-interface result. No proof-kernel formalization
+or binding to an actual selected caller is supplied.
+
+The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362381)
+and overlap check used canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8,
+selected PR6030. The cached scan covered 387 open PRs and 6,328 Discussion
+records with complete pagination. Its local scan covered 108 of 8,917
+note paths; all-main README searches and distinctive merged-PR searches
+supplemented it. Arbitrary code diffs and unpublished work remain outside
+that coverage. No novelty certificate is claimed.
+
+## Limitations and verification design
+
+The theorem requires a full-rank additive sublattice of the integer plane,
+the same lattice at both substeps, rational fixed slopes, half-up rounding,
+and separately rounded increments followed by exact integer updates.
+Both nonintegrality hypotheses are essential for the product equivalence.
+The closure criterion itself also handles integral slopes. Affine cosets,
+lower-rank domains, changing stage domains, nonlinear entrance sets and
+whole-word-only closure are excluded.
+
+Actual caller reachability, physical native realization, restoration and
+precision/movement/storage prices, the complete paid/productive invoice,
+supplier admission and all five selected framework assumptions remain
+open. No predecessor scientific replay, selected cold replay, Lean or
+Docker run was performed. Independent human and formal proof-kernel
+review are unclaimed.
+
+The verifier has no recursion, subprocesses, external imports or writes.
+Its fixed census bounds and validated Hermite/slope limits bound every
+enumeration. Functions remain below 60 lines. Mathematical checks use
+explicit exceptions and remain active under optimized Python. Python's
+managed allocation and dataclass-generated methods are documented Power
+of Ten deviations; the finite parameter sets bound live storage and
+dispatch, with no fixed-memory or static-analyzer claim. Warning-strict
+normal and optimized execution provide interpreter diagnostics.
+
+## Open next questions
+
+Can changing lattice domains support one actual rounded lifting caller?
+First fix its literal update sequence and derive the exact image domain
+at each substep. This matters because the present obstruction requires
+one common invariant lattice. Actual source reachability, later inverse
+compatibility and the complete precision/movement/storage bill remain
+blockers. The structured question is retained in TASK.json. No further
+construction search is part of this contribution.

research/rounded-shear-lattice-closure/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/affine-lattice-inverse-precision/README.md",
+      "usage": "provenance",
+      "git_blob": "01d4a83e39092d609b16f81772b8bd057522abd7",
+      "sha256": "e28d3637dcb322c12205f5754656393f7d066f715a9653a794b879f2e8707373"
+    }
+  ]
+}