[petalas]

Summary

Scoped written proof with exact finite corroboration. For nonzero ternary rank-one frames uv^T/2^j, j>=1, the sharp denominator cutoff is:

at most four terms summing to I3   => every j <= 2
at most five terms summing to 2I3  => every j <= 2

Both denominator cutoffs and both term limits are sharp. Explicit quarter-frame decompositions attain the bounds; one additional term permits eighths. The written proof is uniform in the exponent, with negative entries and repetitions allowed.

Consequently, at most eight frames with total 3I3 and a positional subset summing to I3 already lie in the half/quarter alphabet. This adds a geometric reduction of the infinite dyadic screening domain prompted by Maximooch's PR1679. The nine-call endpoint floor is already proved for unrestricted rational frames in Tuafo's PR1628, and is not claimed as new. No predecessor census or scientific result is audited or replayed.

Only research/ternary-short-denominator-cutoff/ is added. Advance claim. Canonical base 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8; upstream was refreshed before publication and remained at that base. The card scope is explicitly changed to this screening side result.

Evidence

• Before, PR1679 left denominator-independent elimination open. The unrestricted endpoint floor was already settled by PR1628.
• After, PROOF.md supplies the new denominator theorem and its sharp term boundaries. verify.py corroborates eight exact gap inequalities, 1,819 exponent profiles, 676 ordered ternary numerator pairs, 4,064 half-pair gap cases, 256 forced positive-square cases and 15,872 five-term gap cases. It checks 192 literal sharpness fixtures and twelve rejecting controls. These are the new checker's counts, not a recount of predecessor evidence.
• CPython 3.12.15 on macOS 27.0.1 arm64, standard library only. Warning-strict normal and optimized direct commands pass with identical generated source-hash-bound receipts. Each registered command was timed locally at about 0.09 seconds.
• Registered package replay, metadata/pins, committed bytes/modes and full declared source history pass at e3f1c9a60c08806672aab5408e5e0b58bd542a5b. Official six-file export and input coverage pass. Both modes also pass read-only, Git-free and with empty PATH; all seven export files, including its manifest, retain their bytes. Receipt controls reject an output inside the package and preserve an existing external file.
• AST compilation and the staged whitespace check pass. Every function is below 60 physical lines. Managed allocation and the four-function local rejection helper are bounded, documented runtime deviations.

From the repository root:

/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 --check-modes

Another CPython 3.12 path may replace the displayed local interpreter. Direct replay prints PASS_TERNARY_SHORT_DENOMINATOR_CUTOFF; registered replay prints PASS_REGISTERED_RESEARCH_PACKAGE.

Limitations

The dimension, ternary numerators, reciprocal dyadic weights, nonzero frames and term limits are hypotheses. The finite checker corroborates the written proof; it is not a proof-kernel certificate of unbounded exponents. General rational weights, other targets, longer sums and other dimensions remain outside scope. No new kappa, native implementation, physical caller, precision/tape, stock, compiler or outer transfer is established. Selected cold replay, predecessor scientific suites, Lean and Docker are unrun. Independent human and formal proof-kernel review are unclaimed.

Open next questions

• Determine the sharp cutoff for five terms summing to I3 or six summing to 2I3. Start with deepest-exponent multiplicities and remaining diagonal capacity. The new eighth-frame fixtures show why the present conclusion cannot simply extend.
• Identify one unequal invertible ternary-dyadic target triple with a finite short-screening domain. Derive its actual determinant and subset equations first; a uniform entry-gap argument for arbitrary targets is missing.

Related open work

The completion refresh inspected this account's open PRs created since the advance CLAIM. No additional open PR studying this same ternary short-decomposition denominator quantity was found, and no shared-instance numerical disagreement was identified. No extra computations audited another contribution. PR1679, PR1604 and PR1628 remain the merged predecessors. Cached sparse local coverage, unsearched diffs and unpublished work remain limits.

CI notes

Both hosted checks, plan and replay (research/ternary-short-denominator-cutoff), passed in run 41511709067 at exact head e3f1c9a60c08806672aab5408e5e0b58bd542a5b. The completed checks were read once. Separate run metadata confirms the matching head and successful completion. All registered scientific commands also passed locally. Hosted finite replay is not independent scientific acceptance or a proof-kernel verification of the written argument.

Merge danger

Door: two-way. Blast radius: isolated research package.

This contribution was produced by Nick Petalas. Credit Maximooch for PR1679's alphabet and denominator question; Tuafo for PR1604/1628; and Ali Romman, woklerx, Cinna Davis, eumemic and huxint for the retained formal-register lineage. Classical Walsh/Hadamard identities, parity, rank and positive-semidefinite methods retain their credit. Apache-2.0.