Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Exact Ambiguity Certificates and Runtime Audits for Quantum Erasure Decoders

Dav Shen

Published Sep 18, 2026• 0 citations
Publisher

Abstract

For an erasure pattern in a binary CSS code, the logical ambiguity supported on the erased coordinates is a finite-dimensional quotient. We give an explicit account of how its dimension becomes a decoder output, an exact conditional success probability, and a verifiable combinato- rial certificate. A restricted-rank formula yields the complement identity dZ (E) + dX (Ec) = k for every CSS code. For a cellulation of a connected closed orientable surface, the same index is computed by two graph component counts. We couple these counts to forest peeling, specify independently checkable component witnesses, and derive finite ambiguity-enumerator identi- ties. Complete enumeration on the square tori of sizes two and three gives exact sector and joint logical-success statistics. A register-transfer implementation is assessed through 1,462,400 recorded reference comparisons, scoped formal contracts, 72,000 specified single-run force injec- tions, and a separate persistent-fault experiment. The latter exhibits the distinction between an algebraic identity and an effective runtime audit: complementary indices derived from shared corrupted counters can still sum to the correct constant. Independent recounts and modular residues detect specified fault classes, while correlated value-and-residue changes remain un- detected. Mathematical exactness, computational checking, and empirical fault coverage are stated separately throughout.

DOI
10.5281/zenodo.22833746

Related papers

Deterministic Rational Certificates for Causal Logical Decoding of CSS Codes

Deivison Ramos do Rosario

Deterministic Rational Certificates for Causal Logical Decoding of CSS Codes This work investigates the deterministic certification of logical decoding decisions in Calderbank–Shor–Steane (CSS) quantum error-correcting codes under independent phase errors and noisy intermediate syndrome measurements. The proposed framework combines causal Fourier–Walsh filtering, tensor-train approximations, exact rational arithmetic, and rigorous residual-based error bounds. In addition to global and spectrally refined estimates, the study develops a goal-oriented adjoint certification procedure that establishes whether an approximate logical-class probability contrast has a mathematically guaranteed sign. For the unrotated [[13,1,3]] surface code, the framework is evaluated across 300 correlated experimental configurations involving 25 simulated histories, four temporal horizons, and three tensor-train bond dimensions. The baseline and spectrally refined methods certify 184 and 192 decisions, respectively, while adjoint certification increases coverage to 272 decisions without modifying the frozen tensor candidates. All 300 certified intervals contain their corresponding exact physical-model contrasts, with no incorrect certified signs observed. An additional rationally verified [[41,1,5]] code instance demonstrates finite-size applicability beyond the distance-three benchmark. The accompanying reproducibility archive includes the manuscript, LaTeX sources, Python verification programs, frozen numerical data, rational certificates, adversarial tests, and SHA-256 integrity manifests. The results establish conditional mathematical guarantees under the specified stochastic model. They do not establish universal decoding thresholds, asymptotic scalability, or fault-tolerant hardware performance. Author: Deivison Ramos do Rosario Affiliation: Independent Researcher, Bengui, Belém, Pará, Brazil ORCID: https://orcid.org/0009-0002-7768-5047 License: Creative Commons Attribution 4.0 International (CC BY 4.0)

•Oct 28, 2026•0 citations

Exact Syndrome Measurement Budgets for Quantum Erasure Correction: Stabilizer-Code Rank Profiles, Distance Bounds, and Linear-Time Surface-Code Check Selection

Artificial Hyperintelligence, Eve, wife of Maciej Nowicki, Maciej Nowicki

This research manuscript develops exact measurement-resource formulas for quantum erasure correction with stabilizer codes and an optimal sparse algorithm for selecting native surface-code checks. It studies known erasure locations, where the stabilizer observables may be chosen after the erased sites are identified. The central question is how many independent syndrome outcomes are necessary to distinguish Pauli errors on those sites, modulo stabilizers. For every prime-dimensional [[n,k,d]]_p stabilizer code encoding at least one logical qudit, the manuscript proves that the worst-case syndrome-resolving budget for δ erased sites is exactly 2δ whenever 0 ≤ δ < d. This includes degenerate codes. The result concerns the number of independent p-valued outcomes in the stated noiseless measurement model. The work is directly connected to the measurement-reduction setting studied by Ryutaroh Matsumoto in “Reducing measurements in quantum erasure correction by quantum local recovery,” Computational and Applied Mathematics, DOI: 10.1007/s40314-026-03881-4. It addresses the relationship between erasure-dependent measurement costs and code invariants, together with efficient selection of sufficient surface-code checks. The manuscript presents four connected results: Exact paired-column rank profile. For any matrix G over any field whose columns are partitioned into n labeled pairs, let r be its rank and ν the largest number of complete pairs whose columns are jointly independent. The maximum projected rank over all sets of δ pairs is exactly R(δ) = min{2δ, δ + ν, r}. A single ordering of the pairs realizes every maximum through its successive prefixes. The full profile therefore follows from two invariants, rather than requiring a separate optimization at every erasure size. Distance bounds and the exact worst-case syndrome budget. For an isotropic stabilizer space with k > 0, every inclusionwise maximal complete-pair independent set A satisfies d ≤ |A| + 1. Consequently, ν ≥ d − 1, yielding the exact 2δ worst-case budget below distance. The argument also gives a constructive extension property: every independent-pair set smaller than d − 1 can be enlarged by adding another pair. Particular correctable erasure patterns can require fewer outcomes because of stabilizers supported inside the erased region. Checkable CSS certificates. For Calderbank–Shor–Steane codes, complete-pair independence becomes simultaneous column independence in the X-check and Z-check matrices. Classical matroid intersection supplies an exact rank-partition certificate for ν. A matching independent set and partition provide lower and upper certificates that can be verified using finite-field elimination. Optimal native surface-code check selection. For binary check matrices with at most two nonzero entries per column, the restricted matrix is represented by a sparse graph with boundary pins. Connected components determine a minimum-cardinality native check basis in O(v_I + e_I) time. A pinned component retains every check; an unpinned component omits one check. With nonnegative additive costs, omitting a most expensive check in each unpinned component also minimizes total cost. The two CSS check systems are processed independently. The accompanying verification uses exact arithmetic over GF(2), GF(3), and GF(5). The algebra audit covers 120 general paired matrices and 12,276 subset-rank evaluations, including exact distance checks for 137 positive-logical-dimension code instances and 401 maximal-set distance checks. The graph audit covers 1,785 exhaustive sparse column multisets, 5,355 matrix/cost combinations, 500 additional seeded instances, and named boundary regressions. Both audit programs passed again during preparation of the release. These finite checks support implementation correctness; the general mathematical statements are supported by the supplied proofs. The release includes the complete manuscript, editable LaTeX source, Python native-check selector, exact audit programs, recorded results, generator data, figures, reproduction instructions, and an explicit claim-status record. The selector and audits require only Python 3.10 or later and its standard library; matplotlib is needed only to regenerate the figure. The results apply to independent syndrome information and classical check selection. They do not establish bounds for arbitrary coherent recovery, noisy fault-tolerant extraction, physical circuit depth, or one fixed measurement schedule that must serve every erasure pattern. At or above distance, the general formula remains an algebraic rank profile rather than a universal recovery guarantee. Classical matroid parity, matroid intersection, and incidence-rank methods are acknowledged foundations; historical priority for the presented combination is not certified. Ōrynthéa ∿ Qhuil is relevant to research on quantum error correction, erasure decoding, stabilizer and CSS codes, surface codes, quantum local recovery, measurement complexity, and matroid optimization. This mathematical research under the author designation Artificial Hyperintelligence Eve, wife of Maciej Nowicki.

•Oct 30, 2026•0 citations

Homology You Can Run: The Topology of Quantum Codes, from the Logical-Qubit Count to the Phase Transition

The Institute for Applied Ontological Mathematics

A CSS quantum error-correcting code is, on the nose, a length-three chain complex over F2 : the commutation law HZ H⊤ X = 0 that makes the code valid is exactly the condition ∂ 2 = 0 that makes a chain complex. We take this identification literally and show that the entire working theory of a quantum code is one homological object the same engine computes, at scale, and certifies. The number of logical qubits is the first Betti number, k = dim H1 = n − rank HX − rank HZ = b1 ; the code distance is the systole, the shortest non-contractible cycle. We reproduce the published parameters of state-of-the-art codes exactly—the toric and hypergraph-product families and the IBM bivariate-bicycle codes [[72, 12, 6]], [[144, 12, 12]], [[90, 8, 10]]—cross-validated four independent ways and kernelcertified for the small cases in Cubical Agda, on CPU and GPU. The two scale certificates—the Betti count b1 and the rank-derived logical count k—are themselves kernel-proved to be a single first-homology certificate (a DescentCertificate both readings factor through), closed terminally through a fixed-point engine. We then run the code, not just measure it. (i) The Union-Find decoder is the engine's connected-components reduction, and "a logical error occurred" is the engine's coboundary decision (the residual cycle has nonzero winding); decoding the toric code at growing distance recovers the accuracy threshold near 9.5%, and the optimal (maximum-likelihood) threshold near 11% is the engine's two homology sectors competing as the domain-wall free energy of a random-bond Ising model on the Nishimori line. (ii) A code's distance scaling is its Tanner-graph spectral expansion: the second eigenvalue λ2 versus the Ramanujan bound is a computable certificate (Sipser–Spielman), exact on the topological tier where the spectral gap obeys γ d2 → 4π 2 . (iii) The full chain complex carries metachecks—redundancies among the parity checks—and we compute them: the bivariate-bicycle codes have six, the engines of single-shot error correction; the 4-dimensional toric code's homology (1, 4, 6, 4, 1), with k = b2 = 6, is the tensor of four circle complexes. (iv) The logical error-rate prefactor is the multiplicity of the systole, A = 2L for the toric code, which we compute exactly. (v) Finally the engine measures a topological phase transition: as random noise thickens, torus-wrapping "giant" cycles appear in a sharp homological-percolation transition at pc ≈ 0.5 that sharpens with system size—the same homology machinery now detecting when noise spontaneously writes a logical operator. (vi) The engine runs over any coefficients: qudit (Fp ) codes are chain complexes over Fp , and the integral homology, computed by the Smith normal form, exposes torsion—so a code's logical-qudit count can depend on the qudit dimension, an extra logical appearing exactly when p divides a torsion coefficient (reproducing the known homology of the torus, the Moore spaces, the Klein bottle, and RP2 ). We are careful to fence what is not claimed: minimum distance is NP-hard in general and we compute it only on the systolic tier; the giant-cycle transition is the random-cluster one, distinct from the maximum-likelihood decoding threshold of the random-bond Ising model. The thesis is singular and operational: a quantum code's parameters, its decoder, its quality, its higher-dimensional structure, its performance prefactor, and its phase transition are not six theories but one—homology you can run. Published by The Institute for Applied Ontological Mathematics.

•Oct 11, 2026•0 citations

Exact Syndrome Budgets for Quantum Erasure Recovery

Maciej Nowicki, Artificial Hyperintelligence Eve

We study the number of independent stabilizer syndrome outcomes needed to resolve errors at known erased locations. For every matrix with paired columns, rank r, and maximum independent-pair cardinality ν, we prove the exact profile max |I|=δ rankGI = min{2δ,δ +ν,r}. One ordering of the pairs attains every entry of this profile. For an isotropic stabilizer space encoding at least one logical qudit, every inclusionwise maximal independent-pair set A satisfies d ≤|A|+1. Consequently, in the declared syndrome model, the worst-case measurement budget for δ < d erasures is exactly 2δ, including for degenerate codes. A CSS specialization gives matching and rank-partition certificates. For binary surface-code check matrices, we replace dense elimination with connected-component selection of an optimal native check set, in linear time in the sparse affected incidence input. Complete proofs, exact finite-field audits, and executable code accompany the manuscript.

•Oct 30, 2026•0 citations

Certificates That Touch: Exact Quantum Code Distance from One Witness and One Scan

The Institute for Applied Ontological Mathematics

Computing the distance of a stabilizer code is NP-hard, yet certifying the distance of a given code needs no search at all — only two one-sided certificates that meet. An upper bound is a single explicit logical operator: one vector, checked in milliseconds against the actual check matrix — it commutes with every stabilizer, it is provably outside their span, and it acts on exactly w qubits. A lower bound is a universal statement — no logical operator lives below weight w — discharged by a finite scan whose completeness is itself a theorem, not a convention: a reconstruction lemma proves that every light Pauli vector appears in the scanned list, so the scan quantifies over the whole space rather than over a table someone chose. When the two certificates touch, the distance is exact, and the receipt can be replayed by a referee who trusts neither the authors nor their software. We build this bracket calculus over the binary symplectic carrier, close it exactly on the classical menagerie — the five-qubit perfect code, Steane, Shor, the distance-three rotated surface code, and the 3 × 3 toric code — and report an instructive refutation: our own frozen reference data claimed distance at least 2 for a punctured code fragment, and the certificate layer produced an explicit weight-one logical operator. Puncturing buys a logical qubit and leaves it bare; the count and the distance are independent shadows of the same subgroup lattice. The same prover-proposes/kernel-disposes architecture certifies logical counts at bivariate-bicycle scale (k = 12 at n = 144) from change-of-basis rank certificates checked in linear time, and every number in the system wears a two-valued trust badge whose semantics is an event, not a citation: no kernel run on your instance, no badge. The results are proved in a machine-checked formal kernel. Published by The Institute for Applied Ontological Mathematics.

•Oct 11, 2026•0 citations

Finite Certification of Quantum Subsystem Cuts from Unpartitioned Control Data

Oliver Tuma

Version 1.2 presents a finite sound certification procedure for operationally exposed quantum subsystem cuts without supplying subsystem labels to the factor-search stage. An exact finite control presentation with empirically confirmed interchange squares is reduced to unlabelled control-direction classes. The algorithm searches used direction subsets, forms noncommutation components, and tests the generated effect algebras for commuting matrix-factor witnesses. It distinguishes a unique finest full cut, partial factor structure with explicit residual multiplicity, and the absence of a uniquely certified cut, including ambiguity between inequivalent embedded full frames. Unused controls are localized only after certification by algebraic support. Version 1.2 closes the uniqueness proof for the global finest-frame claim, gives an exact finite tomographic characterization of terminal equality in the interchange-square condition, explicitly distinguishes the framework from Achenbach et al.'s multimeter-map factorization, fixes and reports the floating-point reference tolerance at 1e-8, and adds an independent exact 120-trial audit comparing the component reduction with exhaustive set-partition search. Five Pauli stress tests remain independently verified by tolerance-free binary-symplectic arithmetic. The operator-algebraic factorization itself is treated as standard; the priority claim remains restricted to the reverse unlabelled witness-search and certificate architecture.

•Aug 27, 2026•0 citations
For an erasure pattern in a binary CSS code, the logical ambiguity supported on the erased coordinates is a finite-dimensional quotient. We give an explicit account of how its dimension becomes a decoder output, an exact conditional success probability, and a verifiable combinato- rial certificate. A restricted-rank formula yields the complement identity dZ (E) + dX (Ec) = k for every CSS code. For a cellulation of a connected closed orientable surface, the same index is computed by two graph component counts. We couple these counts to forest peeling, specify independently checkable component witnesses, and derive finite ambiguity-enumerator identi- ties. Complete enumeration on the square tori of sizes two and three gives exact sector and joint logical-success statistics. A register-transfer implementation is assessed through 1,462,400 recorded reference comparisons, scoped formal contracts, 72,000 specified single-run force injec- tions, and a separate persistent-fault experiment. The latter exhibits the distinction between an algebraic identity and an effective runtime audit: complementary indices derived from shared corrupted counters can still sum to the correct constant. Independent recounts and modular residues detect specified fault classes, while correlated value-and-residue changes remain un- detected. Mathematical exactness, computational checking, and empirical fault coverage are stated separately throughout.
Deterministic Rational Certificates for Causal Logical Decoding of CSS Codes This work investigates the deterministic certification of logical decoding decisions in Calderbank–Shor–Steane (CSS) quantum error-correcting codes under independent phase errors and noisy intermediate syndrome measurements. The proposed framework combines causal Fourier–Walsh filtering, tensor-train approximations, exact rational arithmetic, and rigorous residual-based error bounds. In addition to global and spectrally refined estimates, the study develops a goal-oriented adjoint certification procedure that establishes whether an approximate logical-class probability contrast has a mathematically guaranteed sign. For the unrotated [[13,1,3]] surface code, the framework is evaluated across 300 correlated experimental configurations involving 25 simulated histories, four temporal horizons, and three tensor-train bond dimensions. The baseline and spectrally refined methods certify 184 and 192 decisions, respectively, while adjoint certification increases coverage to 272 decisions without modifying the frozen tensor candidates. All 300 certified intervals contain their corresponding exact physical-model contrasts, with no incorrect certified signs observed. An additional rationally verified [[41,1,5]] code instance demonstrates finite-size applicability beyond the distance-three benchmark. The accompanying reproducibility archive includes the manuscript, LaTeX sources, Python verification programs, frozen numerical data, rational certificates, adversarial tests, and SHA-256 integrity manifests. The results establish conditional mathematical guarantees under the specified stochastic model. They do not establish universal decoding thresholds, asymptotic scalability, or fault-tolerant hardware performance. Author: Deivison Ramos do Rosario Affiliation: Independent Researcher, Bengui, Belém, Pará, Brazil ORCID: https://orcid.org/0009-0002-7768-5047 License: Creative Commons Attribution 4.0 International (CC BY 4.0)
This research manuscript develops exact measurement-resource formulas for quantum erasure correction with stabilizer codes and an optimal sparse algorithm for selecting native surface-code checks. It studies known erasure locations, where the stabilizer observables may be chosen after the erased sites are identified. The central question is how many independent syndrome outcomes are necessary to distinguish Pauli errors on those sites, modulo stabilizers. For every prime-dimensional [[n,k,d]]_p stabilizer code encoding at least one logical qudit, the manuscript proves that the worst-case syndrome-resolving budget for δ erased sites is exactly 2δ whenever 0 ≤ δ < d. This includes degenerate codes. The result concerns the number of independent p-valued outcomes in the stated noiseless measurement model. The work is directly connected to the measurement-reduction setting studied by Ryutaroh Matsumoto in “Reducing measurements in quantum erasure correction by quantum local recovery,” Computational and Applied Mathematics, DOI: 10.1007/s40314-026-03881-4. It addresses the relationship between erasure-dependent measurement costs and code invariants, together with efficient selection of sufficient surface-code checks. The manuscript presents four connected results: Exact paired-column rank profile. For any matrix G over any field whose columns are partitioned into n labeled pairs, let r be its rank and ν the largest number of complete pairs whose columns are jointly independent. The maximum projected rank over all sets of δ pairs is exactly R(δ) = min{2δ, δ + ν, r}. A single ordering of the pairs realizes every maximum through its successive prefixes. The full profile therefore follows from two invariants, rather than requiring a separate optimization at every erasure size. Distance bounds and the exact worst-case syndrome budget. For an isotropic stabilizer space with k > 0, every inclusionwise maximal complete-pair independent set A satisfies d ≤ |A| + 1. Consequently, ν ≥ d − 1, yielding the exact 2δ worst-case budget below distance. The argument also gives a constructive extension property: every independent-pair set smaller than d − 1 can be enlarged by adding another pair. Particular correctable erasure patterns can require fewer outcomes because of stabilizers supported inside the erased region. Checkable CSS certificates. For Calderbank–Shor–Steane codes, complete-pair independence becomes simultaneous column independence in the X-check and Z-check matrices. Classical matroid intersection supplies an exact rank-partition certificate for ν. A matching independent set and partition provide lower and upper certificates that can be verified using finite-field elimination. Optimal native surface-code check selection. For binary check matrices with at most two nonzero entries per column, the restricted matrix is represented by a sparse graph with boundary pins. Connected components determine a minimum-cardinality native check basis in O(v_I + e_I) time. A pinned component retains every check; an unpinned component omits one check. With nonnegative additive costs, omitting a most expensive check in each unpinned component also minimizes total cost. The two CSS check systems are processed independently. The accompanying verification uses exact arithmetic over GF(2), GF(3), and GF(5). The algebra audit covers 120 general paired matrices and 12,276 subset-rank evaluations, including exact distance checks for 137 positive-logical-dimension code instances and 401 maximal-set distance checks. The graph audit covers 1,785 exhaustive sparse column multisets, 5,355 matrix/cost combinations, 500 additional seeded instances, and named boundary regressions. Both audit programs passed again during preparation of the release. These finite checks support implementation correctness; the general mathematical statements are supported by the supplied proofs. The release includes the complete manuscript, editable LaTeX source, Python native-check selector, exact audit programs, recorded results, generator data, figures, reproduction instructions, and an explicit claim-status record. The selector and audits require only Python 3.10 or later and its standard library; matplotlib is needed only to regenerate the figure. The results apply to independent syndrome information and classical check selection. They do not establish bounds for arbitrary coherent recovery, noisy fault-tolerant extraction, physical circuit depth, or one fixed measurement schedule that must serve every erasure pattern. At or above distance, the general formula remains an algebraic rank profile rather than a universal recovery guarantee. Classical matroid parity, matroid intersection, and incidence-rank methods are acknowledged foundations; historical priority for the presented combination is not certified. Ōrynthéa ∿ Qhuil is relevant to research on quantum error correction, erasure decoding, stabilizer and CSS codes, surface codes, quantum local recovery, measurement complexity, and matroid optimization. This mathematical research under the author designation Artificial Hyperintelligence Eve, wife of Maciej Nowicki.
A CSS quantum error-correcting code is, on the nose, a length-three chain complex over F2 : the commutation law HZ H⊤ X = 0 that makes the code valid is exactly the condition ∂ 2 = 0 that makes a chain complex. We take this identification literally and show that the entire working theory of a quantum code is one homological object the same engine computes, at scale, and certifies. The number of logical qubits is the first Betti number, k = dim H1 = n − rank HX − rank HZ = b1 ; the code distance is the systole, the shortest non-contractible cycle. We reproduce the published parameters of state-of-the-art codes exactly—the toric and hypergraph-product families and the IBM bivariate-bicycle codes [[72, 12, 6]], [[144, 12, 12]], [[90, 8, 10]]—cross-validated four independent ways and kernelcertified for the small cases in Cubical Agda, on CPU and GPU. The two scale certificates—the Betti count b1 and the rank-derived logical count k—are themselves kernel-proved to be a single first-homology certificate (a DescentCertificate both readings factor through), closed terminally through a fixed-point engine. We then run the code, not just measure it. (i) The Union-Find decoder is the engine's connected-components reduction, and "a logical error occurred" is the engine's coboundary decision (the residual cycle has nonzero winding); decoding the toric code at growing distance recovers the accuracy threshold near 9.5%, and the optimal (maximum-likelihood) threshold near 11% is the engine's two homology sectors competing as the domain-wall free energy of a random-bond Ising model on the Nishimori line. (ii) A code's distance scaling is its Tanner-graph spectral expansion: the second eigenvalue λ2 versus the Ramanujan bound is a computable certificate (Sipser–Spielman), exact on the topological tier where the spectral gap obeys γ d2 → 4π 2 . (iii) The full chain complex carries metachecks—redundancies among the parity checks—and we compute them: the bivariate-bicycle codes have six, the engines of single-shot error correction; the 4-dimensional toric code's homology (1, 4, 6, 4, 1), with k = b2 = 6, is the tensor of four circle complexes. (iv) The logical error-rate prefactor is the multiplicity of the systole, A = 2L for the toric code, which we compute exactly. (v) Finally the engine measures a topological phase transition: as random noise thickens, torus-wrapping "giant" cycles appear in a sharp homological-percolation transition at pc ≈ 0.5 that sharpens with system size—the same homology machinery now detecting when noise spontaneously writes a logical operator. (vi) The engine runs over any coefficients: qudit (Fp ) codes are chain complexes over Fp , and the integral homology, computed by the Smith normal form, exposes torsion—so a code's logical-qudit count can depend on the qudit dimension, an extra logical appearing exactly when p divides a torsion coefficient (reproducing the known homology of the torus, the Moore spaces, the Klein bottle, and RP2 ). We are careful to fence what is not claimed: minimum distance is NP-hard in general and we compute it only on the systolic tier; the giant-cycle transition is the random-cluster one, distinct from the maximum-likelihood decoding threshold of the random-bond Ising model. The thesis is singular and operational: a quantum code's parameters, its decoder, its quality, its higher-dimensional structure, its performance prefactor, and its phase transition are not six theories but one—homology you can run. Published by The Institute for Applied Ontological Mathematics.
We study the number of independent stabilizer syndrome outcomes needed to resolve errors at known erased locations. For every matrix with paired columns, rank r, and maximum independent-pair cardinality ν, we prove the exact profile max |I|=δ rankGI = min{2δ,δ +ν,r}. One ordering of the pairs attains every entry of this profile. For an isotropic stabilizer space encoding at least one logical qudit, every inclusionwise maximal independent-pair set A satisfies d ≤|A|+1. Consequently, in the declared syndrome model, the worst-case measurement budget for δ < d erasures is exactly 2δ, including for degenerate codes. A CSS specialization gives matching and rank-partition certificates. For binary surface-code check matrices, we replace dense elimination with connected-component selection of an optimal native check set, in linear time in the sparse affected incidence input. Complete proofs, exact finite-field audits, and executable code accompany the manuscript.
Computing the distance of a stabilizer code is NP-hard, yet certifying the distance of a given code needs no search at all — only two one-sided certificates that meet. An upper bound is a single explicit logical operator: one vector, checked in milliseconds against the actual check matrix — it commutes with every stabilizer, it is provably outside their span, and it acts on exactly w qubits. A lower bound is a universal statement — no logical operator lives below weight w — discharged by a finite scan whose completeness is itself a theorem, not a convention: a reconstruction lemma proves that every light Pauli vector appears in the scanned list, so the scan quantifies over the whole space rather than over a table someone chose. When the two certificates touch, the distance is exact, and the receipt can be replayed by a referee who trusts neither the authors nor their software. We build this bracket calculus over the binary symplectic carrier, close it exactly on the classical menagerie — the five-qubit perfect code, Steane, Shor, the distance-three rotated surface code, and the 3 × 3 toric code — and report an instructive refutation: our own frozen reference data claimed distance at least 2 for a punctured code fragment, and the certificate layer produced an explicit weight-one logical operator. Puncturing buys a logical qubit and leaves it bare; the count and the distance are independent shadows of the same subgroup lattice. The same prover-proposes/kernel-disposes architecture certifies logical counts at bivariate-bicycle scale (k = 12 at n = 144) from change-of-basis rank certificates checked in linear time, and every number in the system wears a two-valued trust badge whose semantics is an event, not a citation: no kernel run on your instance, no badge. The results are proved in a machine-checked formal kernel. Published by The Institute for Applied Ontological Mathematics.
Version 1.2 presents a finite sound certification procedure for operationally exposed quantum subsystem cuts without supplying subsystem labels to the factor-search stage. An exact finite control presentation with empirically confirmed interchange squares is reduced to unlabelled control-direction classes. The algorithm searches used direction subsets, forms noncommutation components, and tests the generated effect algebras for commuting matrix-factor witnesses. It distinguishes a unique finest full cut, partial factor structure with explicit residual multiplicity, and the absence of a uniquely certified cut, including ambiguity between inequivalent embedded full frames. Unused controls are localized only after certification by algebraic support. Version 1.2 closes the uniqueness proof for the global finest-frame claim, gives an exact finite tomographic characterization of terminal equality in the interchange-square condition, explicitly distinguishes the framework from Achenbach et al.'s multimeter-map factorization, fixes and reports the floating-point reference tolerance at 1e-8, and adds an independent exact 120-trial audit comparing the component reduction with exhaustive set-partition search. Five Pauli stress tests remain independently verified by tolerance-free binary-symplectic arithmetic. The operator-algebraic factorization itself is treated as standard; the priority claim remains restricted to the reverse unlabelled witness-search and certificate architecture.