This artifact documents a formally verified optimization in the QSOL-IMC Quantum Error Correction (QEC) framework (v68.4.1). The optimization exploits the algebraic identity that belief propagation decoding using uniformly reweighted min-sum with ρ=1.0 is bitwise identical to baseline min-sum decoding under IEEE 754 double-precision arithmetic. This invariant is proven analytically, validated across all decoder schedules, and confirmed via bitwise equality tests. The optimization removes redundant benchmark computation by reusing baseline results for the ρ=1.0 case without altering outputs, convergence behavior, or test coverage. A secondary improvement eliminates repeated reconstruction of derived data structures through deterministic precomputation. The full test suite (3779 tests) remains unchanged and passes completely. The optimization reduces preview sweep runtime by approximately 43% and overall runtime by approximately 7.6%. This artifact includes formal proof, execution-path validation, safety analysis, and reproducibility guarantees, and serves as a reference for invariant-driven optimization in deterministic QEC benchmarking systems.
This artifact documents a formally verified optimization in the QSOL-IMC Quantum Error Correction (QEC) framework (v68.4.1). The optimization exploits the algebraic identity that belief propagation decoding using uniformly reweighted min-sum with ρ=1.0 is bitwise identical to baseline min-sum decoding under IEEE 754 double-precision arithmetic. This invariant is proven analytically, validated across all decoder schedules, and confirmed via bitwise equality tests. The optimization removes redundant benchmark computation by reusing baseline results for the ρ=1.0 case without altering outputs, convergence behavior, or test coverage. A secondary improvement eliminates repeated reconstruction of derived data structures through deterministic precomputation. The full test suite (3779 tests) remains unchanged and passes completely. The optimization reduces preview sweep runtime by approximately 43% and overall runtime by approximately 7.6%. This artifact includes formal proof, execution-path validation, safety analysis, and reproducibility guarantees, and serves as a reference for invariant-driven optimization in deterministic QEC benchmarking systems.
This document presents a formally verified optimization within the QSOL-IMC Quantum Error Correction (QEC) framework (v68.4.1). The optimization exploits an algebraic invariant in belief propagation decoding: URW(min-sum, ρ = 1.0) ≡ baseline min-sum This equivalence is proven analytically, validated across all decoder schedules, and confirmed via bitwise identity checks under IEEE 754 double-precision arithmetic. Leveraging this invariant enables elimination of redundant computation in benchmark sweeps without altering outputs, convergence behavior, or test coverage. A secondary optimization removes repeated reconstruction of derived data structures through deterministic precomputation. The full test suite (3779 tests) remains unchanged and passes completely. The optimization yields a 43% reduction in preview sweep runtime and a ~7.6% overall runtime reduction. Scope. This document covers invariant validation and test-suite optimization only. No algorithmic changes to decoding behavior are introduced.
This document presents a formally validated optimization within the QSOL-IMC Quantum Error Correction (QEC) framework (v68.5.0). The optimization exploits a data-level invariant in belief propagation (BP) dynamics diagnostics: sign vectors and their derived CRC32 signatures are pure, deterministic functions indexed solely by trace position. This invariant enables elimination of redundant computation across multiple diagnostic metrics through trace-level precomputation and reuse. The invariant is proven via slice-level equivalence, byte-level identity, and purity arguments, and validated with deterministic instrumentation. The full test suite remains unchanged and passes completely. The optimization reduces redundant sign computations by 75.3% within BP dynamics analysis while preserving bitwise identity, convergence behavior, and reproducibility guarantees. Scope. This document covers invariant validation and diagnostic-layer optimization only. No algorithmic changes to decoding behavior are introduced.
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 work introduces QEC, a deterministic, replay-safe reasoning system for quantum error correction and invariant-driven computation. Unlike conventional adaptive systems that rely on stochastic exploration, QEC operates as a deterministic reasoning layer over system evolution, producing proof-carrying state transitions that are fully reproducible and verifiable. The system replaces probabilistic optimization with a structured pipeline of invariant detection, deterministic control, memory accumulation, governance, validation, repair reasoning, and invariant-preserving compression. Each stage produces canonical, hash-stable artifacts, ensuring that identical inputs yield byte-identical outputs across environments. QEC reframes failure as a structural phenomenon ("dark states") and introduces deterministic repair through symmetry breaking, validated via counterfactual replay. The system further demonstrates that reasoning itself can be compressed into minimal canonical forms without loss of replay fidelity. Empirical runs over QLDPC Tanner graph simulations demonstrate zero hash divergence across independent executions and compact proof artifacts (~2–5 KB), supporting the feasibility of deterministic reasoning with proof in complex systems. This work establishes a new paradigm: execution → reasoning → proof
Real-time quantum error correction requires classical decoders to process growing syndrome workloads with low and predictable latency. For quantum low-density parity-check (qLDPC) codes, iterative belief propagation (BP) repeatedly updates messages over sparse Tanner graphs, creating substantial memory-access and data-movement demands. We map normalized Min-Sum BP decoding of the [[144,12,12]] Bivariate Bicycle qLDPC code onto a DPU-based Processing-in-Memory (PIM) architecture. Within each DPU, 11 tasklets cooperatively decode one syndrome, while multiple DPUs process independent syndrome instances in parallel. Using uPIMulator and a data-qubit Pauli error model with ideal syndrome measurements, we compare throughput, per-syndrome processing time, logical error rate (LER), and single-syndrome tail latency against a 16-logical-CPU baseline. At a component-wise physical error probability of p=0.001 and one BP iteration, the projected aggregate kernel throughput of 2,560 DPUs reaches 1.071 x 10^7 decodes/s, compared with 1.22 x 10^6 decodes/s for the CPU, an 8.8x improvement. From two iterations onward, the measured LER remains below the physical error probability for every evaluated value of p. For one to five iterations, the maximum sampled serialized X+Z DPU compute latency remains below the 1 ms decoder-side reference for trapped-ion QEC, reaching approximately 0.873 ms at five iterations. These results show that near-memory processing can provide high aggregate throughput and sub-millisecond compute latency for qLDPC BP decoding under the evaluated conditions.
This work introduces a deterministic framework for identifying, validating, and falsifying structural invariants in decoder transformation pipelines. Departing from traditional performance-centric analyses of belief propagation, the study treats decoder execution as a composition of deterministic operators and focuses on invariant properties that persist under repeated application. We formally establish several classes of invariants, including ternary closure, operator idempotence, and dark-skip cascade behavior, and validate them directly against implementation through deterministic testing. In parallel, we construct explicit counterexamples to demonstrate the failure of commonly assumed properties such as universal absorbing states and global idempotence under damping. A key contribution is the introduction of invariant-guided reasoning as a mechanism for eliminating redundant computation rather than optimizing it. By reframing decoder pipelines as dynamical systems with provable algebraic structure, this work provides a foundation for deterministic runtime reduction, modular pipeline design, and future extensions into qudit-based decoding and sonification-driven analysis. This work builds on prior results in dark-state invariant detection and forms part of an ongoing research program in invariant-driven computation and quantum-inspired information dynamics.