From e3f1c9a60c08806672aab5408e5e0b58bd542a5b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 19:36:25 +0000 Subject: [PATCH] feat(research): prove sharp ternary denominator cutoffs --- .../ternary-short-denominator-cutoff/PROOF.md | 104 ++++++++ .../README.md | 130 ++++++++++ .../SOURCES.json | 30 +++ .../TASK.json | 87 +++++++ .../VERIFY.json | 34 +++ .../verify.py | 227 ++++++++++++++++++ 6 files changed, 612 insertions(+) create mode 100644 research/ternary-short-denominator-cutoff/PROOF.md create mode 100644 research/ternary-short-denominator-cutoff/README.md create mode 100644 research/ternary-short-denominator-cutoff/SOURCES.json create mode 100644 research/ternary-short-denominator-cutoff/TASK.json create mode 100644 research/ternary-short-denominator-cutoff/VERIFY.json create mode 100644 research/ternary-short-denominator-cutoff/verify.py diff --git a/research/ternary-short-denominator-cutoff/PROOF.md b/research/ternary-short-denominator-cutoff/PROOF.md new file mode 100644 index 0000000000..998b4985ee --- /dev/null +++ b/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. diff --git a/research/ternary-short-denominator-cutoff/README.md b/research/ternary-short-denominator-cutoff/README.md new file mode 100644 index 0000000000..d0dab2ceeb --- /dev/null +++ b/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. diff --git a/research/ternary-short-denominator-cutoff/SOURCES.json b/research/ternary-short-denominator-cutoff/SOURCES.json new file mode 100644 index 0000000000..3f2dbb7d97 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/ternary-short-denominator-cutoff/TASK.json b/research/ternary-short-denominator-cutoff/TASK.json new file mode 100644 index 0000000000..633c73d95a --- /dev/null +++ b/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" + } +} diff --git a/research/ternary-short-denominator-cutoff/VERIFY.json b/research/ternary-short-denominator-cutoff/VERIFY.json new file mode 100644 index 0000000000..330c86a33c --- /dev/null +++ b/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." + } + ] +} diff --git a/research/ternary-short-denominator-cutoff/verify.py b/research/ternary-short-denominator-cutoff/verify.py new file mode 100644 index 0000000000..4b60258131 --- /dev/null +++ b/research/ternary-short-denominator-cutoff/verify.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the short-decomposition denominator proof.""" + +import argparse +from fractions import Fraction +import hashlib +from itertools import combinations_with_replacement, permutations, product +import json +from pathlib import Path + + +IDENTITY = tuple(int(i == j) for i in range(3) for j in range(3)) +SIGNS = tuple((1, a, b) for a, b in product((-1, 1), repeat=2)) +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def outer(u, v): + require(len(u) == len(v) == 3, "three coordinates required") + require(all(type(x) is int and x in (-1, 0, 1) for x in (*u, *v)), + "ternary coordinates required") + require(any(u) and any(v), "nonzero vectors required") + return tuple(x * y for x in u for y in v) + + +def frame(u, v, exponent): + require(type(exponent) is int and 1 <= exponent <= 256, + "finite checker exponent must be in 1..256") + return tuple(Fraction(x, 1 << exponent) for x in outer(u, v)) + + +def matrix_sum(matrices): + require(1 <= len(matrices) <= 8, "finite checker term limit exceeded") + require(all(len(a) == 9 for a in matrices), "3 by 3 matrices required") + return tuple(sum(a[i] for a in matrices) for i in range(9)) + + +def check_sum(matrices, multiple): + require(matrix_sum(matrices) == tuple(multiple * x for x in IDENTITY), + "incorrect literal decomposition") + + +def check_ceiling(exponents, ceiling): + require(all(j <= ceiling for j in exponents), "denominator ceiling exceeded") + + +def arithmetic_certificate(): + require(3 * Fraction(1, 8) + Fraction(1, 2) < 1, "three deepest terms fit") + require(2 * Fraction(1, 8) + 2 * Fraction(1, 4) < 1, "two quarters fit") + require(2 * Fraction(1, 8) + Fraction(1, 2) + Fraction(1, 4) == 1, + "mixed case does not saturate every diagonal") + require(2 * Fraction(1, 16) + Fraction(1, 2) + Fraction(1, 4) < 1, + "mixed case can have a deeper exponent") + require(2 * Fraction(1, 8) < Fraction(1, 2), "half-grid gap failed") + require(Fraction(9, 2) > 3, "positive half square fits under the identity") + require(3 * Fraction(1, 2) + Fraction(1, 4) + Fraction(1, 8) < 2, + "five-term complement gap failed") + require(Fraction(1, 8) < 1, "integer off-diagonal gap failed") + return 8 + + +def denominator_profiles(): + checked = 0 + surviving = [] + for length in range(1, 5): + for js in combinations_with_replacement(range(1, 13), length): + checked += 1 + if js[-1] < 3 or js.count(js[-1]) == 1: + continue + if sum(Fraction(1, 1 << j) for j in js) < 1: + continue + require(js == (1, 1, js[-1], js[-1]) or js == (1, 2, 3, 3), + "unclassified deep denominator profile") + surviving.append(js) + expected = [(1, 1, j, j) for j in range(3, 13)] + [(1, 2, 3, 3)] + require(sorted(surviving) == sorted(expected), "profile coverage differs") + return checked, len(surviving) + + +def binary_leading_terms(): + vectors = tuple(v for v in product((-1, 0, 1), repeat=3) if any(v)) + checked = 0 + full_diagonal = set() + for u, v in product(vectors, repeat=2): + a = outer(u, v) + require(any(x % 2 for x in a), "unique deepest numerator vanished") + if all(a[i] == 1 for i in (0, 4, 8)): + require(u == v and all(u), "positive full diagonal is not a square") + full_diagonal.add(a) + checked += 1 + require(full_diagonal == {outer(w, w) for w in SIGNS}, + "full-diagonal square classification differs") + return checked, len(full_diagonal) + + +def half_pair_obstructions(): + checked = 0 + for u, v in product(SIGNS, repeat=2): + a = matrix_sum((frame(u, u, 1), frame(v, v, 1))) + residual = tuple(t - x for t, x in zip(IDENTITY, a, strict=True)) + require(all(x.denominator == 1 for x in residual), "integer gap lost") + require(max(map(abs, residual)) >= 1, "two rank-one halves became I3") + for exponent in range(3, 257): + require(max(map(abs, residual)) > Fraction(2, 1 << exponent), + "deep pair can cover the residual") + checked += 1 + return checked + + +def mixed_case_obstructions(): + checked = 0 + for u, v, w, z in product(SIGNS, repeat=4): + a = matrix_sum((frame(u, u, 1), frame(v, v, 2), + frame(w, w, 3), frame(z, z, 3))) + quadratic = sum(u[i] * a[3 * i + j] * u[j] + for i in range(3) for j in range(3)) + require(quadratic >= Fraction(9, 2), "positive square contribution lost") + require(quadratic > sum(x * x for x in u), "mixed identity escaped") + require(a != IDENTITY, "false mixed-case exclusion") + checked += 1 + return checked + + +def five_term_obstructions(): + checked = 0 + zero_remainders = 0 + for vectors in product(SIGNS, repeat=4): + a = matrix_sum(tuple(frame(v, v, 1) for v in vectors)) + residual = tuple(2 * t - x for t, x in zip(IDENTITY, a, strict=True)) + require(all(x.denominator == 1 for x in residual), "four-half sum not integral") + if not any(residual): + zero_remainders += 1 + else: + require(max(map(abs, residual)) >= 1, "nonzero integer gap lost") + for exponent in range(3, 65): + require(not any(residual) or max(map(abs, residual)) > Fraction(1, 1 << exponent), + "deep frame can cover the complement residual") + checked += 1 + require(zero_remainders > 0, "zero-residual branch was not exercised") + return checked, zero_remainders + + +def attainers(): + checked = 0 + for permutation in permutations(range(3)): + for signs in product((-1, 1), repeat=3): + vectors = tuple(tuple(signs[i] * w[permutation[i]] for i in range(3)) + for w in SIGNS) + quarter = tuple(frame(w, w, 2) for w in vectors) + half = tuple(frame(w, w, 1) for w in vectors) + check_sum(quarter, 1) + check_sum((*half[:3], quarter[3], quarter[3]), 2) + eighth = frame(vectors[3], vectors[3], 3) + check_sum((*quarter[:3], eighth, eighth), 1) + check_sum((*half[:3], quarter[3], eighth, eighth), 2) + checked += 4 + return checked + + +def rejects(function, *args): + try: + function(*args) + except ValueError: + return 1 + raise ValueError("a false boundary was accepted") + + +def rejection_controls(): + w = SIGNS[0] + quarter = tuple(frame(v, v, 2) for v in SIGNS) + count = rejects(frame, (0, 0, 0), w, 2) + count += rejects(frame, (2, 0, 1), w, 2) + count += rejects(frame, (1, 1), w, 2) + count += rejects(frame, w, w, 0) + count += rejects(frame, w, w, True) + count += rejects(frame, w, w, 257) + count += rejects(check_sum, quarter[:3], 1) + count += rejects(check_sum, (*quarter[:3], frame(w, w, 3)), 1) + count += rejects(check_ceiling, (2, 2, 2, 2), 1) + count += rejects(check_ceiling, (2, 2, 2, 3, 3), 2) + count += rejects(check_ceiling, (1, 1, 1, 2, 3, 3), 2) + count += rejects(matrix_sum, ()) + return count + + +def run(): + return { + "status": "PASS_TERNARY_SHORT_DENOMINATOR_CUTOFF", + "claim_type": "scoped written proof with exact finite corroboration", + "arithmetic_inequalities": arithmetic_certificate(), + "denominator_profiles": denominator_profiles(), + "ternary_numerator_pairs": binary_leading_terms(), + "half_pair_gap_checks": half_pair_obstructions(), + "mixed_square_obstructions": mixed_case_obstructions(), + "five_term_gap_checks": five_term_obstructions(), + "sharp_attaining_decompositions": attainers(), + "rejecting_controls": rejection_controls(), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + result = run() + root = Path(__file__).resolve().parent + hashes = {} + for name in FILES: + path = root / name + require(path.stat().st_size <= 128 * 1024, "package file exceeds checker bound") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + result["sha256"] = hashes + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.receipt is not None: + target = args.receipt.resolve() + require(root not in target.parents, "receipt must remain outside the package") + with target.open("x", encoding="utf-8") as stream: + require(stream.write(encoded) == len(encoded), "incomplete receipt write") + print(encoded, end="") + + +if __name__ == "__main__": + main()