[petalas]

Result

Scoped proof in a formal register model (no new κ). For the four-role target diag([A+P],[A+Q],[B+P],[B+Q]) of PR #2085, extended by the fifth rational rank-one address R_t = (1,t)^T(1,t), the exact minimum number of paid calls is eight for every rational t.

At t = 1/2 this settles the seven-call case left open by PR #2112: its 7 ≤ min ≤ 8 becomes min = 8. It also answers #2085's open question for the whole slope family.

Proof outline (full proof in the package README):

1. Exponent support. Expanding ∏ (I+N_j) + [F_j]N_j shows every monomial has exponent equal to a subset sum of the labels, as rational matrices. So each target frame is a nonnegative sum of labels with multiplicities bounded by the label counts. With at most seven calls, R_t can enter such a sum only at t = 0 (exact enumeration over all rational t). For t ≠ 0, each of A, B, P, Q is therefore used.
2. Odd denominator. Λ_t/Λ has odd order, so L/2L is the old lattice mod 2 and R_t ≡ A or 0. The Research: exact rational frame floor on four roles #2085 rank/trace floor of 8 applies at every word length.
3. Even denominator. B ∈ 2Λ_t, and A, P, R_t give a basis mod 2. A word using R_t needs an even number (at least 2) of R_t calls, at least one B call by step 1, and at least 5 A/P/Q calls. The last bound is an exact minimum over all 65,536 masks. Total: 8. A word without R_t has the Research: exact rational frame floor on four roles #2085 floor of 8.

The direct eight-call word attains 8.

Evidence and reproduction

Package: research/bit-fifth-rational-frame-every-rational-t. From the repository root, using CPython 3.12 (~/git/integer-mult-bounds/.venv/bin/python3.12 locally):

python3.12 -I -B research/bit-fifth-rational-frame-every-rational-t/verify.py
python3.12 -B scripts/research_package.py --package research/bit-fifth-rational-frame-every-rational-t
python3.12 -B scripts/check_research_commit.py --package research/bit-fifth-rational-frame-every-rational-t --check-source-history

All three pass locally. The verifier takes about 0.5 s and prints:

PASS_FIFTH_RATIONAL_FRAME_EVERY_T_EXACT_MINIMUM_8 grid_odd=949 grid_even=482 support_exceptions=['0'] idempotents=120 odd_floor=8 even_visible_floor=5 even_total=8 mutated_visible_floor=3 direct_calls=8

It recomputes:

• every finite input: support exceptions, both first-order minima and the 120 idempotents;
• the parity classification of Λ_t/2Λ_t on 1,431 reduced slopes;
• the direct word, by exact multiplication in the group algebra.

Two controls must fail: dropping one call, and a mutated mask.

Limitations

• The general lattice classification (step 2/3) is a hand proof in the README. The grid check supports it but does not prove it. No proof-assistant verification.
• Only the one-parameter family R_t is covered. Scaled addresses c·R_t, other rank-one frames, two added frames and other targets are not covered.
• Formal paid-call model only: frame construction, additions, precision and interface charges are excluded. No supplier mapping or κ change.
• Research: rule out six-call saving from fifth rational frame #2112's six-call enumeration is cited, not rechecked. This proof does not depend on it.

Open next questions

• Can a scaled rational rank-one address c v^T v, or a pair of added frames, lower eight? First step: classify the addresses that can enter a target's exponent support within seven calls.
• Can exponent support plus the first-order floor decide other open minimum-length cases in torsion-free address models without word enumeration? The blocker is targets with several supports.

Related open work

No open PR studies this target or the R_t alphabet (rechecked after CI, including this account's #6037–#6039, which study other objects). The predecessors #2085 and #2112 are merged.

CI notes

Both hosted checks passed for head 3b098803eb854afbd5d63ad3bf4d75cdb1e515d5: plan and replay (research/bit-fifth-rational-frame-every-rational-t), run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40608029164.

Claim: #1166 (comment)

Produced by Nick Petalas. Model, target and the t = 1/2 instance credit Cinna Davis (1337isnot1337), #2085 and #2112.