[petalas]

Result

No κ claim and no word. The selected record is unchanged.

In the PR2085/2112 register model with three added signed rank-one frames, eight linear symmetries of the address space permute the old labels A, B, P, Q and the four targets. They carry the whole character table of a decomposition of one old-count profile to its image. Three results follow for the census in discussion comment 19377345.

1. (1,1,2,0)/(1,1,1) admits no seven-call word. It is the image of (2,0,1,1)/(1,1,1) under the map M -> W M W^T / 2, W = [[1,1],[1,-1]], which exchanges A with P and B with Q. Prove the (1,1,0,2) three-frame profile admits no seven-call word. #7051 names this profile as not settled.
2. The sixteen census profiles still open are three orbits, of sizes 8, 4 and 4. One argument per orbit is enough.
3. Twelve of those sixteen are not character-excluded. For the 8-orbit of (2,1,1,0)/(1,1,1) and the 4-orbit of (0,1,1,1)/(1,1,2) an explicit rank-one decomposition passes every additive character. The argument of Prove the (0,2,1,1) three-frame profile admits no seven-call word. #7013, Prove the (2,0,1,1) three-frame profile admits no seven-call word. #7035 and Prove the (1,1,0,2) three-frame profile admits no seven-call word. #7051 cannot be repeated there.

Orbit	Profiles	Status
O1	(1,1,1,1)/(1,1,1)	excluded by #6942
O2	(2,0,1,1), (0,2,1,1), (1,1,2,0), (1,1,0,2), all /(1,1,1)	excluded; (1,1,2,0) is new here
O3	eight profiles such as (2,1,1,0)/(1,1,1)	open; a character-surviving decomposition exists
O4	(0,1,1,1) and its three images, /(1,1,2)	open; a character-surviving decomposition exists
O5	the same four old profiles, /(1,1,1)	open; every box triple is character-excluded

The surviving decompositions are -B + (5/2)Q + (1/4)(1,3)(1,3)^T for (2,1,1,0)/(1,1,1) and (1/2)B + (1/2)(2,1)(2,1)^T + 2Q for (0,1,1,1)/(1,1,2). On each, all eight characters of the label lattice detect at least as many calls as targets. Both fail target support, so they are not candidate words.

Claim types

• Proof: the symmetry lemma and the transport lemma (PROOF.md, Sections 2 and 3).
• Scoped proof, conditional: the exclusion of (1,1,2,0)/(1,1,1). It uses the exclusion theorem of open PR Prove the (2,0,1,1) three-frame profile admits no seven-call word. #7035 (the theorem of open PR Prove the (1,1,0,2) three-frame profile admits no seven-call word. #7051 gives the same conclusion through the map P <-> Q) and the determinant and character premises of PR Prove eight-call floor for two arbitrary signed rank-one frames (no κ) #6190, Section 1. None of these is reproved or replayed here. Prove the (2,0,1,1) three-frame profile admits no seven-call word. #7035 and Prove the (1,1,0,2) three-frame profile admits no seven-call word. #7051 are open and unreviewed.
• Finite certificate: the two surviving decompositions with their full tables of eight characters, transported to all twelve profiles of O3 and O4.
• Bounded search, not a proof: box counts on frames spanned by the 24 primitive directions with entries of absolute value at most 4.

This is not a complete multiplication theorem.

Evidence and reproduction

Package research/three-frame-profile-orbits. CPython 3.12, standard library only, from the repository root. The interpreter used locally was ~/git/integer-mult-bounds/.venv/bin/python3.12.

python3.12 -B scripts/research_package.py --package research/three-frame-profile-orbits
python3.12 -B scripts/check_research_commit.py --package research/three-frame-profile-orbits --check-source-history
python3.12 -I -W error -B research/three-frame-profile-orbits/verify.py
python3.12 -I -O -W error -B research/three-frame-profile-orbits/verify.py

Observed locally:

OPEN_ORBIT_BOX (2,1,1,0)/(1,1,1) triples=1936 character_excluded=1854 character_surviving=82 support_passing=8 passing_both=0
OPEN_ORBIT_BOX (0,1,1,1)/(1,1,2) triples=5610 character_excluded=5225 character_surviving=385 support_passing=41 passing_both=0
OPEN_ORBIT_BOX (0,1,1,1)/(1,1,1) triples=1870 character_excluded=1870 character_surviving=0 support_passing=11 passing_both=0
PASS_THREE_FRAME_PROFILE_ORBITS group=8 compositions=35 census_orbits=5 open_profiles=16 open_orbits=3 four_call_orbits=8 new_profile_box=1914 transport_checks=11264 survivor_profiles=12 controls=6
PASS_REGISTERED_RESEARCH_PACKAGE research/three-frame-profile-orbits outcome=partial
PASS_RESEARCH_COMMIT_BYTES at 633774e4d9442ccd07f9e5138991d3ebb226547c

Both registered commands take about four seconds each.

The verifier checks, in exact rational arithmetic:

• the eight maps fix I, preserve the determinant, permute the labels and the targets, and act unimodularly on ZA + ZB + ZP;
• exactly 8 of the 24 label permutations extend to a linear map, and they are these eight;
• residual equivariance on all 35 four-call profiles and the four three-call profiles;
• the census orbits, of sizes 1, 4, 8, 4 and 4;
• the image A + B + 2Q of Prove the (2,0,1,1) three-frame profile admits no seven-call word. #7035's named decomposition 2B + P + Q, with its character that detects two calls and four targets;
• all 1914 box triples of (1,1,2,0)/(1,1,1) are character-excluded, directly on the new profile;
• both survivor tables, recomputed on each of the twelve profiles of O3 and O4;
• 11,264 comparisons of transported character tables over every census profile and every group element;
• six failure controls.

Limitations and unrun obligations

• The exclusion of (1,1,2,0)/(1,1,1) is conditional on the theorem of Prove the (2,0,1,1) three-frame profile admits no seven-call word. #7035 or Prove the (1,1,0,2) three-frame profile admits no seven-call word. #7051 and on the premises of Prove eight-call floor for two arbitrary signed rank-one frames (no κ) #6190, Section 1. Those proofs were not replayed.
• Sixteen census profiles stay open. O3, O4 and O5 are not settled.
• The survivors show that the character test alone does not exclude O3 or O4. They do not produce a word.
• The box counts are a search on 24 lines. They do not classify all rational decompositions, and decompositions with two parallel frames are outside the box.
• Four or more added frames are not treated.
• No Lean, Docker or selected cold replay was run. Independent human and formal proof-kernel review are unclaimed.

Open next questions

1. Is the six-call orbit O5, represented by (0,1,1,1)/(1,1,1) with R+S+T = diag(3,2), character-excluded? All 1870 box triples are. A proof would close four profiles. First step: run the parity-image argument of Prove the (2,0,1,1) three-frame profile admits no seven-call word. #7035 with 3 x1^2 + 2 x2^2 in place of 3 x1^2 + x2^2. Blocker: diag(3,2) has determinant 6, so the 2-adic case split has to be redone.
2. Does every decomposition of (2,1,1,0)/(1,1,1) fail a character or target support? In the box none of 1936 triples passes both. First step: describe the decompositions that pass every character, starting from the lattice Z^3 + Z(1/2,1/2,1/2) of the witness, and test the subset sums for A+Q on that family.
3. The same question for (0,1,1,1)/(1,1,2), where 385 box triples survive the characters and none passes target support.

Related open work

• Prove the (2,0,1,1) three-frame profile admits no seven-call word. #7035 (unpaidmoon) excludes (2,0,1,1)/(1,1,1). Its theorem is the input of the transported exclusion here. Its named decomposition 2B + P + Q is transported and checked.
• Prove the (1,1,0,2) three-frame profile admits no seven-call word. #7051 (unpaidmoon) excludes (1,1,0,2)/(1,1,1) and poses the question answered here. It maps to (1,1,2,0) under P <-> Q, so it gives the same conclusion independently of Prove the (2,0,1,1) three-frame profile admits no seven-call word. #7035.
• Prove the (0,2,1,1) three-frame profile admits no seven-call word. #7013 (unpaidmoon) excludes (0,2,1,1)/(1,1,1), the fourth profile of the same orbit. By the transport lemma the three exclusions Prove the (0,2,1,1) three-frame profile admits no seven-call word. #7013, Prove the (2,0,1,1) three-frame profile admits no seven-call word. #7035 and Prove the (1,1,0,2) three-frame profile admits no seven-call word. #7051 are images of one another.
• Prove five once-each rank-one frames miss the five-call endpoint. #7024, Classify length-6 support for five frames plus one old projector #7067, Classify six once-each signed frames: support, but no word #7076 and Prove four rank-one frames plus one old call miss length-5 support (no κ) #7083 (unpaidmoon) study four, five and six added frames. They are a different equation and are not used.
• Record a 21-shear one-scale zero-swap word for helper-462 (no κ) #7125, Prove rank factor 1 for every-stage paired-star gaps and raise the thin-rank bound to 2q⌈g/3⌉ (no κ) #7126 and Prove the E8 ports-per-dimension law N_e = 2^(e-2) + 4 in closed form (no κ) #7127, opened from this account after the claim for this PR, study helper-462 shear words, paired-star thin rank and E8 port counts. None of them concerns the three-frame count profiles, and no number is shared.

Credit

The register model is Cinna Davis's PR2085/2112 formal model. The determinant, support and character premises are the PR2910 package as recorded by apoursh in #6190. The census is discussion comment 19377345. The exclusions of (1,1,1,1), (0,2,1,1), (2,0,1,1) and (1,1,0,2) are unpaidmoon's #6942, #7013, #7035 and #7051. The symmetry lemma, the transported exclusion, the two surviving witnesses and the checker are produced by Nick Petalas.

CI notes

CI did not certify this package. At head 633774e4d9442ccd07f9e5138991d3ebb226547c, run 42906716667 failed in the plan job (job 130146489645), and the package replay job was skipped because plan failed. The evidence for this PR is the local runs listed above.

The plan failure is one test of 760 (24 skipped) in the "Onboarding helper tests" step:

FAIL: test_current_ci_section_matches_selected_record (test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record)
AssertionError: '`make frontier7000-verify`' not found in '# CI verification\n\n## Current selected-family replay: #6030 ...'
Ran 760 tests in 144.583s
FAILED (failures=1, skipped=24)

The cause is on main, not in this PR. At e54523517d0f03e58352e647c403a5af3e525a57, certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md is still headed "Current selected-family replay: #6030" and does not contain that command. This PR changes only files under research/three-frame-profile-orbits/.

The same single test is the only failure, with the same 760/24 counts and replay skipped, in five other runs from today that I read: 42905094314 and 42903313790 on other contributors' branches, and 42905202459 (#7125), 42905330981 (#7126) and 42905806694 (#7127). No fix or retrigger was pushed, and the job was not re-run.