Prove the exact two-image inverse input lattice (no new κ)

research/two-image-inverse-lattice/PROOF.md

@@ -0,0 +1,164 @@
+# Exact inverse input lattice
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let D = Z[i,1/2], f >= 1 and n = 8^f. Use the literal letters of
+lee-phys's #4688 and Yiyang's #4710, as fixed in Cinna Davis's #4998:
+
+- U e_(x0,x1,x2) = e_(x0,x1,x2+x0).
+- V e_(x0,x1,x2) = e_(x1,x0,x2).
+- S e_x = i^popcount(x) e_x, P = SUS, Q = SVS.
+- C = ((1+i)/2) I + ((1-i)/2) X_0.
+
+A subscript f means the tensor power of that individual letter. Define
+
+    F_f = C_f (U_f + 2 V_f) C_f,
+    F'_f = C_f (P_f + 2 Q_f) C_f.
+
+These are the two prescribed first outputs of #4998. Its second output is
+the inverse applied to an independent input. We cite its operator definition
+and inverse construction as premises; we do not audit that construction.
+
+For either G = F_f or F'_f, put
+
+    a_f = (4^f + 2^f)/2,
+    b_f = (8^f - 4^f)/4,
+    h_f = a_f + b_f = (8^f + 4^f + 2*2^f)/4.
+
+The new claim is the following D-module isomorphism:
+
+    D^n / G D^n  =  (D/(3))^a_f  direct-sum  (D/(15))^b_f.       (1)
+
+Thus the exact index is 9^h_f * 25^b_f. The independent inverse input y
+has G^-1 y in D^n precisely when y belongs to G D^n. Its fraction in every
+complete residue period modulo 15, on any fixed dyadic Gaussian grid, is
+
+    9^(-h_f) * 25^(-b_f).                                      (2)
+
+At f=1 this is 1/164025. At every f>=1 the least positive odd integer m
+such that m G^-1 D^n is contained in D^n is exactly 15. This is a statement
+about the odd denominator; no fixed bound on powers of two is claimed.
+
+## Reduction to cycle relations
+
+C^2 = X_0, so C^-1 = X_0 C has entries in D. Consequently C_f is in
+GL_n(D). The same holds for the permutation letters and the phase S_f.
+For R = U^-1 V = UV, let H_f = I + 2 R_f. Then
+
+    F_f  = (C_f U_f) H_f C_f,
+    F'_f = (C_f S_f U_f) H_f (S_f C_f).                         (3)
+
+The repaired identity follows from P_f + 2 Q_f = S_f (U_f+2V_f) S_f.
+Both sides of H_f in (3) are unimodular over D. Right multiplication does
+not change its image module; left multiplication carries that module by an
+ambient automorphism. Thus both cokernels are isomorphic to coker H_f.
+This reduction preserves the actual phase-repaired interface, rather than
+replacing it with an unsigned permutation matrix.
+
+On the eight base addresses, the cycles of R are
+
+    (0), (4), (1,2,5,6), (3,7).
+
+The fixed-point counts of R and R^2 are 2 and 4. Independent tensor digits
+therefore give 2^f fixed points of R_f and 4^f fixed points of R_f^2.
+Since R_f has order four, its cycle counts are
+
+    c1 = 2^f,
+    c2 = (4^f - 2^f)/2,
+    c4 = (8^f - 4^f)/4.
+
+Here c1+c2=a_f and c4=b_f. In particular b_f>0 for every positive f.
+
+## One cycle, with an explicit quotient map
+
+Order a cycle of length ell in {1,2,4} as e_0,...,e_(ell-1), with
+R_f e_j = e_(j+1 mod ell). The image relations of H_f are
+
+    e_j + 2 e_(j+1) = 0.
+
+Because 2 is a unit in D, these relations express every generator using
+e_0, and the closing relation is (1-(-2)^ell)e_0=0. There are no further
+relations. Explicitly, let d_ell=abs(1-(-2)^ell), and set
+
+    phi_ell(z) = sum_(j=0)^(ell-1) (-2)^(ell-j) z_j mod d_ell.   (4)
+
+Each column e_j+2e_(j+1) maps to zero, including the closing column.
+The coefficient at z_0 is (-2)^ell, which is a unit modulo d_ell, so phi
+is onto. Conversely the generator elimination just given shows that the
+quotient is generated by one element killed by d_ell. Its surjection onto
+D/(d_ell) is therefore an isomorphism. Hence
+
+    coker(I+2 cycle_ell) = D/(d_ell),
+    d_1=3, d_2=3, d_4=15.
+
+This proves (1) by the direct sum over disjoint cycles. It is also an
+invariant-factor decomposition over D. Unit diagonal entries are omitted.
+No finite-field rank measurement is used to infer higher prime powers.
+
+## Actual input membership and exact density
+
+For an actual input y, first compute z = L^-1 y, where the left factor L
+in (3) is C_f U_f or C_f S_f U_f. Thus
+
+    z = U_f C_f^-1 y                    for the original prefix,
+    z = U_f S_f^-1 C_f^-1 y             for the repaired prefix.
+
+Apply (4) separately on every R_f cycle. The inverse output is dyadic
+Gaussian if and only if every resulting congruence is zero. On a four-cycle
+one can use the weights (1,7,4,13) modulo 15. Replacing those weights by a
+plain sum is incorrect.
+
+The quotient D/(d) has d^2 elements for odd positive d. Indeed reducing the
+real and imaginary integer coordinates modulo d gives d^2 possibilities,
+and inverting 2 does not change them. Therefore the independent conditions
+have total index 9^a_f * 225^b_f = 9^h_f * 25^b_f. Also 15D^n is contained
+in G D^n by (1). Reduction modulo 15D^n makes the membership condition a
+kernel of that exact index. Any dyadic grid 2^-q Z[i]^n maps bijectively
+onto all residue coordinates modulo 15D^n when its integer numerators run
+over a complete period of length 15 in each real coordinate. Every kernel
+fiber has equal size. This proves (2), without assuming a probability
+measure on the infinite set D^n. Expanding boxes in any such fixed grid
+have the same limiting natural density.
+
+The first independent input x of #4998 always has Gx in D^n. Thus the same
+fraction describes pairs (x,y) with both prescribed outputs in D^n.
+A caller may deliberately restrict y to G D^n, in which case every input
+it supplies is safe. The complete-period fraction is not a claim about
+that caller's distribution.
+
+## Sharp denominator and implementation consequence
+
+For a positive odd integer m,
+
+    m G^-1 D^n subset D^n  iff  m D^n subset G D^n.
+
+Equivalently m annihilates the cokernel in (1). Since b_f>0, the summand
+D/(15) forces m to lie in 15D. For an ordinary odd integer this means
+15 divides m. Conversely 15 kills every summand. Thus the least such m
+is exactly 15 at every width. Both odd primes are necessary; a larger
+dyadic precision alone cannot remove either one for unrestricted inputs.
+
+Any exact implementation whose input, intermediate and literal output
+coordinates all lie in D cannot deliver the prescribed pair on all of D^n.
+This follows already from its output set, regardless of how much D-valued
+workspace it has. A dyadic-linear program is one example. The statement
+allows exact odd-denominator arithmetic, rational encodings with a decoded
+output contract, rounded outputs and restricted safe inputs as changed
+premises. It does not rule out any of those alternatives or price them.
+
+## Evidence and limits
+
+The universal theorem is the written module argument above. The self-contained
+verifier enumerates the new cycle counts at widths 1 through 5, exhausts all
+50,865 real residue vectors on the three cycle types, and checks the literal
+Gaussian realifications at widths 1 and 2 modulo 3 and 5. Its separate rational
+matrix inversion at width 1 checks both prefixes' sharp odd denominator and
+128 input-membership probes, plus 32 forward-image columns. These are finite
+corroboration, not a proof-kernel certificate or an audit of predecessor words.
+
+No complete multiplication theorem, new kappa, physical realization, precision
+budget, Gaussian-compatible consumer or supplier admission follows. The proof
+uses the elementary cyclic presentation computation and makes no claim of
+literature priority for Smith normal form or finite-module counting.

research/two-image-inverse-lattice/README.md

@@ -0,0 +1,119 @@
+# Exact dyadic input lattice for the compensated two-image inverse
+
+Claim type: scoped all-width proof with finite corroboration. No new kappa.
+This contribution was produced by Nick Petalas.
+
+For either prefix G_f in Cinna Davis's [#4998](https://github.com/CrocSwap/integer-mult-bounds/pull/4998),
+let D = Z[i,1/2], n = 8^f, and
+
+    a = (4^f + 2^f)/2,   b = (8^f - 4^f)/4.
+
+The new result is the exact inverse-input lattice quotient
+
+    D^n / G_f D^n = (D/(3))^a direct-sum (D/(15))^b.
+
+Consequently an independent input y has dyadic Gaussian inverse output
+G_f^-1 y on exactly the fraction 9^(-a-b) * 25^(-b) of every complete
+residue period on any fixed dyadic Gaussian grid. At width one the fraction
+is 1/164025. The least odd denominator needed for unrestricted exact inputs
+is exactly 15 at every positive width. Merely increasing dyadic precision
+cannot supply literal exact outputs on every input.
+
+[PROOF.md](PROOF.md) gives the all-width module proof and explicit input
+congruences, including the actual phase-repaired frames. The denominator 15
+and its sufficiency were already explicit in #4688/#4998. The contribution
+here is its necessity, the complete quotient and the exact safe-input lattice
+and density. No predecessor program is imported, replayed or audited.
+
+This answers the exact-grid feasibility part of #4998 Open next question 2.
+Exact odd-denominator encodings, rounded realizations and inputs deliberately
+restricted to the safe lattice remain available changed contracts. No physical
+cost or rounding error estimate is supplied. The selected frontier is unchanged.
+
+## Evidence and reproduction
+
+From the repository root, with the Python 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-image-inverse-lattice/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/two-image-inverse-lattice/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-image-inverse-lattice
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-image-inverse-lattice --check-source-history
+```
+
+Any CPython 3.12 executable can replace the local interpreter path. The direct
+verifier also runs without Git or predecessor files. It writes nothing and
+prints a freshly generated result with hashes of every package file.
+
+Expected marker: `PASS_TWO_IMAGE_INVERSE_LATTICE`.
+
+The verifier enumerates cycles at widths 1 through 5 and all 50,865 real
+residue vectors on cycle lengths 1, 2 and 4. Their safe counts are 5, 75
+and 3375. It separately constructs the literal Gaussian operators and checks
+realified ranks modulo 3 and 5 at widths 1 and 2 for both variants. Those
+ranks are (8,14) at width one and (84,104) at width two. A separate rational
+inverse at width one checks the sharp odd denominator, 128 input-membership
+probes and 32 forward-image columns. False unweighted cycle congruences and
+single-prime denominator replacements have explicit counterexamples. Finite
+checks corroborate the written proof; they do not establish its universal
+quantifiers by enumeration.
+
+## Scope and source record
+
+Base: `4c0a359d88f22f05189d51f48387750b801a45d4`, priority revision 7.
+The `complex-new-helper-inventory` card is explicitly changed to a numerical
+interface side result. Its historical first command fails with
+`KeyError: 'complex_profile'` against the newer selected schema; the current
+`scripts/research_selected_baseline.py` control passes. That control only checks
+source-bound metadata. No frozen supplier, shared script or predecessor file
+is changed.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141364)
+reserves this exact lattice question. The initial overlap cache covers 329
+open PR bodies and 4,185 Discussion records with complete remote pagination.
+Only 147 of 6,760 local note paths were materialized at the targeted scan;
+separate main-tree and merged-PR searches cover distinctive object and formula
+terms. Sparse notes, arbitrary diffs and unpublished work limit coverage.
+[SOURCES.json](SOURCES.json) records historical provenance; the verifier has
+no external mathematical inputs.
+
+## Limitations
+
+The exact-output obstruction assumes literal D-valued input and output
+coordinates. It does not exclude rational encodings, odd-denominator arithmetic,
+rounded outputs or safe-lattice inputs. Complete-period density need not equal
+an actual caller's input distribution. Powers of two in a finite precision
+format are unpriced. Physical routing, storage, precision, a useful Gaussian
+consumer, supplier admission and the complete multiplication theorem remain
+unproved. Independent human and formal proof-kernel review are unclaimed.
+Lean, Docker and the selected scientific cold replay are unrun.
+
+The verifier uses managed allocation. The largest orbit census has 32,768
+addresses; literal matrices have at most 128 real coordinates; rational inversion
+uses 16 coordinates. All loops have bounds from those fixed domains, no recursion
+or dynamic evaluation is used, and functions stay below 60 lines. Python's
+runtime and ordinary library dispatch allocate dynamically; no fixed-memory
+runtime guarantee is made. Both registered commands treat warnings as errors
+and keep their checks active under optimization.
+
+## Open next questions
+
+1. Can an actual caller produce its independent inverse input directly in
+   G_f D^n without paying back the intended benefit? Begin with one named
+   producer and the explicit cycle congruences. Independence, input distribution
+   and complete preparation/restoration costs are unresolved.
+2. Can a rationally encoded or rounded invocation meet a complete native
+   precision/storage/routing bill? Begin with one exact odd-denominator output
+   representation or one rounded return contract. The lattice theorem supplies
+   no numerical error or complete physical cost bound.
+
+## Credit
+
+Cinna Davis #4998 supplies the compensated interface and its exact-grid open
+question, following #4991. lee-phys #4688 supplies the original prefix and its
+order-four inverse polynomial. Yiyang #4710 supplies the phase repair.
+Dugongue #4743 supplies arbitrary-input triangular ports. Jacob Alan Sussman
+#4628, eumemic #288 and Swapnil Jain P1/P2 supply the retained small-unit and
+certificate lineage. The cyclic presentation and finite-module counting tools
+are classical; their application to this exact inverse input lattice is proved
+here. Original sources and notices are unchanged. Apache-2.0.

research/two-image-inverse-lattice/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/two-image-compensated-pair/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c2d4d743f368d5e1cdf1955303f7d2d8a077b735",
+      "sha256": "bc07ad665eab28e8fbac7577b8ecb3cf35c24332688fc9354f5680199bfc727f"
+    },
+    {
+      "path": "research/two-image-compensated-pair/README.md",
+      "usage": "provenance",
+      "git_blob": "0a76dfcff068a3199cfe473b8acf6543bc9e2ba9",
+      "sha256": "f7e94b7e5602f4243dd94013f92560eda1ee6cee4706b9df05841382e8887198"
+    }
+  ]
+}