From 43f558c1b8fc14fb0ed33a4512fbc976beea6b0f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 09:18:03 +0100 Subject: [PATCH] feat(research): classify bounded equivariant grid rounders --- .../README.md | 204 ++++++++++++++ .../SOURCES.json | 30 ++ .../TASK.json | 80 ++++++ .../VALIDATION.md | 78 +++++ .../VERIFY.json | 36 +++ .../verify.py | 266 ++++++++++++++++++ 6 files changed, 694 insertions(+) create mode 100644 research/equivariant-grid-frame-classification/README.md create mode 100644 research/equivariant-grid-frame-classification/SOURCES.json create mode 100644 research/equivariant-grid-frame-classification/TASK.json create mode 100644 research/equivariant-grid-frame-classification/VALIDATION.md create mode 100644 research/equivariant-grid-frame-classification/VERIFY.json create mode 100644 research/equivariant-grid-frame-classification/verify.py diff --git a/research/equivariant-grid-frame-classification/README.md b/research/equivariant-grid-frame-classification/README.md new file mode 100644 index 0000000000..518d895629 --- /dev/null +++ b/research/equivariant-grid-frame-classification/README.md @@ -0,0 +1,204 @@ +# Exactly which integer frame groups admit bounded equivariant grid rounding + +This contribution is produced by Nick Petalas. Apache-2.0. + +**Scoped proof with finite corroboration; no new kappa.** Let `d >= 1`, +`m >= 2` be integers and `G <= GL_d(Z)` be any group. There is a function + + q : (1/m) Z^d -> Z^d + +with a finite uniform absolute-error bound and `q(gx)=g q(x)` for every +`g in G` and every input x **if and only if G is finite**. The function may +be coupled, nonlinear and discontinuous. The positive direction actually +constructs such a function on all of `R^d`, fixing every integer vector. + +[PR1631](https://github.com/CrocSwap/integer-mult-bounds/pull/1631), by +Sricharan Vagvala, proves the particular infinite-order shear obstruction. +The new result classifies the entire integer frame group and supplies a +compatible positive construction. It does not replay that predecessor's +finite-orbit optima or dirty echoes. In particular, checking that each chosen +generator has finite order is insufficient: two involutions can generate +an infinite group and hence admit no common rounder of this kind. + +## Necessity: d seed errors bound the entire group + +Assume `||q(x)-x||_infinity <= C < infinity`. Let `e_i` be the standard +coordinate vectors and put + + z_i = q(e_i/m) in Z^d, + E = [m z_1-e_1 | ... | m z_d-e_d] = m Z-I. + +The integer matrix E satisfies `E = -I mod m`, so + + det(E) = (-1)^d mod m. + +Consequently `det(E) != 0`, even when m is composite. For every `g in G`, +equivariance at these seed orbits gives + + g E_i = m (q(g e_i/m)-g e_i/m). + +Every entry of `g E` therefore has absolute value at most `m C`. Since E +is invertible, `g=(g E)E^-1`. In particular, + + max_ij |g_ij| <= m C ||E^-1||_1, + +where the matrix 1-norm is the maximum absolute column sum. A bounded set +of integer matrices is finite. More explicitly, with +`M=floor(m C ||E^-1||_1)`, it contains at most `(2M+1)^(d*d)` matrices. +Thus G is finite. + +This proof needs only bounded errors on the G-orbits of the d displayed +seeds. It does not assume a nearest-point rule, linearity, continuity, +translation-equivariance or an identity-on-grid condition. The refinement +condition is essential: on the unrefined domain `Z^d`, the identity function +has zero error and commutes with every integer frame group. + +## Sufficiency: a stabilizer-compatible construction + +Now assume G is finite. Define the G-invariant norm + + ||v||_G = max_(g in G) ||g v||_infinity. + +It dominates the infinity norm because G contains I. For each subgroup H, +let `V_H={v: h v=v for all h in H}`. These are rational linear equations, +so rational row reduction and clearing denominators gives integer vectors +`b_(H,1),...,b_(H,k)` that are a real basis of `V_H`. They need not be a +basis of the whole fixed integer lattice. Set + + R_H = (1/2) sum_i ||b_(H,i)||_G, + R = max_(H <= G) R_H. + +There are finitely many subgroups, so R is finite. Every `y in V_H` is +within G-norm `R_H` of an H-fixed integer vector: expand y in this basis +and round each real coefficient to an integer. The triangle inequality +proves the stated bound. An empty basis has `V_H={0}` and `R_H=0`. + +For arbitrary `x in R^d`, define q by the following finite procedure. + +1. Choose the lexicographically smallest orbit point `y=min_(g in G) gx`. + Take any t with `t x=y` and let `H={h in G: h y=y}`. +2. Among integer z fixed by H, minimize `||z-y||_G`; break remaining ties + lexicographically. A minimizer exists within radius `R_H`. There are + finitely many candidates there because the G-norm dominates the infinity + norm. It suffices to enumerate the integer box + `ceil(y_j-R_H) <= z_j <= floor(y_j+R_H)` and filter by fixedness and radius. +3. Return `q(x)=t^-1 z`. + +This is independent of the choice of t. If `t' x=y`, then `t' t^-1 in H` +fixes z, so `t'^-1 z=t^-1 z`. To prove equivariance, for any `a in G`, +the same canonical y and stabilizer H apply to ax, and `t a^-1` is a valid +transport. Hence `q(ax)=a t^-1 z=a q(x)`. + +Finally, integrality of `t^-1` gives `q(x) in Z^d`, and norm invariance gives + + ||q(x)-x||_infinity <= ||t^-1(z-y)||_G = ||z-y||_G <= R_H <= R. + +If x is integral, y itself is an H-fixed integer candidate of zero error; +the chosen z equals y, so `q(x)=x`. Restricting this construction to any +refined grid proves the positive direction of the theorem. + +This is a mathematical finite algorithm using exact comparisons and floor +operations. Its physical bit/tape cost, real-input representation and optimal +error radius are not established. + +## Why the compatibility conditions matter + +At `x=(1/2,-1/2)`, the frame `A=[[0,-1],[-1,0]]` fixes x. In the ordinary +infinity norm, the lexicographically first unrestricted nearest integer +point is `z=(0,-1)`. It is not fixed by A. Transporting it with either I +or A therefore gives different answers for the very same input. Restricting +to stabilizer-fixed integer points removes this ambiguity. + +Nor can one merely check generator orders. The integer reflections + + r = [[1,1],[0,-1]], s = [[1,0],[0,-1]] + +have `r^2=s^2=I`, but `rs=[[1,-1],[0,1]]` has infinite order. The necessity +theorem excludes a single bounded rounder commuting with both r and s. + +The construction does not promise translation-equivariance. Adding +`q(x+n)=q(x)+n` changes the problem even for the finite group `{I,-I}` in +dimension one: at `x=1/2`, translation and sign equivariance together would +give `q(1/2)-1=q(-1/2)=-q(1/2)`, impossible for an integer output. The +classification concerns precisely the hypotheses in the opening statement. + +## Evidence and reproduction + +The written argument is dimension-uniform. [verify.py](verify.py) supplies +finite corroboration using only exact integers and rational numbers. It +implements the positive construction for five explicit finite groups, +including a nonorthogonal conjugate of the order-eight dihedral group and +the three-dimensional permutation group. Every group is checked for closure, +identity, inverses and integral determinant of absolute value one. + +For each group it checks all numerator tuples in `{-2,-1,0,1,2}^d`, each +with denominator 1, 2, 3 and 4, and every group translate of each point. +It checks integer output, the written radius, identity on integer inputs, +transport independence and exact equivariance. The seed-matrix census checks +`m Z-I` for all two-dimensional Z with entries -2..2 and m=2..8, and all +three-dimensional Z with entries -1..1 and m=2..4. These are finite tests +of the proof's mechanisms, not a finite proof of the universal theorem. + +Controls distinguish the stabilizer tie, coordinatewise nearest-even failure +under a finite reflection, the unrefined-grid exception, shear error growth +and two finite-order generators whose product has infinite order. No +predecessor verifier or receipt is imported. + +From the repository root: + +```sh +PY=/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 +"$PY" -W error -B research/equivariant-grid-frame-classification/verify.py +"$PY" -W error -I -O -B research/equivariant-grid-frame-classification/verify.py +"$PY" -B scripts/research_package.py --package research/equivariant-grid-frame-classification +"$PY" -B scripts/check_research_commit.py --package research/equivariant-grid-frame-classification --check-source-history +``` + +Expected markers are `PASS_EQUIVARIANT_GRID_FRAME_CLASSIFICATION no_new_kappa` +and `PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed`. An equivalent +CPython 3.12 interpreter suffices. Default replay writes no package files. +Optional `--receipt /absolute/external/path.json` exclusively creates a +computed receipt with SHA256 hashes of every package file. + +[SOURCES.json](SOURCES.json) pins the unchanged predecessor prose, selected +record and original catalogue. The original `uniform-transfer-audit` card +asks about an actual #4100 caller. [TASK.json](TASK.json) explicitly changes +scope to this carried-frame side theorem; no #4100 obligation is discharged. +[VALIDATION.md](VALIDATION.md) records the executed checks and their limits. + +## Limitations + +The input domain is the whole refined grid, or at least the specified seed +orbits for necessity. An actual reader can avoid the obstruction by having a +smaller reachable domain. Stateful or frame-dependent rounding, nonuniform +error bounds, noninteger frames and changing output grids are outside the +theorem. The positive construction supplies no optimal radius or efficient +physical implementation. No actual supplier child, rounded dirty echo, +storage recurrence, analytic transfer, selected cold replay, formal proof +kernel or complete multiplication theorem is supplied. The selected frontier +is unchanged. + +## Open next questions + +1. What is the least possible uniform error radius for one nonorthogonal + finite frame group? The construction proves finiteness but need not be + optimal. Start with the displayed order-two reflection and classify its + stabilizer-fixed nearest lattice points. No such optimization is claimed. +2. Which actual carried reader has reachable outputs containing the d seed + orbits used here? This determines whether the obstruction applies at a + physical caller. Start with one concrete reader and its dirty-input image; + source-bound reachability and arithmetic prices remain missing. + +## Credit + +Sricharan Vagvala / PR1631 supplies the shear obstruction and its explicit +rounding-interface scope. Woklerx's [PR1892](https://github.com/CrocSwap/integer-mult-bounds/pull/1892) +and `shear-orbit-interval-audit` supply the +separate rational-window oracle and emphasize that per-orbit choices need +not assemble into one rounder. Sagar Thakrar / PR1537 supplies the exact +carried-reader construction; Ross Richardson / PR1287 and the retained +PR1227/889/1203 lineage supply output-frame and dirty-echo context. Their +exact arithmetic constructions are not alleged to be defective. The new +contribution is the finite-group equivalence, its d-seed argument and the +stabilizer-compatible positive construction. Independent human and formal +proof-kernel review are unclaimed. diff --git a/research/equivariant-grid-frame-classification/SOURCES.json b/research/equivariant-grid-frame-classification/SOURCES.json new file mode 100644 index 0000000000..8bf25fd638 --- /dev/null +++ b/research/equivariant-grid-frame-classification/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/shear-equivariant-rounding-seed70/README.md", + "usage": "input", + "git_blob": "60b74da73f08e7630c1028535ff27bdde5936e72", + "sha256": "2daf86bbc607fbf31fb5868e42698ba7fbdefca5e41744055af7d6757238be86" + }, + { + "path": "research/shear-orbit-interval-audit/README.md", + "usage": "input", + "git_blob": "3160d2d31b323f2c85d8beb532e5d4a462ca5720", + "sha256": "6ed6a51e4c72989242600e22a27b0c19cd7d153d4e3e8e8060fe33034e8e78d0" + } + ] +} diff --git a/research/equivariant-grid-frame-classification/TASK.json b/research/equivariant-grid-frame-classification/TASK.json new file mode 100644 index 0000000000..3dee44df5b --- /dev/null +++ b/research/equivariant-grid-frame-classification/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Classify G <= GL_d(Z) admitting a uniformly bounded exactly equivariant rounder from (1/m)Z^d to Z^d for every fixed integer m >= 2; construct the positive finite-group direction on R^d.", + "scope_change_reason": "The original card asks for a caller-bound audit of #4100. The donor requires an original result rather than re-verification. This changes to a side theorem classifying exact carried-frame rounding, extending the single-shear setting of PR1631 without auditing it.", + "bottleneck_link": "Side result for the precision/interface boundary: a fixed absolute-error rounded reader cannot commute with an infinite integer frame group on a full refined output grid. No actual selected reader is shown to meet that domain hypothesis.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved classification and finite corroboration; do not optimize its radius or attach a supplier.", + "outcome": "completed", + "evidence": "README.md contains the dimension-uniform necessity and constructive sufficiency proofs; verify.py checks five finite groups, the complete stated seed-matrix domains and five semantic controls. VALIDATION.md records local checks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the least uniform error radius for the displayed nonorthogonal order-two reflection?", + "why_it_matters": "The existence proof gives a finite bound but no optimal precision allowance.", + "first_step": "Classify stabilizers and fixed-lattice nearest points for [[1,1],[0,-1]].", + "blocked_by": "No optimality argument or physical arithmetic implementation is supplied." + }, + { + "question": "Does an actual indivisible carried reader reach the d refined-grid seed orbits?", + "why_it_matters": "The classification applies only when the input domain includes these orbits.", + "first_step": "Pin one actual reader and determine its complete image under arbitrary dirty inputs.", + "blocked_by": "Source-bound reachability, arithmetic and physical caller costs are not established." + } + ] +} diff --git a/research/equivariant-grid-frame-classification/VALIDATION.md b/research/equivariant-grid-frame-classification/VALIDATION.md new file mode 100644 index 0000000000..a870c97e00 --- /dev/null +++ b/research/equivariant-grid-frame-classification/VALIDATION.md @@ -0,0 +1,78 @@ +# Validation scope + +The claim is the written equivalence in README.md. Finite execution corroborates +its mechanisms and does not replace the dimension-uniform argument. + +## Local environment and result + +CPython 3.12.15, Clang 23.1.3, macOS 27.0.1 arm64. The interpreter is +`/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12`. No third-party +Python dependencies are used. Every invocation uses `-B`. + +The direct exact replay passes. It enumerates 900 group/input fixtures, +5,100 equivariance comparisons, 4,375 two-dimensional and 59,049 +three-dimensional seed matrices. Inputs with different numerator/denominator +representations are separate fixtures; they are not claimed to be distinct +rational points. The reported maximum observed errors are only maxima over +these finite fixtures, not optimal global radii. + +The five finite group orders are 3, 8, 8, 6 and 2. The controls exhibit an +unstable nearest-point tie, coordinatewise nearest-even failure for a finite +reflection, the m=1 exception, shear error growth and a product of involutions +with infinite order. Checks use explicit exceptions and remain active under +optimized Python. No predecessor code or historical suite is executed. + +Direct normal and isolated optimized runs passed in 4.91 and 4.88 seconds +wall time. The registered runner passed both commands in 10.32 seconds total. +These are replay-duration records, not performance comparisons. Both commands +are far below their individual 120-second timeouts. + +Three deliberate verifier mutations were rejected under isolated optimized +execution. Removing the stabilizer filter produced `transport ambiguity`. +Replacing the invariant norm by the ordinary infinity norm, or omitting the +inverse transport, produced `transport changed invariant error`. These +mutations were exercised only in external scratch copies. + +The optional receipt is generated by the verifier and binds every package +file by SHA256. It is written outside the checkout; no receipt is hand-written +or checked in. Default execution is read-only. + +An isolated optimized standalone replay also passed from a Git-free, +read-only copy in an external path containing spaces. It generated its +receipt outside that copy. Standalone replay checks the mathematics; the +registered runner separately authenticates the declared Git provenance. + +## Implementation constraints + +The verifier is a closed collection of fixtures, with no matrix or point +inputs from the command line. Dimensions are at most 3 and finite group order +at most 8. Row reduction has at most 24 rows and 3 pivots. Candidate radius is +checked at 20, so each integer box has at most `41^3` candidates. Every loop +has a finite fixture, range, permutation or product bound; no recursion is +used. All functions are below 60 physical lines. Group shape and arithmetic +are trusted internal data; closure, inverses and determinant conditions are +checked before rounding. A computed fixed basis must satisfy every fixedness +equation and the rank/nullity count. Every transport must yield the same +output, including at stabilizer ties. + +Rule 3, fixed allocation, has a managed-runtime deviation in verify.py. +CPython fractions, integer arithmetic, comprehensions and standard-library +iteration allocate dynamically. Scope is this single finite replay. The +fixed dimensions, groups, point lists and radius cap bound live collections; +there are no workers, subprocesses or retained histories in the verifier. +Normal and optimized execution exercise these bounds. A fixed-allocation +implementation would require a separately specified arithmetic runtime; +no production implementation is claimed. + +Rule 10, maximum diagnostics, uses `-W error` in both registered commands. +No external Python static analyzer was available on PATH. The source is +also parsed by Python's AST parser. Repository-wide diagnostic configuration +is outside this isolated mathematical package; future integration should +apply the host's analyzer without suppressing findings. + +## Unrun obligations + +No physical rounder, source-bound reader reachability proof, optimal radius, +bit/tape cost, dirty restoration programme, full selected replay, Lean build, +Docker replay, independent human review or formal proof-kernel review is +claimed. Hosted CI is pending at initial publication. diff --git a/research/equivariant-grid-frame-classification/VERIFY.json b/research/equivariant-grid-frame-classification/VERIFY.json new file mode 100644 index 0000000000..c94c74db5e --- /dev/null +++ b/research/equivariant-grid-frame-classification/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/shear-equivariant-rounding-seed70/README.md", + "research/shear-orbit-interval-audit/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact finite-group construction, stabilizer consistency, refined-grid determinant census and semantic controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same mathematical checks with isolated imports and optimization; explicit contracts stay active." + } + ] +} diff --git a/research/equivariant-grid-frame-classification/verify.py b/research/equivariant-grid-frame-classification/verify.py new file mode 100644 index 0000000000..ddfd402caf --- /dev/null +++ b/research/equivariant-grid-frame-classification/verify.py @@ -0,0 +1,266 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the frame-group rounding theorem. + +Produced by Nick Petalas. Apache-2.0. Standard library only; no source imports. +""" + +import argparse +from fractions import Fraction as F +import hashlib +from itertools import permutations, product +import json +from math import ceil, floor, gcd, lcm +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(d): + require(1 <= d <= 3, "fixture dimension outside 1..3") + return tuple(tuple(int(i == j) for j in range(d)) for i in range(d)) + + +def apply(a, x): + return tuple(sum(c * v for c, v in zip(row, x)) for row in a) + + +def multiply(a, b): + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(len(a))) + for j in range(len(a))) for i in range(len(a))) + + +def difference(x, y): + return tuple(a - b for a, b in zip(x, y)) + + +def determinant(a): + d = len(a) + total = 0 + for p in permutations(range(d)): + inversions = sum(p[i] > p[j] for i in range(d) for j in range(i + 1, d)) + term = (-1) ** inversions + for i in range(d): + term *= a[i][p[i]] + total += term + return total + + +def invariant_norm(group, x): + return max(abs(v) for g in group for v in apply(g, x)) + + +def fixed_basis(stabilizer, d): + """Rational row reduction, followed by clearing each basis denominator.""" + rows = [[F(h[i][j] - int(i == j)) for j in range(d)] + for h in stabilizer for i in range(d)] + pivots = [] + rank = 0 + for col in range(d): + pivot = next((r for r in range(rank, len(rows)) if rows[r][col]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + scale = rows[rank][col] + rows[rank] = [v / scale for v in rows[rank]] + for r in range(len(rows)): + if r != rank: + scale = rows[r][col] + rows[r] = [v - scale * w for v, w in zip(rows[r], rows[rank])] + pivots.append(col) + rank += 1 + basis = [] + for free in range(d): + if free in pivots: + continue + x = [F(int(j == free)) for j in range(d)] + for r, col in enumerate(pivots): + x[col] = -rows[r][free] + denominator = lcm(*(v.denominator for v in x)) + z = tuple(int(v * denominator) for v in x) + divisor = gcd(*z) + z = tuple(v // divisor for v in z) + require(all(apply(h, z) == z for h in stabilizer), "invalid fixed basis") + basis.append(z) + require(len(basis) + rank == d, "nullity mismatch") + return tuple(basis) + + +def round_point(group, x): + """Finite orbit canonicalization and nearest stabilizer-fixed lattice point.""" + y = min(apply(g, x) for g in group) + transports = [g for g in group if apply(g, x) == y] + stabilizer = tuple(h for h in group if apply(h, y) == y) + basis = fixed_basis(stabilizer, len(x)) + radius = sum((invariant_norm(group, b) for b in basis), F(0)) / 2 + require(radius <= 20, "fixture candidate-radius cap exceeded") + boxes = [range(ceil(v - radius), floor(v + radius) + 1) for v in y] + candidates = [] + for z in product(*boxes): + if all(apply(h, z) == z for h in stabilizer): + error = invariant_norm(group, difference(z, y)) + if error <= radius: + candidates.append((error, z)) + require(bool(candidates), "fixed lattice covering failed") + error, z = min(candidates) + outputs = [] + for g in transports: + inverse = next(h for h in group if multiply(h, g) == identity(len(x))) + outputs.append(apply(inverse, z)) + require(all(q == outputs[0] for q in outputs), "transport ambiguity") + require(invariant_norm(group, difference(outputs[0], x)) == error, + "transport changed invariant error") + return outputs[0], radius + + +def powers(a, order): + require(1 <= order <= 8, "fixture order cap exceeded") + out = [identity(len(a))] + for _ in range(1, order): + out.append(multiply(a, out[-1])) + require(multiply(a, out[-1]) == out[0], "wrong declared order") + return tuple(out) + + +def fixture_groups(): + c3 = powers(((0, -1), (1, -1)), 3) + c4 = powers(((0, -1), (1, 0)), 4) + reflection = ((1, 0), (0, -1)) + d4 = tuple(sorted(set(c4 + tuple(multiply(g, reflection) for g in c4)))) + p, pinv = ((1, 2), (0, 1)), ((1, -2), (0, 1)) + sheared = tuple(multiply(multiply(p, g), pinv) for g in d4) + s3 = tuple(tuple(tuple(int(j == perm[i]) for j in range(3)) + for i in range(3)) for perm in permutations(range(3))) + negative_swap = (identity(2), ((0, -1), (-1, 0))) + return {"order_three": c3, "dihedral_eight": d4, + "sheared_dihedral_eight": sheared, + "permutation_six": s3, "negative_swap": negative_swap} + + +def check_group(group): + require(1 <= len(group) <= 8, "group size cap exceeded") + d = len(group[0]) + require(identity(d) in group, "missing identity") + require(len(set(group)) == len(group), "duplicate group element") + for g in group: + require(abs(determinant(g)) == 1, "nonunimodular frame") + require(any(multiply(h, g) == identity(d) for h in group), "missing inverse") + for h in group: + require(multiply(g, h) in group, "group is not closed") + + +def check_rounders(): + report = {} + for name, group in fixture_groups().items(): + check_group(group) + d = len(group[0]) + points = calls = 0 + worst = F(0) + for denominator in (1, 2, 3, 4): + for numerators in product(range(-2, 3), repeat=d): + x = tuple(F(v, denominator) for v in numerators) + q, radius = round_point(group, x) + require(all(isinstance(v, int) for v in q), "noninteger output") + error = max(abs(v) for v in difference(q, x)) + require(error <= radius, "absolute-error bound failed") + if denominator == 1: + require(q == x, "integer input changed") + worst = max(worst, error) + for g in group: + other, _ = round_point(group, apply(g, x)) + require(other == apply(g, q), "equivariance failed") + calls += 1 + points += 1 + report[name] = {"dimension": d, "order": len(group), "points": points, + "equivariance_checks": calls, "maximum_observed_error": str(worst)} + return report + + +def check_seed_matrices(): + counts = {} + for d, entries, moduli in ((2, range(-2, 3), range(2, 9)), + (3, range(-1, 2), range(2, 5))): + checked = 0 + for values in product(entries, repeat=d * d): + z = tuple(tuple(values[i * d + j] for j in range(d)) for i in range(d)) + for m in moduli: + e = tuple(tuple(m * z[i][j] - int(i == j) for j in range(d)) + for i in range(d)) + det = determinant(e) + require(det != 0 and (det - (-1) ** d) % m == 0, + "refined-grid error matrix is singular") + checked += 1 + counts[str(d)] = checked + return counts + + +def check_controls(): + """Each control discriminates a premise or an essential construction step.""" + swap = ((0, -1), (-1, 0)) + x = (F(1, 2), F(-1, 2)) + require(apply(swap, x) == x, "stabilizer fixture changed") + naive = min(product((0, 1), (-1, 0))) + require(apply(swap, naive) != naive, "unrestricted tie lost its ambiguity") + constrained, _ = round_point((identity(2), swap), x) + require(apply(swap, constrained) == constrained, "fixed tie not repaired") + # Coordinatewise nearest-even rounding need not commute with finite frames. + reflection = ((1, 1), (0, -1)) + witness = None + for a, b in product(range(-4, 5), repeat=2): + v = (F(a, 2), F(b, 2)) + lhs = tuple(round(t) for t in apply(reflection, v)) + rhs = apply(reflection, tuple(round(t) for t in v)) + if lhs != rhs and witness is None: + witness = {"input": [str(t) for t in v], "lhs": lhs, "rhs": rhs} + require(witness is not None, "coordinatewise failure disappeared") + shear = ((1, 1), (0, 1)) + # With m=1, q(x)=x is equivariant even for this infinite shear group. + seed_outputs = identity(2) + unrefined_error = tuple(tuple(seed_outputs[i][j] - int(i == j) + for j in range(2)) for i in range(2)) + require(determinant(unrefined_error) == 0, "m=1 error matrix changed") + for point in product(range(-2, 3), repeat=2): + require(apply(shear, point) == tuple(int(v) for v in apply(shear, point)), + "identity rounder left the unrefined integer domain") + for k in range(21): + g = ((1, k), (0, 1)) + require(apply(g, (0, F(1, 2))) == (F(k, 2), F(1, 2)), "orbit changed") + require(apply(g, (0, F(-1, 2)))[0] == F(-k, 2), "linear error growth") + require(determinant(shear) == 1, "shear not unimodular") + r = ((1, 1), (0, -1)) + s = ((1, 0), (0, -1)) + require(multiply(r, r) == identity(2) and multiply(s, s) == identity(2), + "involution generators changed") + require(multiply(r, s) == ((1, -1), (0, 1)), "infinite product changed") + return {"stabilizer_tie": {"input": list(map(str, x)), "naive": naive, + "fixed": constrained}, + "coordinatewise_failure": witness, + "controls": ["stabilizer tie", "coordinatewise finite-frame failure", + "m=1 singular seed", "shear error growth", + "finite-order generators with infinite product"]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="exclusively create an external receipt") + args = parser.parse_args() + report = {"claim_type": "scoped proof", "evidence": "finite corroboration", + "rounders": check_rounders(), "seed_matrices": check_seed_matrices(), + "controls": check_controls()} + package = Path(__file__).resolve().parent + report["package_sha256"] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + payload = json.dumps(report, indent=2, sort_keys=True) + "\n" + if args.receipt is not None: + require(not args.receipt.resolve().is_relative_to(package), + "receipt must be outside the package") + with args.receipt.open("x", encoding="utf-8") as output: + output.write(payload) + print(payload, end="") + print("PASS_EQUIVARIANT_GRID_FRAME_CLASSIFICATION no_new_kappa") + + +if __name__ == "__main__": + main()