Prove sharp sparse cyclic quotient minima (no new κ)

research/sparse-cyclic-quotient-obstructions/PROOF.md

@@ -0,0 +1,120 @@
+# Sharp obstructions to sparse cyclic compression
+
+Let S be a finite subset of Z^d. A cyclic projection is a homomorphism
+
+    phi_w,q(x) = w dot x modulo q,       q >= 2, w in Z^d.
+
+Call it faithful on S when its restriction to S is injective. The ambient
+lattice Z^d is fixed. We optimize over all integer weights; weights need
+not be units. This concerns a certificate's exponent support, not a physical
+address operation.
+
+## Two-point supports
+
+**Theorem 1.** Let S={u,v}, u != v, and let h>0 be the gcd of the coordinates
+of v-u. A faithful projection to Z/q exists if and only if q does not divide h.
+Consequently its smallest possible modulus is
+
+    mu(h) = min { q >= 2 : q does not divide h }.
+
+**Proof.** If q divides every coordinate difference, every dot product
+vanishes modulo q. Conversely, if q does not divide h, it fails to divide
+at least one coordinate difference. The corresponding coordinate weight
+vector separates the two points. The gcd characterization follows because
+q divides h exactly when it divides every coordinate difference. Translation
+only adds a constant residue and does not affect injectivity. QED.
+
+**Corollary 1.** Every mu(h) is a prime power, and every prime power occurs.
+No bound depending only on |S| or d bounds a faithful modulus, even for
+|S|=2 and d=1.
+
+**Proof.** Put m=mu(h). Every positive integer below m divides h. If m has
+at least two distinct prime factors, all its maximal prime-power factors
+are below m and divide h. Their least common multiple is m, a contradiction.
+Thus m is a prime power. Conversely, for a prime power m=p^a, set
+h=lcm(1,...,m-1). Its p-adic valuation is a-1, so m does not divide h, while
+every smaller positive integer does. Thus mu(h)=m. Arbitrarily large prime
+powers give the unboundedness. QED.
+
+This is an existence minimum, not merely a failure of one weight heuristic.
+The support points remain distinct over the integers throughout.
+The fixed ambient lattice matters. If the allowed domain instead becomes
+the subgroup generated by the differences, then {0,h} in hZ maps faithfully
+to Z/2 by sending h to one. That map need not extend to the original Z.
+The unboundedness therefore does not obstruct a frontend that first rebases
+the generated subgroup. It is a precise limitation of integer weights on
+the supplied coordinates.
+
+**Corollary 2.** For integer H>=1, the sharp worst-case minimum among
+two-point differences with maximum absolute coordinate at most H is
+
+    max mu(h) = min { m >= 2 : lcm(1,...,m) > H }.
+
+**Proof.** Write L_m=lcm(1,...,m), and let m be the first index with L_m>H.
+For any 1<=h<=H, the supposition mu(h)>m implies L_m divides h,
+contradicting L_m>H. Thus mu(h)<=m. The scalar difference h=L_(m-1)
+is at most H. Also m does not divide it, since otherwise L_m=L_(m-1)<=H.
+Every smaller integer divides it, so this difference attains mu(h)=m.
+Every nonzero vector difference in the stated box has gcd at most H, and
+the scalar witness embeds into any positive dimension. QED.
+
+For example, S={0,6} has optimal modulus four. Restricting the search to
+prime moduli can therefore miss the optimum.
+
+## Pairwise possibility does not give a common projection
+
+**Theorem 2.** The support
+
+    S = {(0,0), (1,0), (0,1), (1,1), (2,2)}
+
+has minimum faithful cyclic modulus six. At modulus five, every pair admits
+a separating weight vector, but no weight vector separates all five points.
+The mixed-radix box bound is nine.
+
+**Proof.** Cardinality excludes moduli below five. Suppose weights (a,b)
+are injective modulo five. The first four points have images 0,a,b,a+b.
+Their distinctness forces a,b != 0 and b/a not in {0,1,-1}. Over F5 the
+remaining possibilities are b/a=2 or 3. Scale by a^-1. If b/a=2, the final
+point has image 2(1+2)=1, colliding with (1,0). If b/a=3, it has image
+2(1+3)=3, colliding with (0,1). Thus modulus five is impossible.
+
+For every pair, the coordinate difference is nonzero modulo five. At least
+one coordinate projection separates it, proving the pairwise assertion.
+At modulus six, weights (1,3) give the distinct residues (0,1,3,4,2),
+in the displayed order. The coordinate widths are both two, so the box
+construction gives (2+1)(2+1)=9. QED.
+
+The first four points are exactly the subset sums of paid labels
+(1,0),(0,1); the last point can be a target exponent. Thus this is a
+subset-sum-plus-target support of the predecessor's declared form. It can
+be used at any register count. No candidate word or true target identity
+is asserted merely from this support description.
+Here the support generates all of Z^2, so rebasing its generated subgroup
+cannot avoid the optimum. All homomorphisms out of that group are already
+among the integer weights considered above.
+
+## Consequence for finite replay
+
+PR #1440 supplies the sufficient mixed-radix projection and faithful
+regular-action criterion. We use that criterion without replaying its
+fixtures or claiming it as new. For completeness, a binary formal coefficient
+vector supported on S maps to a cyclic coefficient vector by XORing terms
+with equal residues. If the projection is injective, different support terms
+cannot cancel, so this coefficient map is injective. If two points collide,
+their two-term sum is a nonzero formal polynomial with zero cyclic image.
+The regular action recovers cyclic coefficients by acting on the basis
+vector at address zero. Checking every role/address column detects exactly
+the cyclic coefficient map, including its kernel at an unfaithful projection.
+
+The new fixture has 32 binary support polynomials. The checker enumerates
+them all, with all weights modulo one through six, and compares direct
+translated address columns with coefficient convolution. Each noninjective
+weight gets an actual two-term kernel witness. Modulus one is a rejection
+control, not an allowed optimum. The written proofs establish the unbounded
+statements; finite checks do not extrapolate them.
+
+This is not an error in PR #1440 or an obstruction to its valid box bound.
+It explains why a smaller exact quotient needs arithmetic information and
+a simultaneous injection check. Native realization, physical conversion,
+complete signed moment, supplier admission and the multiplication theorem
+remain outside this result.

research/sparse-cyclic-quotient-obstructions/README.md

@@ -0,0 +1,114 @@
+# Sharp sparse cyclic quotient obstructions
+
+Scoped algebraic proof with exact finite corroboration. No new kappa.
+
+For a two-point exponent support {u,v}, let h be the positive gcd of the
+coordinates of v-u. With the ambient integer lattice fixed, its smallest
+faithful cyclic quotient has size
+
+    mu(h) = min { q >= 2 : q does not divide h }.
+
+Every such minimum is a prime power, and every prime power occurs. Thus even
+two points in one dimension can require arbitrarily large moduli. For maximum
+coordinate difference H, the sharp worst-case minimum is the first m with
+`lcm(1,...,m)>H`. These statements optimize over every integer weight vector.
+
+A separate exact fixture shows the simultaneous constraint. The support
+
+    {(0,0), (1,0), (0,1), (1,1), (2,2)}
+
+has optimum modulus **six**, versus its mixed-radix box bound **nine**.
+Weights (1,3) give residues (0,1,3,4,2) modulo six. Modulus five fails for every
+weight, although all ten pairs can be separated individually modulo five.
+The first four points are the subset sums of (1,0),(0,1), and the last is a
+target exponent. No true register identity is asserted from that support alone.
+
+[PROOF.md](PROOF.md) proves the unbounded laws and the exact fixture minimum.
+The result answers the short-quotient question in woklerx's
+[PR #1440](https://github.com/CrocSwap/integer-mult-bounds/pull/1440).
+It gives a smaller finite representation on a new support and two exact
+obstructions to support-size or pairwise-only compression rules. The source's
+mixed-radix theorem remains valid and is not audited here.
+
+## Reproduce
+
+From the repository root, using the local CPython 3.12 interpreter:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sparse-cyclic-quotient-obstructions/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sparse-cyclic-quotient-obstructions/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sparse-cyclic-quotient-obstructions
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sparse-cyclic-quotient-obstructions --check-source-history
+```
+
+Another CPython 3.12 path can replace the absolute interpreter path. Only the
+standard library is needed. The verifier writes no files and has no executable
+predecessor dependency. Both registered commands produce
+`PASS_SPARSE_CYCLIC_QUOTIENT_OBSTRUCTIONS no_new_kappa`; the runner also reports
+`PASS_REGISTERED_RESEARCH_PACKAGE`. A generated stdout receipt binds all six
+package files by SHA256. No handwritten receipt is used.
+
+The declared finite corroboration is:
+
+- All 4,096 scalar heights through 4,096, with the exact minimax envelope at
+  every height, and all 27 prime-power realizations through 64.
+- All 1,176 vector/modulus cases for nonzero differences in [-6,6]^2 and
+  moduli 2 through 8, enumerating 34,104 weight vectors.
+- All 91 weight vectors modulo 1 through 6 on the new support. The numbers
+  of injective projections are (0,0,0,0,0,8).
+- All 32 binary support polynomials at every such projection, comparing
+  14,112 regular-action columns against direct integer-exponent translations.
+  Every unfaithful projection gets an explicit nonzero two-term kernel witness.
+- All ten pairs modulo five, four rejected unsafe projections and three
+  semantic controls for an omitted target, prime-only search and a modulus
+  bound based solely on support size.
+
+Finite enumeration is evidence for the implementation. The written proof,
+not extrapolation from those counts, establishes the general statements.
+
+## Scope and limitations
+
+This is a verification side result under a changed task-card scope. It does
+not satisfy the card's complete decoder/supplier acceptance gate. The modulus
+is a certificate representation size; a smaller modulus is not a runtime
+speedup or a legal physical address realization. No larger-register candidate,
+selected paid/target profile, complete native/ordinary invoice, all-size
+compiler, precision, tape/stock bound or multiplication theorem is supplied.
+No selected cold replay, proof kernel or independent human review was run.
+
+The two-point obstruction assumes integer weights on the supplied ambient
+lattice. A frontend may evade it by first rebasing the subgroup generated
+by the differences: {0,h} inside hZ then needs only modulus two. That is a
+different domain for the homomorphism. The five-point support generates
+all of Z^2, so its optimum six survives such a change of group basis.
+
+[SOURCES.json](SOURCES.json) pins the source README, original catalogue and
+selected record as historical provenance at canonical main
+`de5ec2e7a6074068452f45b1a191b5c72832df4a`. They are not executable inputs.
+The package itself can replay without Git or a network. Predecessor code,
+frozen evidence and the selected frontier are unchanged.
+
+The Python checker uses bounded finite loops and functions below 60 lines.
+Managed-runtime allocation is the Power of Ten deviation: live collections
+are limited to 32 polynomial images, six fixture success counts and a fixed
+six-file hash receipt, plus fixed-size vectors. Integer values are bounded
+by the displayed scalar and prime-power domains. It has no recursive calls,
+code generation, subprocesses or hidden runtime dispatch.
+
+## Open next questions
+
+Can one compress the full support of an actual larger-register candidate
+below its mixed-radix box bound? First retain every subset sum and target
+exponent, test arithmetic pair obstructions, then certify one simultaneous
+injective weight vector. A specified candidate and an explicit representation
+cost allowance are missing. [TASK.json](TASK.json) records this handoff.
+
+## Credit
+
+The sharp sparse-support analysis, new five-point fixture, proof and checker
+were produced by Nick Petalas. Credit woklerx's PR #1440 for posing the
+short-quotient question, its sufficient mixed-radix injection and faithful
+regular-action criterion, and its retained eumemic PR #288 / huxint PR #203
+register-model lineage. Gcd, least-common-multiple and regular-representation
+facts are classical; no general literature-priority claim is made.
+Independent human and formal proof-kernel review are unclaimed. Apache-2.0.

research/sparse-cyclic-quotient-obstructions/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bit-faithful-finite-address/README.md",
+      "usage": "provenance",
+      "git_blob": "0f3c0ded3e2ec8af5e50d9919784cde88ab29bb4",
+      "sha256": "b4e345bc8e86d069979a57ade7cb381812474ffbb0d7033d5a1283fc99eb16cb"
+    }
+  ]
+}

research/sparse-cyclic-quotient-obstructions/TASK.json

@@ -0,0 +1,75 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp fixed-ambient-lattice obstructions and exact smallest faithful cyclic quotients for two-point supports and one five-point subset-sum/target support.",
+  "scope_change_reason": "The selected baseline binds correctly, but this is an explicitly scoped verification side result answering PR1440's short-quotient question. It does not price a changed decoder or satisfy the original complete supplier gate.",
+  "bottleneck_link": "A faithful cyclic quotient can reduce the exact finite certificate representation. The result identifies arithmetic and simultaneous-separation barriers to compressing that representation. It does not change a recursive invoice.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first checked exact modulus improvement and sparse-support obstruction; package the five-point optimum and two-point law without extending to a larger search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the unbounded gcd/LCM laws and exact five-point minimum. verify.py generates a SHA256-bound receipt for all six package files and exhausts the declared finite domains.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one compress the full support of an actual larger-register candidate below its mixed-radix box bound?",
+      "why_it_matters": "This would turn the sparse-support criteria into a concrete reduction of finite replay state and column count.",
+      "first_step": "Retain every subset sum and target exponent of one newly proposed candidate, test arithmetic pair obstructions, and certify one simultaneous injective weight vector.",
+      "blocked_by": "A specified candidate with a complete support and an explicit representation-cost allowance; pairwise separation alone is insufficient."
+    }
+  ]
+}

research/sparse-cyclic-quotient-obstructions/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact two-point gcd/LCM laws on the stated finite domains; all small-fixture projections and binary regular-action columns; unsafe quotient, omitted-target, prime-only and support-size controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact two-point gcd/LCM laws on the stated finite domains; all small-fixture projections and binary regular-action columns; unsafe quotient, omitted-target, prime-only and support-size controls."
+    }
+  ]
+}