diff --git a/research/rounded-shear-lattice-closure/PROOF.md b/research/rounded-shear-lattice-closure/PROOF.md new file mode 100644 index 0000000000..af0a8eea3a --- /dev/null +++ b/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=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. diff --git a/research/rounded-shear-lattice-closure/README.md b/research/rounded-shear-lattice-closure/README.md new file mode 100644 index 0000000000..5d1c98c8cf --- /dev/null +++ b/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=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 None: + if not condition: + raise ValueError(message) + + +@dataclass(frozen=True) +class Lattice: + """Columns (h,r), (0,k), with bounded canonical Hermite parameters.""" + + h: int + r: int + k: int + + def __post_init__(self) -> None: + require(all(type(v) is int for v in (self.h, self.r, self.k)), "integer HNF") + require(1 <= self.h <= 16 and 1 <= self.k <= 16, "HNF size limit") + require(0 <= self.r < self.k, "canonical HNF residue") + + def contains(self, x: int, y: int) -> bool: + return x % self.h == 0 and (y - self.r * (x // self.h)) % self.k == 0 + + +def slope_check(a: Fraction) -> None: + require(type(a) is Fraction, "exact rational slope required") + require(a.denominator <= 12 and abs(a.numerator) <= 64, "slope size limit") + + +def nearest(t: Fraction) -> int: + """Euclidean quotient/remainder implementation, including signed ties.""" + whole, residue = divmod(t.numerator, t.denominator) + return whole + int(2 * residue >= t.denominator) + + +def criterion(lattice: Lattice, a: Fraction) -> tuple[bool, bool]: + slope_check(a) + g = gcd(lattice.r, lattice.k) + horizontal = lattice.h * lattice.k // g + up = lattice.k == 1 or (a * lattice.h / lattice.k).denominator == 1 + right = horizontal == 1 or (a * g / horizontal).denominator == 1 + return up, right + + +def period_oracle(lattice: Lattice, a: Fraction) -> tuple[tuple[bool, bool], int]: + """Apply literal rounded updates to every lattice point modulo q*index. + + Neither gcd, the projected source spacing, nor the closure criterion is + used here. The finite reduction is justified separately in PROOF.md. + """ + slope_check(a) + period = a.denominator * lattice.h * lattice.k + up, right, comparisons = True, True, 0 + for u in range(period // lattice.h): + for v in range(period // lattice.k): + x = lattice.h * u + y = (lattice.r * u + lattice.k * v) % period + require(lattice.contains(x, y), "oracle representative outside lattice") + up = lattice.contains(x, y + nearest(a * x)) and up + right = lattice.contains(x + nearest(a * y), y) and right + comparisons += 2 + require(comparisons == 2 * a.denominator**2 * lattice.h * lattice.k, + "incomplete residue enumeration") + return (up, right), comparisons + + +def finite_census() -> tuple[dict[str, int], tuple[Lattice, ...], tuple[Fraction, ...]]: + lattices = tuple(Lattice(h, r, k) for h in range(1, 6) + for k in range(1, 6) for r in range(k)) + slopes = tuple(sorted({Fraction(p, q) for p in range(-5, 6) + for q in range(1, 6)})) + cases = comparisons = 0 + for lattice in lattices: + for a in slopes: + observed, work = period_oracle(lattice, a) + require(observed == criterion(lattice, a), + f"closure mismatch: {lattice}, {a}, {observed}") + cases += 2 + comparisons += work + return {"lattices": len(lattices), "slopes": len(slopes), + "one_shear_cases": cases, "point_updates": comparisons}, lattices, slopes + + +def existence_census(lattices: tuple[Lattice, ...], + slopes: tuple[Fraction, ...]) -> dict[str, int]: + nonintegral = tuple(a for a in slopes if a.denominator > 1) + pairs = positive = negative = construction_updates = 0 + for a in nonintegral: + for b in nonintegral: + predicted = (a * b).denominator == 1 + bounded_exists = any(l.h * l.k > 1 and criterion(l, a)[0] + and criterion(l, b)[1] for l in lattices) + require(predicted == bounded_exists, "bounded existence disagreement") + if predicted: + lattice = Lattice(a.denominator, 0, abs(a.numerator)) + up, work_up = period_oracle(lattice, a) + right, work_right = period_oracle(lattice, b) + require(up[0] and right[1], "constructive lattice failed") + require((a * lattice.h).denominator == 1 + and (b * lattice.k).denominator == 1, "rounding still active") + construction_updates += work_up + work_right + positive += 1 + else: + negative += 1 + pairs += 1 + return {"nonintegral_slope_pairs": pairs, "integer_products": positive, + "noninteger_products": negative, + "construction_point_updates": construction_updates} + + +def controls() -> int: + # Unit fibers permit fractional slopes on the unrestricted grid. + require(criterion(Lattice(1, 0, 1), Fraction(1, 3)) == (True, True), "unit fibers") + # Removing either nonintegrality hypothesis permits nonintegral products. + require(criterion(Lattice(1, 0, 2), Fraction(2))[0] + and criterion(Lattice(1, 0, 2), Fraction(1, 3))[1], "integral first slope") + require(criterion(Lattice(2, 0, 1), Fraction(1, 3))[0] + and criterion(Lattice(2, 0, 1), Fraction(2))[1], "integral second slope") + # Skew lattices have distinct projection and fiber spacings. + require(criterion(Lattice(1, 1, 2), Fraction(1)) == (False, False), "skew fibers") + require(criterion(Lattice(1, 1, 2), Fraction(2)) == (True, True), "skew positive") + require(period_oracle(Lattice(2, 0, 3), Fraction(3, 2))[0][0] + and period_oracle(Lattice(2, 0, 3), Fraction(2, 3))[0][1], "product positive") + # An inverse subtracts the same increment; half-up rounding is not odd. + require(nearest(Fraction(1, 2)) == 1 and nearest(Fraction(-1, 2)) == 0, "signed ties") + require(nearest(Fraction(-3, 2)) == -1 and nearest(Fraction(3, 2)) == 2, "shifted ties") + # Completed-word closure is weaker than closure at every stage. + lattice = Lattice(1, 0, 2) + x, y = 1, 0 + middle = y + nearest(Fraction(1, 2) * x) + require(not lattice.contains(x, middle) and lattice.contains(x, middle - 1), + "completed inverse pair does not require stage closure") + require(criterion(Lattice(2, 0, 1), Fraction(1, 2))[0] + and not criterion(Lattice(2, 0, 1), Fraction(-4, 5))[1], "single direction") + return 10 + + +def invalid_controls() -> int: + count = 0 + for args in ((0, 0, 1), (1, 0, 0), (1, -1, 2), (1, 2, 2), + (17, 0, 1), (1, 0, 17), (True, 0, 1)): + try: + Lattice(*args) + except ValueError: + count += 1 + else: + raise ValueError(f"invalid lattice accepted: {args}") + for a in (Fraction(1, 13), Fraction(65), 0.5): + try: + slope_check(a) + except ValueError: + count += 1 + else: + raise ValueError("invalid slope accepted") + return count + + +def receipt(counts: dict[str, int]) -> None: + package = Path(__file__).resolve().parent + hashes = {} + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + payload = (package / name).read_bytes() + require(len(payload) <= 262144, "package file size limit") + hashes[name] = sha256(payload).hexdigest() + print(json.dumps({"status": "PASS_ROUNDED_SHEAR_LATTICE_CLOSURE", + "counts": counts, "sha256": hashes}, sort_keys=True)) + + +def main() -> None: + counts, lattices, slopes = finite_census() + counts.update(existence_census(lattices, slopes)) + counts["semantic_controls"] = controls() + counts["invalid_input_rejections"] = invalid_controls() + receipt(counts) + + +if __name__ == "__main__": + main()