Prove exact conjugation tariffs for separate complex frames (no κ)

research/real-imaginary-conjugation-tariff/CODE-BOUNDS.md

@@ -0,0 +1,42 @@
+# Executable bounds and inspection
+
+The retained artifact is one standard-library Python file. `compile_frames`
+is its public computational entry; the other matrix routines are internal to
+that entry or the fixed no-argument replay. The compiler validates both inputs,
+matching dimensions, exact rational types, coefficient sizes and orthogonality.
+Unsupported inputs fail with ValueError. Boolean and floating-point entries
+are rejected. Every mathematical check uses an explicit exception and remains
+active under optimized Python.
+
+There is no recursion. Compiler dimension is at most eight, reduction has at
+most eight iterations, and each iteration strictly decreases the independently
+checked displacement rank. There are at most 25 emitted instructions. Compiler
+matrix loops have at most eight iterations per dimension. Product outputs have
+at most 4,096 numerator/denominator bits. Reflection construction and elimination
+between those checks use a finite number of exact operations on bounded-size
+matrices; no claim of a practical public worst-case runtime is made.
+
+The replay has 2,921 fixed program fixtures, at most eight active-plus-dirty
+complex coordinates, real matrices at most 16-by-16, at most 25 instructions per
+fixture, and at most 16 elimination pivots. Its nonreal word corpus has exactly
+1+5+25+125+625 words, each of at most four steps. All other loops range over
+these finite dimensions, the 12 control cases, or the package's source files.
+The receipt inventories only package-local regular files. The replay writes
+nothing and owns no network connection, subprocess, random generator or lock.
+
+Power of Ten rule 3 deviation: CPython and Fraction allocate during operation.
+The fixed corpus, dimension limits and input/product bit guards bound live
+matrices; one program endpoint is retained at a time. There is no service loop,
+external state or retained history of the census. A native fixed-allocation
+implementation is a separate obligation. Python has no pointer arithmetic or
+preprocessor; the artifact uses direct named calls, no dynamic evaluation,
+code generation or callback dispatch. Ordinary exception propagation is the
+failure path. No shared repository implementation is changed.
+
+Functions are below 60 physical lines. The compiler checks nonzero normals,
+rational basis inverses, strict rank progress, exact termination and the tariff.
+The separate interpreter verifies full endpoint matrices, every prefix bound,
+returned dirty coordinates and an independent antilinear-rank calculation.
+Warning-strict normal and optimized runs, AST syntax/function-size inspection
+and tabnanny are the local diagnostics. No static type checker, native compiler
+or formal proof kernel is claimed. Registered replay repeats both strict modes.

research/real-imaginary-conjugation-tariff/PROOF.md

@@ -0,0 +1,155 @@
+# Exact conjugation tariff for separate real and imaginary frames
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof. Finite rational checks corroborate the
+construction. Independent human and formal proof-kernel review are unclaimed.
+
+## Contract and theorem
+
+Fix a positive integer n and real orthogonal n-by-n matrices P,Q. The target is
+
+    T(x+iy) = Px + iQy,       x,y in R^n arbitrary.
+
+There may also be any finite number s of arbitrary dirty complex coordinates.
+The complete endpoint must be T direct-sum I_s, including all dirty returns.
+Intermediate mixing with those coordinates is permitted.
+
+A program is a fixed finite sequence with these operations:
+
+- Any invertible complex-linear map on C^(n+s), at zero price in this model.
+- Conjugation of one coordinate z_j, leaving every other coordinate unchanged,
+  at unit price.
+
+No other real-linear, nonlinear, approximate, branching or irreversible
+operation is free. In particular, simultaneous conjugation of an arbitrary
+block is not one unit-price call.
+
+**Theorem.** The minimum paid-call count is exactly
+
+    rank_R(P-Q).
+
+It is independent of s. If P,Q are rational, an attaining program uses rational
+real matrices as its complex-linear maps. It requires no square roots and no
+dirty coordinates. The upper construction has r paid calls and 2r+1 displayed
+linear instructions, where r=rank(P-Q); adjacent linear instructions may be
+combined. This instruction count gives no physical scalar-cost bound.
+
+This is an exact tariff in the declared relaxation, not a lower bound on all
+possible real-linear provider alphabets or an admitted native supplier.
+
+## Lower bound from the antilinear part
+
+Every real-linear map S on C^d has a unique expression
+
+    S(z)=A_S z+B_S conjugate(z).
+
+Define b(S)=rank_C(B_S). For two such maps,
+
+    B_(S R) = A_S B_R + B_S conjugate(A_R).
+
+Rank subadditivity and the rank bound for a product imply
+
+    b(S R) <= b(S)+b(R).
+
+A complex-linear map has b=0. Single-coordinate conjugation has B=e_j e_j^t,
+so b=1. Consequently, any program with k paid calls has b(endpoint)<=k,
+irrespective of the number of dirty coordinates or intermediate mixing.
+
+For the required endpoint,
+
+    A = diag((P+Q)/2, I_s),
+    B = diag((P-Q)/2, 0_s).
+
+Its antilinear rank is rank_C(P-Q)=rank_R(P-Q). This proves the lower bound
+and the dirty-workspace assertion. It also proves additivity for independent
+direct-sum targets in this model. The last statement follows from the one
+theorem by choosing block-diagonal P,Q, rather than from a separate search.
+
+## A rank-tight rational reflection factorization
+
+Set R=P^t Q. Then R is real orthogonal and rank(I-R)=rank(P-Q). We give the
+classical Euclidean Householder reduction explicitly to specify the compiler.
+
+For a nonzero real v put H_v=I-2vv^t/(v^t v). Suppose R is not identity.
+Choose a coordinate e_j with Re_j != e_j and put v=Re_j-e_j. Since R preserves
+length, H_v Re_j=e_j. If f is fixed by R, then
+
+    f^t v = f^t R e_j - f^t e_j = (R^t f)^t e_j - f^t e_j = 0.
+
+Thus H_v also fixes every old fixed vector, and H_v R fixes e_j in addition.
+The new fixed space has dimension at least one larger. Conversely,
+
+    I-H_v R = (I-R)+(I-H_v)R
+
+differs from I-R by a rank-one matrix. Its rank can decrease by at most one.
+It therefore decreases by exactly one. Repeating terminates after exactly
+r=rank(I-R) steps, with
+
+    H_(v_r) ... H_(v_1) R = I,
+    R = H_(v_1) ... H_(v_r).
+
+All v_j and H_(v_j) are rational when R is rational. Positive definiteness
+ensures every nonzero v_j has v_j^t v_j>0. No assertion about arbitrary
+indefinite forms is used.
+
+## One coordinate conjugation per imaginary reflection
+
+Let J_v act by J_v(x+iy)=x+iH_v y. Choose an index k with v_k != 0. Define
+a rational real matrix S with first column v and, for every j != k, another
+column
+
+    u_j=e_j-(v_j/v_k)e_k.
+
+The u_j form a basis of v-perp, so S is invertible. Explicit inverse
+coordinates of a vector a are
+
+    c_0=(v^t a)/(v^t v),
+    c_j=a_j-v_j c_0,       j != k.
+
+Write C_0 for conjugation of coordinate zero. It fixes the real parts of all
+coordinates and flips only the imaginary part of coordinate zero. Therefore
+
+    S C_0 S^-1 (x+iy) = x+i S diag(-1,1,...,1) S^-1 y = J_v(x+iy).
+
+The identity follows because the displayed real matrix negates v and fixes
+v-perp. Each J_v costs exactly one paid call. Apply J_(v_r),...,J_(v_1)
+chronologically, then the free real matrix P. The result is
+
+    x+iy -> x+iRy -> Px+iPRy = Px+iQy.
+
+This uses exactly r conjugations and attains the lower bound. Extending each
+operation by identity supplies every s without using its dirty contents.
+
+## Discriminating two-coordinate example
+
+Take P=I_2 and
+
+    Q = [ 3/5  -4/5 ] = H_(-1,2) H_(0,1).
+        [ 4/5   3/5 ]
+
+Then rank(I-Q)=2. Conjugating the imaginary coordinates in the two displayed
+reflection bases, in reverse order, attains two calls. One call is impossible
+even with arbitrary complex-linear mixing and exactly restored dirty space.
+The complete real target has positive determinant, so orientation alone does
+not give this exclusion. Ordinary real displacement rank is not the right
+tariff either: multiplication by i is a free complex-linear map with
+rank_R(T-I)=2 and zero paid calls.
+
+## Attribution and scope
+
+Real-linear complex decomposition, rank subadditivity and the
+Cartan-Dieudonne-Scherk reflection method are classical. See
+[Rodriguez-Andrade, Aragon-Gonzalez, Aragon and Verde-Star, 2010](https://arxiv.org/abs/1011.1027)
+for constructive reflection factorization and minimum-length context. The
+reflection theorem itself and the antilinear-rank principle are not claimed
+as new. The contribution is their exact combined tariff, the explicit rational
+conjugation compiler and its dirty-workspace interface in this research model.
+No general literature-priority claim is made.
+
+The matrices P,Q need not commute. Free frames may be arbitrary complex-linear
+maps, although the attaining compiler uses real rational ones. Arbitrary
+real-linear targets outside the separate orthogonal P,Q contract are not
+classified. Conjugation delivery, the actual scalar/basis invoice, native
+frames, independent productive targets, all-size supplier compilation,
+precision, stock, tape movement and the outer multiplier are not provided.

research/real-imaginary-conjugation-tariff/README.md

@@ -0,0 +1,138 @@
+# Exact conjugation tariff for separate real and imaginary frames
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof with exact finite corroboration. For every
+positive n and real orthogonal n-by-n P,Q, the exact number of single-coordinate
+conjugations required for
+
+```text
+T(x+iy) = Px+iQy
+```
+
+is **rank(P-Q)** when arbitrary invertible complex-linear frames are free.
+Any finite number of exactly restored arbitrary dirty complex coordinates
+leaves this minimum unchanged. For rational P,Q, an explicit attaining
+compiler uses rational real frames and no square roots.
+
+[PROOF.md](PROOF.md) proves the all-size statement, its dirty-workspace lower
+bound and the rational construction. [verify.py](verify.py) implements that
+construction and a separate full real-matrix interpreter. This is a changed
+provider alphabet, rather than a new native supplier or a kappa improvement.
+
+The lower bound records the rank of the antilinear part of the complete map.
+Each paid conjugation increases it by at most one, while every free frame has
+zero antilinear part. Classical rank-tight Householder factorization attains
+the resulting bound. Those ingredients are credited below; the new scoped
+contribution is their exact tariff and explicit rational interface here.
+
+For example, P=I and Q=[[3/5,-4/5],[4/5,3/5]] need exactly two conjugations,
+even with dirty workspace and arbitrary complex-linear mixing. This excludes
+one-call realification of that pair. Positive real determinant alone would
+not exclude it. Conversely, the free map z->iz has real displacement rank two
+but needs no conjugation, so ordinary displacement rank is not this tariff.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and its standard library:
+
+```sh
+/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 path may replace the absolute interpreter. The direct
+commands print `PASS_REAL_IMAGINARY_CONJUGATION_TARIFF` inside generated JSON
+stdout receipts bound to every package file hash. They write no files. The
+registered and publication checks print `PASS_REGISTERED_RESEARCH_PACKAGE`
+and `PASS_RESEARCH_COMMIT_BYTES` respectively.
+
+The finite corpus contains:
+
+- All 2,372 ordered pairs of signed permutation matrices in dimensions one,
+  two and three, and all 384 dimension-four targets with P=I.
+- 162 parameterized rational fixtures in dimensions one through six, with
+  zero, one or two arbitrary dirty complex coordinates. These fixtures may
+  repeat a matrix pair; no distinct-pair count is claimed.
+- Three dimension/coefficient boundary fixtures, including dimension eight
+  and a reflection with 253-bit rational coefficients.
+- 124,532 full real endpoint entries across those 2,921 program fixtures,
+  covering 22,136 emitted instructions. Every prefix obeys its antilinear
+  call bound. A separate 64-entry fixture transiently mixes active data and
+  dirty coordinates using a nonreal complex-linear shear and restores them.
+- All 781 words of length zero through four over two conjugations and three
+  complex-linear generators. A separately evaluated 2-by-2 Gaussian
+  determinant agrees with the full real antilinear-rank oracle.
+- Twelve rejected cases: nine malformed or unsupported compiler inputs and
+  three actual endpoint corruptions, omitting a call, flipping a real part
+  instead of an imaginary part, and reversing instruction order.
+
+The rank oracles use independent elimination implementations. Complete real
+matrix identities establish arbitrary-input endpoints for each finite
+fixture; they do not extrapolate the theorem. Normal and optimized receipts
+must agree. The first complete local corpus ran in about five seconds on
+CPython 3.12.15, macOS 27.0.1 arm64. This is a replay duration, not a speedup.
+
+## Scope and current bottleneck
+
+The complex-new-helper-inventory card is explicitly changed to a real-linear
+interface side result. The selected source-binding positive control passed
+at canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8.
+The selected record is PR6030, kappa 0.003125804; older values in priority prose
+do not replace that record. [TASK.json](TASK.json) retains the complete card.
+
+A different real/imaginary frame cannot be supplied by complex-linear frames
+alone when P differs from Q. The theorem gives the exact remaining conjugation
+resource in this generous relaxation. It supplies no actual P104 cut, productive
+target or favorable complete recursive bill. Free frames are an accounting
+assumption, not a claim that physical basis work is free. The rational compiler
+can use odd denominators. A native or dyadic installation needs its own
+coefficient, scalar, access, lifetime and restoration argument.
+
+The logical identity, exact call tariff and rational frame constructor are
+proved. Native conjugation delivery, physical basis costs, chronology, owned
+storage, independent Gaussian targets, precision/tape, stock, uniform supplier
+compilation and outer funding are unknown here. No selected cold replay,
+predecessor scientific replay, Lean, Docker, native realization or rounded
+multiplier was run. All five selected framework assumptions remain. Independent
+human and formal proof-kernel review are unclaimed.
+
+[The advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376836)
+preceded substantial work. Live open/account PRs, recent handoffs, active
+Discussions, local reservations, general-form and distinctive main README
+searches, and merged PR searches were checked. The broader cache covered 141
+of 8,917 local note records, so it was supplemented by main-tree searches.
+These checks do not cover unpublished work or arbitrary historical diffs.
+No contributor's package or scientific checker is imported by the result.
+
+## Open next questions
+
+1. Can one actual complex supplier use separate real and imaginary frames at
+   a favorable complete bill? First name its literal producer and consumer,
+   and charge every basis, conjugation, return and target change. No native
+   delivery or full signed invoice is supplied here.
+2. Which rational frame pairs admit an attaining program in a required
+   physical coefficient ring? Fix that ring and examine the displayed bases
+   for one reached pair. Rational frames may have odd denominators.
+
+Structured versions, first steps and blockers are in [TASK.json](TASK.json).
+The first exact tariff is shipped without classifying more general real-linear
+maps or expanding into physical supplier construction.
+
+## Credit and executable bounds
+
+Antilinear decomposition and rank subadditivity are classical. The
+Cartan-Dieudonne-Scherk reflection method is classical; see
+[Rodriguez-Andrade, Aragon-Gonzalez, Aragon and Verde-Star, 2010](https://arxiv.org/abs/1011.1027)
+for constructive factorization context. The needed positive-definite reduction
+is proved explicitly in PROOF.md. No external code or proof text is copied,
+and no general literature-priority claim is made. Repository predecessors and
+their credit lines are unchanged.
+
+The public compiler accepts dimensions one through eight and integer/Fraction
+entries of at most 256 bits. Matrix-product outputs are guarded at 4,096 bits;
+exceeding an executable bound raises an error, not a mathematical impossibility.
+The written rational construction has no such limits. [CODE-BOUNDS.md](CODE-BOUNDS.md)
+records loop bounds, allocation deviations and diagnostics.

research/real-imaginary-conjugation-tariff/SOURCES.json

@@ -0,0 +1,31 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ],
+  "external_background": [
+    {
+      "url": "https://arxiv.org/abs/1011.1027v1",
+      "title": "An algorithm for the Cartan-Dieudonne theorem on generalized scalar product spaces",
+      "authors": [
+        "M.A. Rodriguez-Andrade",
+        "G. Aragon-Gonzalez",
+        "J.L. Aragon",
+        "Luis Verde-Star"
+      ],
+      "role": "Classical constructive reflection-factorization background. No code or proof text imported; PROOF.md proves the needed positive-definite rank-tight reduction explicitly."
+    }
+  ]
+}