Prove exact affine-lattice hulls of rounded-linear programs (no κ)

research/rounded-program-affine-hull/PROOF.md

@@ -0,0 +1,172 @@
+# Exact images and affine-lattice hulls of rounded-linear programs
+
+## 1. Contract
+
+Let the independent parameters be `z in Z^k`, with finite `k >= 1`.
+A program has finitely many scalar registers. Its initial registers and
+every unrounded assignment are rational affine combinations of `z` and
+previous registers. A rounded assignment applies
+
+    R(t) = floor(t + 1/2)
+
+to such a rational affine combination. Outputs are any fixed list of
+registers. Write the resulting map as `F: Z^k -> Q^m`.
+
+This includes a rational affine entrance `x=x0+Bz`, correlated or redundant
+parameters, separately rounded shears and rational rescaling. A fixed
+rational-grid rounder is a composition of rational scaling, R and scaling
+back. No variable products, data-dependent branches, unbounded iteration,
+overflow or saturation are included. A finite unrolled sequence is allowed.
+
+An affine lattice means `y+Lambda`, where Lambda is a finitely generated
+additive subgroup of `Q^m`. Its rank may be less than m. These groups are
+discrete in their real linear spans because their generators are rational.
+All integer combinations use signed, unbounded integer coefficients.
+
+## 2. A computable translation lattice
+
+Replace each occurrence of R by the identity map. Propagate the linear
+coefficient row of each register with respect to z through this idealized
+program. Let `d_j in Q^(1 x k)` be the idealized coefficient row of the
+argument of rounded assignment j, and let `M in Q^(m x k)` be the final
+output coefficient matrix. Affine constants do not enter these rows.
+
+Choose any finite-index subgroup `H <= Z^k` such that
+
+    d_j h is an integer for every rounded assignment j and every h in H.  (1)
+
+Such a subgroup always exists. If q is the least common multiple of all
+denominators in all d_j, with q=1 when there are no rounded assignments,
+then `q Z^k` satisfies (1). Alternatively, the kernel of the finite-image
+map `h -> (d_j h mod Z)_j` gives a possibly larger H. Neither choice is
+asserted to be the maximal translation subgroup of F.
+
+**Translation lemma.** For every z in `Z^k` and h in H,
+
+    F(z+h) = F(z) + M h.                                           (2)
+
+Proof. Induct through the actual program. Initially each register has
+exactly its idealized linear drift on replacing z by z+h. Rational affine
+combinations preserve this property. At rounded assignment j, the induction
+hypothesis makes the actual argument drift exactly `d_j h`. This is an
+integer by (1), and `R(t+n)=R(t)+n` for every real t and integer n, including
+negative t and half-integer ties. Thus the rounded register has the same
+drift as its idealized counterpart. The output rows give (2). No linearity
+of the rounded program has been assumed.
+
+## 3. Exact output set and its smallest affine lattice
+
+Let C be any complete set of representatives of `Z^k/H`, containing 0,
+and let `h_1,...,h_k` be an integer basis of H. Define
+
+    L0 = M H = sum_i Z (M h_i),
+    G  = L0 + sum_(c in C) Z (F(c)-F(0)).
+
+**Theorem.** The complete, unbounded output set and its smallest containing
+affine lattice are exactly
+
+    F(Z^k) = union_(c in C) (F(c) + L0),                            (3)
+    hull_Z(F(Z^k)) = F(0) + G.                                    (4)
+
+Proof of (3). Every z is uniquely c+h with c in C and h in H. Equation
+(2) gives `F(z)=F(c)+Mh`. Conversely every element of `F(c)+MH` equals
+`F(c+h)` for some h in H. Both inclusions therefore hold, even when M
+has a kernel or L0 has smaller rank than the output space.
+
+Proof of (4). Formula (3) places every output in `F(0)+G`. Conversely,
+suppose an affine lattice contains all outputs. Since it contains F(0),
+write it as `F(0)+Lambda`. It contains each difference `F(c)-F(0)`.
+It also contains `F(h_i)-F(0)=M h_i`. Therefore `G <= Lambda`.
+This proves minimality among all affine lattices, including skew lattices
+and lattices with lower rank. It proves independence from C, its basis and
+the permissible H used to compute the answer.
+
+For the rectangular choice `H=q Z^k`, (4) gives an explicit finite
+generating list with at most `q^k - 1 + k` vectors:
+
+    F(c)-F(0) for c in {0,...,q-1}^k except 0,
+    q M e_i for i=1,...,k.                                        (5)
+
+This is an exact finite reduction, not a polynomial-time bound. The
+denominator product or the number of input parameters can make q^k large.
+No optimality of this generating-list length or period is claimed.
+
+## 4. Necessary and sufficient closure test
+
+For a proposed rational target affine lattice `y0+Lambda`, the following
+three finite conditions are jointly necessary and sufficient:
+
+    F(0)-y0 belongs to Lambda;
+    M h_i belongs to Lambda for every basis vector h_i of H;
+    F(c)-F(0) belongs to Lambda for every c in C.                    (6)
+
+This follows directly from (4), or from both inclusions of (3). Membership
+in a rational finitely generated lattice is an exact integer-module
+problem after clearing denominators. Thus (6) is a decision procedure,
+with no numerical tolerance and no bounded-reachability assumption.
+
+For a sequence of separately specified input and target lattices, applying
+(6) at every boundary proves preservation by induction from an admitted
+entrance. This is a conditional interface implication. It neither proves
+that the chosen entrance describes an actual selected caller nor states
+that replacing a nonlinear reachable set by its hull preserves all its
+nonlattice information. The lattice hull is the strongest *affine-lattice*
+consequence of the given complete parameter domain.
+
+## 5. Why residue outputs alone are insufficient
+
+Consider the separately rounded shear on a new input domain
+
+    x=3n, y=2m,
+    F(n,m) = (3n, 2m + R(3n/2)).
+
+Here q=2 is a valid rectangular period and
+
+    M = [[3,0],[3/2,2]],
+    F(0,0) = (0,0),
+    q M e_1 = (6,3),    q M e_2 = (0,4).
+
+All four residue outputs for `n,m in {0,1}` have even second coordinate.
+Checking only these outputs would incorrectly admit target `3Z x 2Z`.
+The actual output `F(2,0)=(6,3)` rejects it. The missing obligation is the
+drift generator, not another residue representative.
+
+The residue difference `(3,2)`, the generator `(6,3)` and the residue
+difference `(0,2)` generate precisely `3Z x Z`: subtract twice `(3,2)`
+from `(6,3)` to obtain `(0,-1)`, then obtain `(3,0)`. Every output has
+first coordinate divisible by 3, proving the reverse containment.
+Consequently the exact hull is `3Z x Z`, while `(0,1)` belongs to this
+hull and is not an output. This distinguishes the hull from the output set.
+The idealized output lattice contains `(3,3/2)`, so it would incorrectly
+reject the actually valid target `3Z x Z`. Thus ideal-image-only testing
+can also give a false closure verdict, in the other direction.
+
+For this example the larger H with basis `(2,0),(0,1)` uses just two
+residue representatives, with drift generators `(6,3),(0,2)`. It yields
+the same hull. The proof does not require the rectangular period to be
+minimal.
+
+## 6. Evidence and scope
+
+The written induction and subgroup argument prove the quantified result.
+The companion verifier corroborates it on nested and two-input rational
+programs. Its second route computes the integer lattice generated by
+literal outputs in a larger signed parameter box, without idealizing any
+rounding node. It also checks actual translation identities and explicit
+failures of residue-only and ideal-image-only shortcuts.
+
+woklerx #1848 supplies the source question about closure under intervening
+updates and the separate mixed-precision cancellation interface. Adam Gall
+#1908 already shows that ideal closure does not imply actual rounded-leaf
+closure. Nick Petalas #6446 classifies common invariant planar lattices for
+opposite rounded shears. Their results are cited rather than replayed, and
+the theorem here does not depend on any of their numerical certificates.
+Integer-translation equivariance, lattice normal forms and finite-coset
+reasoning are classical. No literature-wide priority is claimed for those
+ingredients. The new contribution is this exact output-set/hull formula
+and finite closure criterion for the stated rounded-program interface.
+
+No particular selected native program is admitted. Actual reachable input
+domains, physical owners, restoration, movement/storage/precision charges,
+the full recursive invoice and the selected five framework assumptions
+remain separate. There is no new kappa or complete multiplication theorem.

research/rounded-program-affine-hull/README.md

@@ -0,0 +1,140 @@
+# Exact affine-lattice output hulls for rounded-linear programs
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written proof with exact finite corroboration.
+
+For every finite rational rounded-linear program on integer parameters,
+the complete output set is a computable finite union of translates of one
+lattice. Its smallest containing affine lattice has an explicit finite
+generating set. This gives a necessary and sufficient test for closure in
+any proposed rational affine target lattice, including changing domains
+and internally nested rounding nodes.
+
+For `R(t)=floor(t+1/2)`, replace each rounding node by the identity and
+propagate its argument's rational linear row. Let q clear every denominator
+in these rows, M be the idealized output matrix and `C={0,...,q-1}^k`.
+Then the new exact formulas are
+
+```text
+F(Z^k) = union_(c in C) (F(c) + q M Z^k)
+hull_Z(F(Z^k)) = F(0) + span_Z({q M e_i}_i, {F(c)-F(0)}_c)
+```
+
+[PROOF.md](PROOF.md) proves translation equivariance by induction through
+the actual rounded program and proves both equalities and minimality.
+A larger permissible translation lattice may reduce the residue set.
+The rectangular formula uses at most `q^k-1+k` generators; it makes no
+polynomial-time or minimal-period claim.
+
+The distinction between residues and drift matters. On the entrance
+`x=3n, y=2m`, the shear `(x,y) -> (x,y+R(x/2))` has even second coordinates
+on all four q=2 residue representatives. Nevertheless `F(2,0)=(6,3)`.
+Its exact affine-lattice hull is `3Z x Z`, while the proposed target
+`3Z x 2Z` fails. Ideal-image and residue-only closure tests both miss
+information supplied by the formula. The output set itself is smaller
+than its hull.
+
+## Evidence and reproduction
+
+From the repository root with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rounded-program-affine-hull/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rounded-program-affine-hull/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-program-affine-hull
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-program-affine-hull --check-source-history
+```
+
+Another CPython 3.12 path may substitute. The last command requires the
+committed package. Direct verification is read-only and Git-free. It prints
+a generated JSON receipt bound to all six package source hashes, followed
+by `PASS_ROUNDED_PROGRAM_AFFINE_HULL`. Both direct modes are registered in
+[VERIFY.json](VERIFY.json); the runner reports `PASS_REGISTERED_RESEARCH_PACKAGE`.
+
+The finite census contains 80 one-parameter nested-rounding programs and
+256 two-parameter rounded-shear programs with rational affine entrances.
+Across these 336 programs it checks 3,904 residue outputs, 33,696 literal
+outputs in signed parameter boxes and 6,336 affine target-closure comparisons.
+The literal-output route generates its lattice without idealizing the
+rounding nodes. All translation identities and hull comparisons agree.
+These are enumerated fixtures, not a count of distinct functions.
+
+An independent determinantal-minor check and rank-one content check cover
+all 729 ordered triples of planar vectors with coordinates in `{-1,0,1}`.
+Fourteen named semantic controls cover the drift counterexample, ideal
+image, nested denominators, signed ties, a smaller nonrectangular period,
+rank-zero and unrounded rational maps. Five malformed-program cases reject.
+The universal statements rest on the written proof, rather than this census.
+
+## Source, credit and scope
+
+Credit woklerx [#1848](https://github.com/CrocSwap/integer-mult-bounds/pull/1848),
+head `d975e19e7e931fc2b45792a4f7140ac13759a7da`, for the explicit question
+about closure under intervening rounded updates and the affine-domain
+mixed-precision interface. Its cancellation theorem is a cited result.
+Retain Gareth Davidson, Chafik Boukhalfa and Ali Romman's precision and
+dirty-restoration lineage credited there.
+
+Adam Gall [#1908](https://github.com/CrocSwap/integer-mult-bounds/pull/1908)
+already gives a source-specific internally rounded-leaf counterexample.
+Nick Petalas [#6446](https://github.com/CrocSwap/integer-mult-bounds/pull/6446)
+classifies a common invariant integer lattice for opposite planar rounded
+shears. Those contracts are related context; neither result nor executable
+is used as a step in this proof. Their numerical certificates are not
+replayed. The new formula and general closure criterion above are the
+contribution. The elementary translation, coset and integer-lattice
+methods are classical, with no literature-wide priority claim.
+
+[TASK.json](TASK.json) records a change from the caller-specific
+`uniform-transfer-audit` card to this general precision-interface lemma.
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19572796)
+states the same mathematical scope. Canonical base is
+`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8 and selected
+#7000. [SOURCES.json](SOURCES.json) binds the source question and related
+packages as historical provenance. There are no external runtime inputs.
+
+Live open PRs, this account's recent work, the latest handoff posts,
+active discussions, local reservations, main-tree README terms and merged
+PR searches were checked. The cached card scan covered 768 open PRs,
+7,355 Discussion records and 10,178 local note records, with separately
+reported freshness. A dedicated author/date scan of 768 open and 6,175
+closed PRs found no recent account PR referencing #1848. Searches cover
+titles, bodies and notes, not every code diff or unpublished result.
+
+## Limits and verification design
+
+The contract has fixed rational affine arithmetic and half-up rounding,
+with finitely many nodes and unrestricted integer parameters. Variable
+products, data-dependent branches, overflow and saturation are excluded.
+The output lattice need not equal the actual reachable set. Replacing
+a reachable set by its hull discards nonlattice information.
+
+No actual selected caller, entrance contract or useful precision policy
+is established. Complete native implementation, owners and restoration,
+movement/storage/precision charges, recursive invoice and all five selected
+framework assumptions remain open. No new kappa, supplier admission,
+selected-frontier change or complete multiplication theorem is claimed.
+Independent human and formal proof-kernel review are unclaimed. No
+predecessor scientific replay, selected cold replay, Lean or Docker run
+was performed.
+
+The verifier has no recursion, subprocesses, external libraries or writes.
+Its fixture contract limits inputs to two parameters, eight nodes and
+period at most 12. Each literal parameter box therefore has at most 1,296
+points; only one program's vectors are live. Package source reads are
+capped at 128 KiB each. All checks remain active under optimized Python.
+Functions fit within 60 physical lines. Python's dynamic allocation is
+a managed-runtime deviation from fixed memory; these bounds constrain
+live collections, while no allocation-free or static-analyzer claim is
+made. Warning-strict normal and optimized execution provide the available
+interpreter diagnostics.
+
+## Open next questions
+
+Apply the criterion to one literal selected rounded caller with an admitted
+rational affine entrance. First extract its fixed rounded-linear fragment
+and compute the residue outputs and drift vectors, then test the next
+required source domain. The caller's exact entrance and reachability,
+later inverse compatibility and complete precision, movement, storage and
+restoration bill remain blockers. No continuation is part of this result;
+the structured question is in [TASK.json](TASK.json).

research/rounded-program-affine-hull/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "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"
+    },
+    {
+      "path": "research/rounded-leaf-lattice-closure/README.md",
+      "usage": "provenance",
+      "git_blob": "505a6b7d6e833b32cb3b6893522dab64a174311f",
+      "sha256": "8346e7579c265c5c4d96bd61f25c954422ccd74394eca63f41f564085e4f75b8"
+    },
+    {
+      "path": "research/rounded-shear-lattice-closure/README.md",
+      "usage": "provenance",
+      "git_blob": "5d1c98c8cfb62ad29531472000a8385a9571cda3",
+      "sha256": "dd69ded761a095392f97a620df89227f552991fcb530282d62a2a96daa39095c"
+    }
+  ]
+}