Prove sharp ternary denominator cutoffs for short decompositions (no κ)

research/ternary-short-denominator-cutoff/PROOF.md

@@ -0,0 +1,104 @@
+# A sharp denominator cutoff for short ternary decompositions
+
+For nonzero vectors u,v in {-1,0,1}^3 and an integer j>=1, call
+A=2^(-j)uv^T a frame. Repetitions and negative entries are allowed.
+Every entry has absolute value at most 1/2. The exponent j is intrinsic,
+since some entry of uv^T is odd.
+
+## The theorem
+
+1. If at most four frames sum to I3, every exponent is at most two.
+2. If at most five frames sum to 2I3, every exponent is at most two.
+
+Both denominator cutoffs and both term limits are sharp. The proof is
+uniform in j and uses no finite frame census or register-word theorem.
+
+## Four terms summing to I3
+
+Suppose the largest exponent is J>=3, with multiplicity t. Clear
+denominators by multiplying by 2^J and reduce entries modulo two.
+The right side and all smaller-exponent frames vanish. A single deepest
+numerator uv^T cannot vanish, since both vectors have nonzero binary
+reduction. Thus t>=2.
+
+If t>=3, even with four terms any diagonal entry is at most
+
+    (4-t)/2 + t/8 <= 7/8 < 1.
+
+This is impossible. Thus t=2. Fewer than four terms would give at most
+1/2+2/8<1 on a diagonal. There are exactly two remaining terms.
+
+If both have exponent one, their diagonal sums are multiples of 1/2,
+at most one. The deepest pair contributes at most 1/4 in absolute value
+at each entry. Each shallow diagonal sum must therefore equal one.
+Each shallow frame has all three diagonal entries +1/2. Its numerator
+is ww^T for a full sign vector w in {+1,-1}^3, because u_i v_i=1 forces
+u_i=v_i=+1 or -1 at every coordinate.
+
+Every off-diagonal entry of the sum of two such half frames is an integer
+in {-1,0,1}. The deepest pair cannot cancel a nonzero integer. Hence the
+shallow sum has zero off-diagonal entries and diagonal one, so it is I3.
+Its rank is at most two, contradicting rank(I3)=3.
+
+Otherwise the two shallow coefficients have sum at most 1/2+1/4. If
+neither is a half, the full diagonal is at most 1/4+1/4+1/8+1/8<1.
+The only remaining possibility saturates the diagonal bound exactly.
+Its exponents are (1,2,3,3), and every numerator is a full sign square
+ww^T. All frames are then positive semidefinite. For the vector w of
+the half frame,
+
+    w^T (sum A) w >= (1/2)(w^T w)^2 = 9/2,
+    w^T I3 w = 3.
+
+This contradiction proves the first statement for every exponent.
+
+## Five terms summing to 2I3
+
+Suppose one frame A has exponent J>=3, so its entries have absolute value
+at most 1/8. On a diagonal the other at most four frames contribute at
+most two. If one such contribution is not +1/2, it is at most +1/4 by
+the dyadic alphabet. The full diagonal is then at most
+
+    3/2 + 1/4 + 1/8 = 15/8 < 2.
+
+There must therefore be four other frames, each with all diagonal entries
++1/2. They are full sign squares divided by two. Their diagonal sum is
+exactly two, so A has zero diagonal. Their off-diagonal sums are integers,
+because each is a sum of four numbers in {+1/2,-1/2}. A cannot cancel a
+nonzero integer, so its off-diagonal entries vanish too. This gives A=0,
+contradicting the nonzero outer-product definition.
+
+## Sharpness
+
+The four sign vectors (1,-1,-1), (1,-1,1), (1,1,-1), (1,1,1) have squares
+summing to 4I3 by entrywise addition. Their quarter frames give I3 in
+four terms. Their half frames give 2I3 in four terms; splitting one half
+into two identical quarters gives a five-term decomposition. Both
+denominator cutoffs require exponent two.
+
+Splitting one quarter of the first decomposition into two eighths gives
+I3 in five terms with exponent three. Splitting one quarter in the
+five-term 2I3 decomposition gives 2I3 in six terms with exponent three.
+Neither term limit can increase while retaining the claimed cutoff.
+These sign-square identities are classical Walsh/Hadamard identities.
+The new assertion is the uniform exclusion.
+
+## Consequence for short-word screening
+
+Consider at most eight frames with total sum 3I3 and a positional subset
+S summing to I3. Rational rank gives |S|>=3. Its complement sums to 2I3
+and has at least four terms, by a diagonal entry and the 1/2 entry bound.
+Thus |S|<=4, and the complement has at most five terms. The two statements
+show that every frame has exponent at most two.
+
+These requirements are weaker than a correct formal register word. In
+Maximooch's PR1679 model, the determinant gives total exponent 3I3. A
+nonzero I3 coefficient in the expanded endpoint requires a positional
+subset summing to I3. The new lemma therefore reduces these necessary
+screens to the half/quarter alphabet without enumerating projectors or
+bounding restored dirty roles.
+
+Tuafo's PR1628 already proves the nine-call endpoint floor for unrestricted
+rational frames. That floor is not a new result here. PR1679's finite
+exclusion may alternatively be cited after this reduction; its census
+is neither rerun nor independently certified by this package.

research/ternary-short-denominator-cutoff/README.md

@@ -0,0 +1,130 @@
+# Sharp denominator cutoffs for short ternary decompositions
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Scoped written proof with exact finite corroboration.** Each frame is
+`uv^T/2^j`, for nonzero `u,v in {-1,0,1}^3` and integer `j>=1`.
+Negative entries, arbitrary exponents and repetitions are allowed.
+
+- If at most four frames sum to `I3`, every exponent is at most two.
+- If at most five frames sum to `2I3`, every exponent is at most two.
+
+Both denominator cutoffs and both term limits are sharp. Quarter sign-square
+frames attain the first bound. Splitting one half sign-square frame gives
+a five-term attainer for the second. Splitting a quarter into two eighths
+disproves the respective five- and six-term extensions.
+
+The [proof](PROOF.md) uses deepest-numerator parity, diagonal and integer
+off-diagonal gaps, and positivity only in a forced full-sign-square case.
+It imposes no positivity assumption on the alphabet. The result is uniform
+in the exponent; a finite cutoff search is not its proof.
+
+## What this adds
+
+Any list of at most eight frames with total `3I3` and a positional subset
+summing to `I3` already lies in the half/quarter alphabet. These are the
+determinant and subset-support screens preceding scalar projector synthesis
+in Maximooch's [PR1679](https://github.com/CrocSwap/integer-mult-bounds/pull/1679).
+The cutoff explains why deeper dyadic denominators add no candidates to
+those necessary screens. Matrix decompositions need not realize an endpoint.
+
+PR1679 asks for denominator-independent elimination. Its finite-alphabet
+theorem and Tuafo's [PR1604](https://github.com/CrocSwap/integer-mult-bounds/pull/1604)
+are credited predecessors. Tuafo's [PR1628](https://github.com/CrocSwap/integer-mult-bounds/pull/1628)
+already proves the nine-call endpoint floor for unrestricted rational
+frames with arbitrary restored dirty workspace. **That floor is not new
+here.** No predecessor census, verifier, count or scientific receipt is
+replayed. The new contribution is the geometric cutoff and its screening
+consequence, with no new kappa or selected-frontier change.
+
+## Reproduce
+
+From the repository root, with the standard library and CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/ternary-short-denominator-cutoff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/ternary-short-denominator-cutoff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ternary-short-denominator-cutoff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ternary-short-denominator-cutoff --check-source-history
+```
+
+Another CPython 3.12 path can replace the displayed interpreter. Direct replay
+prints `PASS_TERNARY_SHORT_DENOMINATOR_CUTOFF` in a generated JSON receipt
+bound to all six package files by SHA256. It writes no files. The optional
+`--receipt /absolute/external/new-file.json` exclusively creates a receipt
+outside the package. No receipt is hand-authored or silently regenerated.
+
+The new checker covers eight exact gap inequalities, all 1,819 sorted
+exponent profiles of lengths one through four with exponents at most twelve,
+all 676 ordered nonzero ternary numerator pairs, 4,064 half-pair gap cases,
+256 forced positive-square cases and 15,872 five-term gap cases. The latter
+exercises 24 zero remainders requiring the nonzero-frame hypothesis.
+Another 192 literal attaining and term-limit counterexample decompositions
+cover all signed coordinate permutations of four fixtures. Twelve rejection
+controls exercise malformed frames, false sums and false denominator bounds.
+Both normal and optimized modes retain every mathematical check. These finite
+counts describe only this checker, not an enumeration of unbounded exponents.
+
+## Scope, provenance and limits
+
+The `bit-new-register-model` card is changed to a geometric screening theorem.
+The current baseline command `scripts/research_selected_baseline.py` passes
+source-binding orientation at canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. It is not a
+scientific replay. The connection to BIT exploration is the explicit infinite
+to finite denominator reduction before word synthesis. This side result
+supplies no changed native mechanism or better recursive moment. The first
+verified improvement is packaged without another construction round.
+
+Dimension three, ternary numerators, reciprocal powers of two, nonzero frames
+and the term limits are hypotheses. General rational weights, other targets,
+more terms and other dimensions are not covered. No native realization,
+physical caller, precision/tape, stock, compiler, outer transfer or complete
+multiplication theorem is established. No selected cold replay, predecessor
+scientific suite, Lean or Docker run was performed. Independent human and
+formal proof-kernel review are unclaimed.
+
+Source READMEs, catalogue and selected record are pinned historical provenance
+in [SOURCES.json](SOURCES.json). Direct replay has no external runtime inputs.
+Live PRs, recent claims, local reservations, distinctive main-tree searches
+and merged searches were checked. Cached overlap reports incomplete sparse
+local coverage; unsearched diffs and unpublished work remain limits.
+
+## Verifier constraints
+
+There is no recursion, subprocess, network, dynamic code execution or import
+of predecessor code. Functions are below 60 physical lines. Matrices have
+nine rational entries, sums have at most eight terms, the profile domain ends
+at twelve, and tested exponents end at 256. Each package file is bounded at
+128 KiB. Explicit exceptions preserve invariants under optimization.
+Warning-strict normal and optimized replay provide Python diagnostics.
+
+Power-of-ten rule 3 deviation: CPython allocates managed integers, Fractions
+and collections during this bounded one-shot check. The fixed domains above
+bound live mathematical data; no fixed-allocation or real-time claim is made.
+A fixed-allocation port would need a separate representation. Rule 9 deviation:
+the rejection helper calls exactly four local functions, `frame`, `check_sum`,
+`check_ceiling` and `matrix_sum`. Its twelve bounded controls exercise these
+targets and propagate unexpected exceptions.
+
+## Open next questions
+
+- What is the sharp exponent cutoff for five frames summing to `I3` or six
+  summing to `2I3`? Eighth-frame fixtures disprove the current cutoff.
+  Start with deepest-exponent multiplicities and remaining diagonal capacity;
+  additional cancellation patterns are unresolved.
+- Which unequal invertible ternary-dyadic target triples have a finite short
+  screening domain? Start with one named triple and its actual determinant
+  and subset equations. No entry-gap theorem for arbitrary targets is supplied.
+
+Structured first steps and blockers are in [TASK.json](TASK.json).
+
+## Credit
+
+Maximooch supplies PR1679's alphabet and denominator-elimination question.
+Tuafo supplies PR1604 and the stronger endpoint theorem PR1628. Ali Romman,
+woklerx, Cinna Davis, eumemic and huxint retain the register, rank and character
+lineage credited in those sources. Their files and credit lines are unchanged.
+Walsh/Hadamard identities, binary reduction, rank subadditivity and positive
+semidefinite comparison are classical; no literature-wide priority is claimed
+for those tools. The sharp denominator cutoffs are the new contribution.

research/ternary-short-denominator-cutoff/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bit-identical-three-targets-dirty/README.md",
+      "usage": "provenance",
+      "git_blob": "e07ca2f021415e467728be5363af7345d3a9e73c",
+      "sha256": "56cb21f6587673aef5cd4e4794f57cc6e4fd73c80e75625c48cb0d387cb3a7c6"
+    },
+    {
+      "path": "research/bit-quarter-ternary-catalyst/README.md",
+      "usage": "provenance",
+      "git_blob": "36f988ebfe61afe3dda5c59301e686264e947713",
+      "sha256": "1ba82c9228b38ab82f67444a94098f47860ba088ce636b58738425fe3584b780"
+    }
+  ]
+}

research/ternary-short-denominator-cutoff/TASK.json

@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp uniform exponent cutoff j<=2 for at most four nonzero ternary dyadic rank-one frames summing to I3 and at most five summing to 2I3; sharp denominator and term-limit fixtures and a finite-domain reduction of short-word determinant/subset screens.",
+  "scope_change_reason": "The unrestricted nine-call endpoint floor is already proved in PR1628. This contribution proves a separate geometric restriction on short matrix decompositions, prompted by PR1679, without auditing predecessor results or claiming a new endpoint floor.",
+  "bottleneck_link": "An infinite dyadic alphabet collapses to half/quarter frames under determinant and target-subset necessary screens for the specified short-word model. This is a scoped BIT screening side result, not a new supplier or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified denominator cutoff with sharpness fixtures; package the proof and checker without extending to larger term counts or other dimensions.",
+  "outcome": "completed",
+  "evidence": "PROOF.md uniform proof; verify.py generated hash-bound receipt, exact gap/profile/numerator checks, sharpness fixtures and rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the sharp exponent cutoff for five frames summing to I3 or six summing to 2I3?",
+      "why_it_matters": "Eighth frames show that quarter enumeration is no longer complete.",
+      "first_step": "Classify deepest-exponent multiplicities using remaining diagonal capacity.",
+      "blocked_by": "Additional cancellation patterns are not classified."
+    },
+    {
+      "question": "Which unequal invertible ternary-dyadic target triples have a finite short-decomposition screening domain?",
+      "why_it_matters": "The cutoff could remove infinite denominator searches before synthesis for a changed target contract.",
+      "first_step": "Choose one named triple and derive its determinant and positional subset equations.",
+      "blocked_by": "No uniform entry-gap bound is supplied for arbitrary targets."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "priority_revision": 8,
+    "checked_at": "2026-11-02T19:30:42Z"
+  },
+  "coordination": {
+    "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358910",
+    "question_source": "PR #1679",
+    "source_author": "Maximooch",
+    "known_stronger_endpoint": "PR #1628"
+  },
+  "environment": {
+    "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12",
+    "python_version": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "Python standard library only"
+  }
+}

research/ternary-short-denominator-cutoff/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": 60,
+      "checks": "New geometric cutoff gap/profile/numerator certificate, sharpness fixtures and rejecting controls, with generated source hashes."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The identical scientific certificate with Python optimization enabled."
+    }
+  ]
+}