Abstract A nonzero real vector can be mapped to a unit vector by taking signed square roots of its normalized absolute coordinates. The associated rank-one projector retains relative magnitudes and signs while forgetting total mass and common sign. We apply this construction to an optimal residual and an optimal dual witness for a finite-dimensional minimum-distance problem in the sum norm. Their trace distance defines an alignment statistic. Complementary slackness gives a strict upper bound below one for every optimal pair, and characterizes the zero-distance case. Successive coordinate minimization selects a unique pair once a coordinate order is fixed. The construction is undefined at a zero residual; a separate convention assigns the statistic the value zero there. We give proofs, an explicit example, and a selection policy that uses the statistic only after primary residual comparisons. The accompanying numerical implementation and discrete Lean results have distinct, stated scopes. Why This Matters The paper distinguishes what its diagnostic inequalities measure from stronger claims that do not follow. Explicit definitions and counterexamples make the selection policy and its limits inspectable. Core Theorems The numbered propositions and proofs in the manuscript state their domains and hypotheses. The revision separates quotient residuals, input norms, discrete formal lemmas and numerical evaluations rather than treating them as equivalent. Formal Verification and Computational Artifacts The package includes source code, tests, a pinned standalone Lean project, an explicit declaration census and source-bound rendered files. The quick start gives commands for replay. Each formal result retains the scope described in the manuscript; test outcomes do not supply a theorem beyond that scope. Scope Boundaries and Non-Claims The real projector construction and strict primal-dual distance bound have prose proofs. Lean checks discrete integer and rational statements. Numerical vector evaluation does not establish optimality or compute the canonical selector. Reproduction See [quick_start.md](quick_start.md) for installation, tests, the Lean census, rendering and independent archive checks. The manuscript and documentation use CC-BY-4.0; reference software and tests use MIT. The renderer, Lua filter and path helperretain Apache-2.0; see the component table in README.md. Related Identifiers and Citations Verified scholarly sources are listed in [references.md](references.md).The new revision has no assigned DOI. The previous record is [10.5281/zenodo.20192297](https://doi.org/10.5281/zenodo.20192297); its verified parent is [10.5281/zenodo.20192296](https://doi.org/10.5281/zenodo.20192296). The metadata records these version relationships.
Abstract A nonzero real vector can be mapped to a unit vector by taking signed square roots of its normalized absolute coordinates. The associated rank-one projector retains relative magnitudes and signs while forgetting total mass and common sign. We apply this construction to an optimal residual and an optimal dual witness for a finite-dimensional minimum-distance problem in the sum norm. Their trace distance defines an alignment statistic. Complementary slackness gives a strict upper bound below one for every optimal pair, and characterizes the zero-distance case. Successive coordinate minimization selects a unique pair once a coordinate order is fixed. The construction is undefined at a zero residual; a separate convention assigns the statistic the value zero there. We give proofs, an explicit example, and a selection policy that uses the statistic only after primary residual comparisons. The accompanying numerical implementation and discrete Lean results have distinct, stated scopes. Why This Matters The paper distinguishes what its diagnostic inequalities measure from stronger claims that do not follow. Explicit definitions and counterexamples make the selection policy and its limits inspectable. Core Theorems The numbered propositions and proofs in the manuscript state their domains and hypotheses. The revision separates quotient residuals, input norms, discrete formal lemmas and numerical evaluations rather than treating them as equivalent. Formal Verification and Computational Artifacts The package includes source code, tests, a pinned standalone Lean project, an explicit declaration census and source-bound rendered files. The quick start gives commands for replay. Each formal result retains the scope described in the manuscript; test outcomes do not supply a theorem beyond that scope. Scope Boundaries and Non-Claims The real projector construction and strict primal-dual distance bound have prose proofs. Lean checks discrete integer and rational statements. Numerical vector evaluation does not establish optimality or compute the canonical selector. Reproduction See quick_start.md for installation, tests, the Lean census, rendering and independent archive checks. The manuscript and documentation use CC-BY-4.0; reference software and tests use MIT. The renderer, Lua filter and path helperretain Apache-2.0; see the component table in README.md. Related Identifiers and Citations Verified scholarly sources are listed in references.md.The new revision has no assigned DOI. The previous record is 10.5281/zenodo.20192297; its verified parent is 10.5281/zenodo.20192296. The metadata records these version relationships.
For the canonical product MUB triple {Z₂ ⊗ Z₃, X₂ ⊗ Q₀, Y₂ ⊗ Q₁} in dimension six, known to admit no vector unbiased to all three bases, we prove an exact two-sided theorem for the projector-space feasibility functional f, where f(v) = 1 would characterize a candidate fourth unbiased vector. We show that the global maximum of f is W = (88 + 3√6) / 100 ≈ 0.9534846923. The bound is attained by an explicit algebraic unit vector, verified entirely in exact arithmetic over the field Q(ζ₂₄, √5). Its symmetry orbit contains 72 distinct maximizing rays. The matching global upper bound f ≤ W is established via an exact positive-semidefinite certificate at the level-2 Veronese lift. The certificate consists of a symmetric matrix over Q(√2, √3), whose polynomial identity and positivity are machine-verified in exact arithmetic and closed deterministically under the triple's 432-element symmetry group. No randomized computation or floating-point arithmetic appears anywhere in the proof chain. We further prove, via exact separating functionals, that degree-4 and degree-6 sum-of-squares certificates do not exist. In this precise sense, the lift level employed is minimal and necessary. Companion results include: • an exact product-vector ceiling for aligned product triples; • the exact wall value for the second known triple; • a complete Weyl-board census in dimension six, together with a Lean 4 kernel-verified combinatorial layer. These results completely characterize the pinned canonical triple. They do not resolve the MUB(6) problem, which remains open. The deposit contains two files: (1) the manuscript (PDF); (2) a complete verification bundle (ZIP; 91 files) containing all computational modules, tests, evidence receipts, execution logs, a SHA-256 manifest, and a minimal independent verifier (verify_global_certificate.py). The verifier is implemented in standard-library-only Python, shares no code with the certificate-construction pipeline, loads the stored exact certificate matrix, and independently re-establishes both directions of the global bound in approximately 150 seconds. Reproduction is available via: make verify-global Code is released under the Apache License 2.0 (with SPDX headers throughout the bundle). The manuscript text is released under CC BY 4.0. This research made extensive use of AI systems for conjecture generation, computation, proof drafting, and adversarial review. However, no mathematical claim depends on the correctness of any AI system. Every reported result is verified by exact rational arithmetic, exact interval arithmetic, or the Lean 4 kernel, and all verification artifacts are included in the deposit.
A partial-transpose image of the positive-semidefinite cone supplies an established alternative ordered presentation on a fixed composite carrier. Transporting both the cone and the processes preserves an abstract equivalence, whereas fixing the process representation can discriminate the two orders. We study the iteration of one specified right-argument transpose rule on supplied finite qubit carriers. With three standard leaves, its two bracketings have different cones, so no linear identification fixing every product operator pointwise can make them agree. Subset-orientation labels give an explicit repair. Relative to a separately supplied tensor-closed standard process category, we construct the raw tensor of arrows, associator, symmetry, asymmetric unit maps, and quasi-inverse tensorator, and prove symmetric monoidal equivalence by faithful transport. Complementary subsets define the same isolated cone, but their identification is not a congruence for the raw tensor product. At fixed rank, a precisely defined two-lift groupoid is a split central Z₂ extension; its odd lift is not an ordinary completely positive endomorphism at fixed representatives. A five-qubit example then separates matched reference transport, a fixed calibrated anchor, and an effect-based quotient. The latter loses a linear subspace rather than only a two-point transpose orbit and is preserved only by histories satisfying the standard kernel-invariance condition. A named real local unitary connects the anchor pair, while a real controlled-NOT (CNOT) gate exposes the limitation of an enlarged single-anchor history class. The contribution is an assumption-controlled analysis of one finite composition rule and its interfaces, not a new general coherence, orientation, or resource theorem, and not a derivation of quantum theory from primitive complementarity. Selected supporting statements and finite witnesses are accompanied by a partial Lean 4.19.0 formalization. A recorded local build and type/axiom audit accepted 117 theorem declarations and 57 definitions or abbreviations. The full symmetric monoidal category and equivalence in Theorems 4.5 and 4.6, and other explicitly listed manuscript links, remain incompletely formalized. The public source supplement also includes three preserved exact Python implementations, expected results, pinned dependencies and claim-to-code maps. Packaging and source/log audits are not another Lean compiler run or external peer review. The public evidence selection preserves the successful type/axiom output and the failure/success chronology. Machine-local account paths are omitted from derived run summaries, and one failed-build diagnostic has an explicitly normalized home-directory prefix. Accepted Lean proof sources remain unchanged; private review archives and original machine-local receipts are not public upload files.
This record contains a technical note on a conditional derivation of the quadratic Born density from a minimal two-cell structural mixing condition. The article starts from a Hilbert-space representation of states and assumes that event weights admit a local gauge-invariant pointwise modulus density. It then adds one structural invariance condition: the total weight of two equal cells is unchanged under a real rotation mixing their amplitudes. Under these assumptions, the local density is forced to be quadratic, f(r) = cr², yielding the usual Born weight after normalization. The result is not presented as a replacement for Gleason-type or decision-theoretic derivations of the Born rule. Its purpose is narrower: to isolate a simple local route by which the square law follows once the density form and a minimal two-cell basis-independence principle are granted. The functional-equation core and the two-cell reduction have been formalized in Lean 4 using Mathlib. The accompanying Lean development is archived separately at Zenodo: https://doi.org/10.5281/zenodo.20528721. The reported axiom footprint for every formalized theorem in the development, including the measure-theoretic born_density and born_rule_weight, is the standard classical Lean base, with no admitted steps (sorryAx) in any of the formalized theorems. The manuscript and the accompanying Lean development were prepared with extensive AI assistance. The author reviewed, selected, corrected, and revised the outputs and remains responsible for the final text, the mathematical claims, the Lean formalization, and the interpretive framing.
This compendium presents four revised studies of deterministic computation, reusable intermediate results, and transformation invariants in belief-propagation diagnostics and quantum error-correction software. It connects earlier QSOL-IMC preprints with commit-pinned QEC source snapshots, reproducible experiments, and machine-checked mathematical models. The four studies examine baseline equivalence between min-sum decoding and unit-weight uniformly reweighted belief propagation; trace-indexed reuse of sign vectors and CRC32 values; the interaction of clipping, damping, freezing, and ternary projection in decoder transformation pipelines; and the interpretation of local “dark-state” observables in belief-propagation traces. The deposit contains four revised papers, editable manuscript sources, a dependency-free Lean 4 project, source snapshots, validation scripts, measured results, proof logs, provenance records, and integrity manifests. The formalization comprises 43 compiled theorem declarations. Empirical validation includes 576 paired decoder cases, 80 cached-versus-inline diagnostic comparisons, a reproduced reduction from 81 to 20 sign computations, 204 selected historical tests, and 18 synthetic dark-state scenario runs. The analysis also documents counterexamples and boundary conditions involving CRC32 collisions, cache provenance, source mutation, damping, NaN handling, transformation order, and the distinction between observed local stability and safe computational reuse. The Lean proofs establish properties of the stated exact mathematical models. They do not constitute a complete refinement proof for the Python/NumPy implementations or IEEE-754 arithmetic, nor do they establish physical quantum-hardware correctness or justify skipping live-decoder updates. Historical runtime improvements are identified as previously reported results, separate from the measurements reproduced in this deposit.
This record contains the manuscript and complete verification artifact for the Bell inequality J62_4422 of Pál and Vértesi.It certifies the exact rational bracket750075557472719639 / 10^18 ≤ β_Q ≤ 750091086083765047288227625 / 10^27,and exact attainment of 3/4 by the stated two-qubit strategy. The lower endpoint is an exact rational strategy. The upper endpoint is certified by a sum-of-squares chain for the retained 365-word relaxation level.The Krawczyk certificate localizes the underlying KKT zero and establishes a strict local maximum, including negativity of the border form in all 256 boundary strata; it does not establish global optimality of that localized point. Accordingly, this work does not claim the exact quantum value, qubit-restricted optimality, minimum optimizer dimension, or global optimality of the localized KKT point.The archive includes SHA-256 manifests, standard-library replay programs, independently written certificate checks, mutation controls, and pinned full Krawczyk replays. The acceptance programs are fail-closed under optimized Python. The manuscript and certificates are licensed CC BY 4.0; verification code is licensed MIT.Version 1.1 is a hygiene-only update: it replaces one machine-local default path in a helper with the portable repository root ".", updates the corresponding checker and certificate source bindings, and leaves the mathematical calculation, inputs, claims, and replay outputs unchanged.
First preprint and reproducibility companion for bounded exact recovery of a nonzero trace-determinant tensor over an unknown binary extension field under corruption supported on a small common covector space. Includes the manuscript PDF and source, complete prose proofs, executable recovery and independent certificate checks, pinned partial Lean proofs, validation receipts, and three AI-model review reports with feedback dispositions. For s >= 2R+5, at most 8*2^(4R)*h trials return a verified compatible representation with probability at least 1-2^(-h). Accepted outputs are checked exactly; unique identification of a planted field is not claimed. The cubic-only bound does not establish the broader quantum application or a BPP/BQP result. Lean verification is partial. The complete recovery theorem, its probability and resource bounds, and the Python implementation are not fully formally verified. The reviews are AI-assisted internal reviews, not independent human peer review. Licenses: manuscript text and PDF are CC-BY-4.0; software and Lean sources are Apache-2.0. See LICENSE, LICENSES/CC-BY-4.0.txt and PROVENANCE.md. The package-level Other (Open) designation preserves these per-component licenses.