DONE: exact boundary for moving truncation across linear frames

[jmbarrancoidener]

DONE: PR #1466, head 8230e01b60d321ca10f2789e27cde037c40e6d6c. The finding and handoff give the proof, exact checks and limits. Scope released.

Original claim:

CLAIM

Question: For which complex linear maps A does componentwise truncation toward zero satisfy Q_p(Ax) = A Q_p(x) for every x? I will characterize this interface and test whether unitarity alone permits the source transform proof's truncation move.

Base: 410026d. Assignment: uniform-transfer-audit, scope key ce7411fb7cf6f3460bfc, nonce 581862d7c100f0437c6ea259a7deb687, priority revision 2. Source: upstream/build/sections/06-transforms.tex, eq:transform-truncate and the forward-round argument following eq:combined-twiddle. The retained source uses signed coefficient permutations and makes a valid restricted claim.

Method/domain: an all-dimension row classification over complex linear maps, exact rational witnesses, the source's signed negacyclic monomials, and a rational orthogonal Hadamard family with both compared exact inputs in the unit disk. Expected package: research/truncation-frame-transport with a written proof, standard-library verifier, source pins and rejection controls. This is a boundary audit, with no alleged source defect or new kappa.

Overlap: the full search at 2026-10-14 00:56 UTC covered 818 open PRs and 154 Discussion records with complete pagination. The existing synthetic-layout-independent package excludes Q_p truncation. PR1282 / Discussion1260 addresses exact signed-prefix norms and explicitly excludes roundoff; PR1255 concerns chart phases; PR1430 concerns Neumann accumulation. I will not repeat those results. No imported pending-PR code.

Stop rule: finish the classification, explicit scalar-phase and dimension-dependent counterexamples, source monomial controls, and a final overlap refresh within this session.

Claim expires: 2026-10-14T03:10:00Z.

Prepared for @jmbarrancoidener with substantial OpenAI Codex assistance, including a read-only source exploration subagent. This is not independent human review. Credit OpenAI's retained source and Douglas Colkitt's audit, plus the related contributors named above.

[jmbarrancoidener]

DONE: PR #1466, head 8230e01b60d321ca10f2789e27cde037c40e6d6c, on main 410026dc5513b87db92ae98571d1d5984c69a983.

For fixed p>=1, we prove that a complex linear map commutes with componentwise toward-zero truncation on every disk input exactly when each row is zero or selects one coordinate with phase 1, -1, i or -i. For square unitaries this is a Gaussian-unit monomial matrix. The source's signed-permutation step satisfies the criterion.

Two exact witnesses mark the boundary: phase (3+4i)/5 at p=1 changes a grid input 1/2 into 3/10+2i/5, whose component truncation is zero; a rational orthogonal Hadamard family gives (3/4)sqrt(n) grid units of discrepancy with both displayed arrays in the disk. We also prove the upper bound sqrt(2)2^-p(1+||A||_infinity). The square-root dimension dependence for general unitaries therefore has matching order.

Evidence: the registered Python 3.12.13 replay and optimized 3.14.6 replay produced identical JSON. We checked 2,401 rational rows, 4,784 constructed rejection witnesses, 372 source monomial cases, four Hadamard dimensions through 256, six weakened-contract controls and 4,096 guard-width cases. Package pins, selected-record integrity and whitespace checks passed. The final complete overlap refresh covered 824 open PRs and 159 Discussion records; main and nearby heads remained unchanged.

Scope: a written boundary theorem with exact finite evidence. We report no production defect, new kappa, full cold replay, Lean proof, hosted-CI success or independent human review. A researcher can investigate restricted reachable states or pay a separate rounding budget for a concrete replacement frame. Physical implementation, wider arithmetic and dirty restoration remain open for such a candidate. The package contains the proof, exact sources, commands and bounded next question.

Credit OpenAI's retained source, Douglas Colkitt, Philipp (@mightyOil), Gareth Davidson's PR1282/1255, Hanson Sun's PR1430, Artus Krohn-Grimberghe's PR371, and the retained transform lineage. Prepared for @jmbarrancoidener with substantial OpenAI Codex assistance and a read-only source exploration subagent. Scope released.