[petalas]

Summary

Prove an exact tariff for a concrete real-linear escape from complex-linear frame changes. For real orthogonal P,Q, the map T(x+iy)=Px+iQy needs exactly rank(P-Q) single-coordinate conjugations when arbitrary invertible complex-linear frames are free. Any finite number of exactly restored dirty complex coordinates leaves the minimum unchanged. Rational P,Q have an attaining rational compiler with no square roots.

separate orthogonal frames P,Q
  -> r = rank(P-Q)
  -> r imaginary Householder reflections
  -> r coordinate conjugations, with explicit rational basis instructions
  -> complete endpoint T direct-sum identity on dirty coordinates

Claim type: scoped written proof with exact finite corroboration. This contribution was produced by Nick Petalas. Antilinear-part rank subadditivity and Cartan-Dieudonne-Scherk factorization are classical and credited in PROOF.md, including constructive reflection-factorization background. No literature-priority claim is made for those ingredients.

The model changes the free operations and the field of linearity: these are actual real-linear endpoints and complex-linear frames, rather than formal group-algebra register words. The original question is recorded in the advance CLAIM. Only research/real-imaginary-conjugation-tariff/ is added. The selected frontier is unchanged.

Evidence

Before, a proposal to change real and imaginary frames had no explicit tariff in this declared interface. After, an antilinear-rank lower bound matches the rational compiler for every real orthogonal pair. For P=I and Q=[[3/5,-4/5],[4/5,3/5]], the exact count is two, excluding one call even with arbitrary restored dirty workspace.

Local CPython 3.12.15, macOS 27.0.1 arm64, standard library only:

• 2,921 complete program fixtures cover 124,532 real endpoint entries and 22,136 emitted instructions. They include every ordered signed-permutation pair through dimension three, every dimension-four target with P=I, parameterized oblique rational/dirty fixtures, and dimension/coefficient boundaries.
• A separate 64-entry fixture transiently mixes active and dirty data through a nonreal complex-linear shear and restores the dirty endpoint.
• All 781 words of length zero through four over five generators agree with an independent 2-by-2 Gaussian determinant oracle.
• Nine invalid/unsupported inputs and three actual endpoint corruptions reject. All checks remain active under optimization.
• Warning-strict normal and optimized direct commands pass in 4.47 and 4.83 seconds respectively, with identical complete generated hash-bound receipts. The registered replay passes both commands. These are replay durations, not performance comparisons.
• Metadata/pins, AST/function-size/tabnanny checks, committed-byte/source-history preflight, official seven-file export integrity and a read-only Git-free optimized export replay with empty PATH pass. The portable receipt equals the complete working receipt.

From the worktree root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/real-imaginary-conjugation-tariff/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/real-imaginary-conjugation-tariff/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/real-imaginary-conjugation-tariff
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/real-imaginary-conjugation-tariff --check-source-history

Another CPython 3.12 interpreter may replace the local absolute path. Expected scientific marker: PASS_REAL_IMAGINARY_CONJUGATION_TARIFF. The finite checks corroborate the written proof; they do not supply its all-size quantifier.

Limitations and unrun obligations

The free frames are an optimistic accounting hypothesis. Their physical cost is unknown here. The rational constructor may use odd denominators, so it is not automatically a legal dyadic basis compiler. The executable compiler admits dimension at most eight, input entries at most 256 bits and guarded matrix-product entries at most 4,096 bits. Exceeding an executable guard is not a mathematical obstruction.

No actual P104 cut, productive target, native conjugation, coefficient delivery, physical basis/scalar bill, owned-storage schedule, precision/tape/stock proof, all-size supplier compiler or complete outer invoice is supplied. Arbitrary real-linear targets outside separate orthogonal P,Q are not classified. No predecessor result was audited or replayed. Selected cold replay, Lean, Docker, a rounded multiplier, independent human review and formal proof-kernel review were not run. All five selected framework assumptions remain. No new kappa is claimed.

Open next questions

1. Bind one actual producer/consumer using separate real and imaginary frames, and price every basis, conjugation, return and target change. Native delivery and a favorable complete signed invoice are missing.
2. Fix a physical coefficient ring and determine whether one reached rational P,Q pair admits an attaining program in that ring. Odd denominators in the displayed frames are an explicit blocker.

Related open work

• #6613 proves a formal monomial-group reflection tariff with scalar mixing. This uses actual real-linear maps, grants complex-linear frames and charges coordinate conjugation; ordinary displacement rank would give the wrong tariff here.
• #6403 prices normal targets in finite binary semilinear groups. This studies real orthogonal frame pairs over complex coordinates, with a different free-operation contract and no common numerical optimum.

Final refresh of this account's open PRs created since the CLAIM found no additional PR studying this exact coordinate-conjugation interface or computing the same tariff. The related open work above remains current. No newly inspected result supplies a conflicting common number.

Fresh object/general-form searches found no open PR on this exact coordinate-conjugation interface. Live claims and reservations were checked before commitment; canonical main remained 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, selected PR6030. Sparse notes, unpublished work and arbitrary historical diffs remain overlap limits.

CI notes

Hosted CI passed at head 6b4e4c89df212fe90dacaad66fad1e36060e04fa in run 41662584021. Both plan and replay (research/real-imaginary-conjugation-tariff) succeeded. The completed checks were read once, and run metadata confirms the same head and successful conclusion. The registered replay includes both warning-strict normal and optimized finite checks. All local checks and publication/export preflights listed above also passed.

Hosted success certifies the registered replay at this commit; it does not discharge the physical, supplier or all-size proof obligations stated above.

Merge Danger

Door: two-way. Blast radius: isolated. Seven new package files; no shared implementation, selected frontier, frozen source or predecessor credit is changed.