[petalas]

Summary

Prove one diagonal sign conjugacy for every independent real body-sign profile of the fixed 20-factor Type A circuit in ToikY's #7439. Claim type: scoped computer-assisted proof with an exact character-ring certificate. No new κ.

E_jj = E_(18+j,18+j) = product_(r=1 to min(max(j-1,0),8)) D_r
T_i(D) = E(D) T_i(1) E(D)^(-1)       for every selected i

The earlier one-body gauge extends to all 17 simultaneous signs. Consequently the cited unit-body 19-factor witness transfers to every real body-sign profile. The predecessor's witness, minimum-length theorem and paid comparison are cited premises, not replay deliverables. The new result, proof and checkers were produced by Nick Petalas.

The package retains the exact literal caller from #7439 head ba83c9bebd99502cd64bb1cab2bc4e5336d9d7b2, originally supplied by rohanarun in #7113. It needs no foreign Git commit or network during replay. Credit ToikY for the selected circuit and real-body opening, rohanarun for the signed caller, Clear1nsight for #7334, and the retained P104/native lineage.

Card p104-side-correction changes scope to this body-sector interface. Base is canonical main e54523517d0f03e58352e647c403a5af3e525a57; selected #7000 remains unchanged. Live PRs, main, merged work and Discussion claims were checked before reservation and commit.

Evidence

• Before: Certify signed Type A factor circuits and gauge #7439 supplies the unit-body circuit and one D8=-1 gauge. After: the new exact rational sign-character calculation proves the common gauge for all independent signs, including every zero displacement entry.
• Primary result: 659 nonzero and 25,261 zero entries; six rejecting controls cover omitted host/idle bodies, incorrect gauges, a changed factor and changed source bytes. Both complete endpoints are checked over the same character ring.
• Separate numerical implementation: negative prefixes and literal suffix transport on 21 nonunit profiles, 544,320 entry comparisons, complete selected products on all basis columns, and 21 rejected factor omissions. It imports no executable predecessor or primary-checker code. Both implementations were produced by the same contributor.
• Registered replay, direct replay, optimized primary replay, AST compilation, whitespace checks, committed bytes/modes/source-history checks and a read-only Git-free exported replay pass. Exported receipts match the committed package's local receipts.
• CPython 3.12.15 on macOS 27.0.1 arm64. Registered commands took 0.111 s and 2.112 s locally, as replay-budget measurements, with 120-second limits each.

Exact reproduction from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-real-body-factor-gauge/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-real-body-factor-gauge/independent.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-real-body-factor-gauge
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-real-body-factor-gauge --check-source-history --check-modes

Use a local CPython 3.12 path on another machine. See research/p104-real-body-factor-gauge/PROOF.md for the exact claim and proof.

Limitations

Only the fixed normalized circuit, real body signs and central signs q=±1 are covered. Arbitrary complex bodies, imaginary central sectors, native host reuse, physical sign synthesis, ownership/restoration and complete pricing are unproved. No selected-supplier replay, independent human review, proof-kernel acceptance or complete multiplication theorem is claimed. The price obstruction in #7439 and fixed-frame host-reuse obstruction in #7457 remain intact.

Open next questions

• Extend the literal character calculation to fourth-root bodies and imaginary central signs; the real-sign simplifications and scalar relative-endpoint premise need replacement.
• Give one changed negative-prefix frame a physical host delivery while preserving its body, mate and ownership contracts, outside Bound fixed-frame reuse of signed Type A hosts #7457's fixed-frame obstruction. No favorable complete bill is supplied.

Related open work

• #7439 supplies the exact selected circuit and one-body gauge; this proves its common real-body-sign extension.
• #7457 excludes sufficient reuse under fixed old negative prefixes and unit bodies; this identity supplies no escape from that restriction.
• #7435 studies four-factor regrouping; this keeps the existing 20-factor selection.
• #7420 studies pair/triple regrouping in the same signed-factor model.
• #7419 bounds direct contiguous host replacement; no replacement is priced here.
• #7144 concerns nonnegative body retiming through a fixed skeleton, a different gauge contract.
• #7113 supplies the literal signed caller; its complete construction is a cited predecessor.
• #7334 supplies the native comparator; its invoice and κ are not recomputed here.
• #7309 excludes fixed-J QUERY/odd-idle edits; the present circuit is unchanged.
• #7310 studies one QUERY replacement with one changed J host.
• #7341 studies original-clock Type A QUERY caches; no cache is introduced here.
• #7342 gives a fixed-cut paired-QUERY correction with general formal bodies, a different target operator.
• #7343 bounds a rank-two host absorbing paired QUERY demotions.
• #7344 bounds retained-J phase-response top-ups; no top-up is supplied here.
• #7404 changes the stage-8 chronology and studies physical carriers; this uses the original caller.
• #7407 bounds that retimed stage-8 host.
• #7412 fixes J8/J9 ingress and egress after QUERY demotion.
• #7431 gives an imaginary-sector fixed-write obstruction, outside this real-sector identity.
• #7401 studies same-clock productive phase retirement; no phase is retired here.
• #7410 studies late-mask permutations at cut 1741; no mask is reassigned here.
• #7417 studies phase-sensitive J9 reassignment under a fixed host.
• #7399 bounds one projection replacing stage-8 singleton idles.
• #7440 bounds arbitrary-clock body-idle fusion; all old idles are retained here.
• #7398 studies fixed-paid rank-17 productive-root splits.
• #7316 studies fixed-paid rank-137 productive-root splits.
• #7405 studies Type B to Type A physical port conversion; the present statement is within Type A.

CI notes

CI did not certify this package. At unchanged head bbaac094a8368bcb49c586d95e2c7975ac43f119, run 43291118984, plan job 131437302165, failed in Onboarding helper tests. I read the job log: exactly one of 760 tests failed, with 24 skipped. The failing test is test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record, at tests/test_research_current_status.py:58. Its AssertionError says that 'make frontier7000-verify' is not found in the CI verification document, whose current section still describes #6030.

This mismatch exists in canonical main e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md still names #6030. Both files and the test are unchanged by this PR. I also read the failed-step logs of run 42905094314 and run 43291152300; each has the same single failing test, the same missing-command assertion, and FAILED (failures=1, skipped=24) after 760 tests.

The package replay job was skipped because plan failed. The successful package checks described above are local evidence only. No fix, retrigger commit or job rerun was made; the repository-level repair is left to maintainers.

Merge Danger

Door: two-way. This adds one isolated research package.

Blast Radius: package. Shared code, selected records and predecessor packages are unchanged.