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

The survivor count of a binary linear code: exact structure, counting complexity, and the bridge to Clifford+T circuits

N. Podgorski

Published Sep 17, 2026• 0 citations
Publisher

Abstract

To predict what a quantum computer will output you have to work out an astronomical sum, and almost every term in it cancels to nothing. This work counts how many actually survive, and shows that number is out of reach of the standard tools: not the Tutte polynomial, not the usual weight counts, not the usual recursions. A binary linear code is a set of bit strings closed under bitwise addition — the object behind error-correcting codes. This paper studies a counting quantity attached to such a code, its survivor count. Where it comes from. Take a quantum circuit built from Clifford gates and T gates and ask for the expected value of its output. That expectation is a signed sum of exponentially many terms — quadratic Gauss sums over the two-element field — indexed by the codewords of a binary linear code. What that sum comes to is a well-studied quantity. This paper asks a different question about the same sum: not what it adds up to, but how many of its terms are really there. The number that survive is the survivor count of the code. What was already known, and what is taken up here. Whether one individual term survives is classical: a quadratic Gauss sum vanishes unless its form is trivial on the radical of its polar form, and is otherwise a power of two carrying the Arf sign. The weight attached to a single support is published as well, as the local isotropic-nullity weight of Bouchet's isotropic systems and of the restricted Tutte–Martin polynomial; the paper treats it as background rather than as a result of its own. What the paper takes up is the whole family at once. The census runs over all 2k codewords of a code, and the questions asked are what determines that total, what exact evaluation costs, which parameters and moduli buy an algorithm, and how far into the planar case each side reaches. What the paper proves. An exact criterion, and a closed form. The class sum at a support vanishes unless a certain half-weight form vanishes on a radical; where it does not vanish, the survivors are counted exactly by a power of two read off the dimensions of the code. One parity obstruction can remove them all. Consequently the survivor count depends only on the code's binary matroid. Separations. It is determined by none of the following: the Tutte polynomial; the cycle and cut weight enumerators taken together on planar graphs; the local marginals. It is not invariant under duality, and it obeys no constant-coefficient deletion–contraction recursion. The standard machinery that classifies graph and matroid invariants therefore does not reach it, and every line drawn below between easy and hard is drawn from the definition instead. A complexity map. Exact evaluation is #P-complete under deterministic polynomial-time Turing reductions, both on explicit generators and on graph cycle codes, and stays hard on four restricted graph families, on linear complementary dual codes, and at each fixed hull dimension. It is polynomial at bounded pathwidth, at bounded treewidth by a proved but unimplemented join step, on several code classes, and modulo 2, 3 and 6. Planar graphs. An exact algorithm running in time 2O(√n log n), conditional on three imported constructors, together with a #P-hardness statement conditional on one named planar Tutte evaluation being #P-hard. A bridge to quantum circuits, in both directions. Every Clifford+T circuit compiles to a single code and a single integer h whose output expectation is exactly (A + B√2)/2h+1, an identity holding exactly in the ring Z[√2], where (A,B) is that code's mod-8 weight census. Separately, a reverse construction makes the sign of such a bias hard for PromiseBQP at an exponentially small threshold, while at inverse-polynomial thresholds the same sign is decided classically with bounded error. Scope, and what is not claimed. Every statement carries exactly the status its proof supports and never a stronger one. Results resting on an unproved hypothesis carry that hypothesis at the head of their own statement, and no hypothesis is discharged anywhere in the paper. Nothing here claims, implies or denies any equality or separation of complexity classes. Where a comparison with the literature was not made, the paper says so at the statement it touches; nothing here asserts priority. Supplementary material. The consolidated record, and the proof files named in the paper's appendix, are deposited separately at doi:10.5281/zenodo.22804078. Abstract, as printed in the paper A Clifford+T circuit's output expectation is a signed sum of quadratic Gauss sums over the codewords of a binary linear code; counted here is how many survive. For C in F_2^m, let K_F be the dual subcode supported in a codeword F and R_F its radical: the survivor count S(C) counts, over all F, the cosets of K_F in the even-weight subspace on F with nonzero Gauss sum. An exact criterion is proved: the class sum at F vanishes unless the half-weight form twisted by the class representative s vanishes on R_F, and survivors at nonzero F number 2^(|F|-1-dim K_F-dim R_F+[F in the dual]), or none under a parity obstruction. So S is a binary-matroid invariant determined by none of the Tutte polynomial, the cycle and cut weight enumerators together on planar graphs, or the local marginals, not duality-invariant, and obeying no constant-coefficient deletion-contraction recursion. Exact evaluation is #P-complete under polynomial-time Turing reductions, and stays hard on four restricted graph families, on linear complementary dual codes and at each fixed hull dimension; it is polynomial at bounded pathwidth, at bounded treewidth by a proved but unimplemented join step, on several code classes and modulo 2, 3, 6. For planar graphs an exact 2^(O(sqrt(n) log n)) algorithm is given, conditional on three imported constructors, with hardness conditional on one named planar Tutte evaluation being #P-hard. Every such circuit compiles to one code and an integer h with output expectation exactly (A+B sqrt 2)/2^(h+1) in Z[sqrt 2], for (A,B) that code's mod-8 weight census; a reverse construction makes that sign PromiseBQP-hard at an exponentially small threshold, while inverse-polynomial ones are decided classically with bounded error. No complexity-class equality or separation is claimed or denied.

DOI
10.5281/zenodo.22804144

Related papers

Quadratic Sums-of-Powers for Fixed-Parameter Tractable Quantum-Circuit Simulation

Alexis de Colnet, Floris Geerts, Rihan Hai +3 more

Strongly simulating a quantum circuit, that is, computing an output amplitude, can be done by summing the circuit's Feynman paths: a weighted count over assignments to Boolean path variables. The circuit's gates induce correlations among these variables, forming a graph whose structure controls several exact simulation routes. This sum-of-powers (SOP) viewpoint underlies recent simulators built on binary decision diagrams and weighted model counting. For a quadratic SOP with $n$ variables, even modulus $r$, and a rank-decomposition of its variable graph of width $k$, our dynamic program (DP) computes an amplitude using only $O(4^kpoly(n))$ arithmetic operations. For Clifford$+T$ circuits, the amplitude is given by an SOP with modulus $8$. Rank-width never exceeds linear rank-width, which governs some decision-diagram approaches, and is at most one greater than the Markov--Shi contraction complexity of the circuit tensor network. Moreover, there are non-Clifford families of bounded rank-width where both competing parameters diverge. We also present a stabilizer-rank optimization, exploiting that the DP tables are stabilizer-type Gauss sums. Each subtree runs at the width price of its cut-ranks or at a magic price that discharges the non-Clifford phases below it. The resulting best total cost never exceeds $O(4^kpoly(n))$, yet is polynomial on mixed families where the pure rank-width and pure $T$-count guarantees are both exponential. Clifford amplitudes take polynomial time on any graph, the exact-amplitude consequence of Gottesman--Knill. A prototype evaluation on standard circuit benchmarks finds treewidth bucket elimination the strongest baseline, with the new rank-width DP complementary: it wins on structured families where treewidth blows up.

quant-pharXiv:2605.29944•May 29, 2026•0 citations

The Rank Price: the interference dimension of Clifford+T circuits

Priyanshu Kumar

Representations of a Clifford+T phase polynomial, modulo Clifford operations, form a coset of the punctured Reed-Muller code RM(h-4, h). The optimization literature decodes this coset for weight: the number of odd-coefficient parities is the T-count, and its exact minimization is NP-hard. We decode the same coset for rank: the F2-dimension d of the span of the odd-parity support, minimized over the coset, which we call the interference dimension, because exact path-sum simulation costs poly x 2^d rather than 2^(T-count). We prove that the subspaces supporting some coset element form an intersection-closed family, so a unique minimal core subspace V0 exists with d = dim V0; that the Clifford-equivalence class is computed by a syndrome map into the shortened code RM(3, h); and that d equals the F2-rank of an explicit h x O(h^2) matrix read off the circuit: polynomial time, in sharp contrast with the NP-hardness of the weight objective. For the standard GF(2^k) multiplier benchmarks the invariant is a convolution tensor and d = 4k-1 exactly; combined with the hierarchy log2(t+1) <= d <= t, where t is the optimal T-count, this yields a linear lower bound on multiplier T-count in the coset model, which meets Karatsuba-type upper bounds at t = Theta(k). A counting argument gives families on which the rank price beats the optimal weight price superpolynomially. Every theorem is machine-verified (exhaustive small-case checks; 142/142 agreement with brute-force coset scans), and the method is benchmarked against the feynman suite and the quizx stabilizer decomposer, with both engines agreeing on every exact amplitude. Optimal T-count is NP-hard; the interference dimension, which is what exact simulation actually pays for, is a matrix rank. Code and machine verification of every proof step: https://github.com/0verflowme/rankprice

•Sep 12, 2026•0 citations

On Survivor Error Patterns For Maximum Likelihood Soft Decoding

Jakov Snyders

Summary Consider an (t1.k.d) binary linear block code specified by a parity-check matrix H. Assume that codewords with equal proba- bility are transmitted through a niemoryless channel. Let Y be the bit-by-bit hard-detected version of the received word, and assume that z, the corresponding syndrome, is nonzero. A set of 1 linearly independent columns of H that adds up to z will be called a /-pat- tern. Thus t does not exceed ni where n1 = ti-k is the number of check bits. A palier'ri is a I-pattern with unspecified 1. Assume, without essential loss of generality, that d t 3. Let r be the set of columns of H; then IF( = ri due to the aforementioned assumption. The ivei,oh/ of a column h of H is defined to be the confidence value (magnitude of the log likelihood ratio) of the bit associated with h. The weigh/ of a subset @ of r is the sum of the weights of the elements of @. An algorithm (I) for carrying out maximum likelihood decoding may now be phrased as follows: I) among all the /-patterns, with 1 ranging up to ni, find (the usually unique) one with least weight, then

IEEE International Symposium on Information Theory (ISIT)•Aug 24, 2005•6 citations

A theorem on the quantum evaluation of Weight Enumerators for a certain class of Cyclic Codes with a note on Cyclotomic cosets

Joseph Geraci, Frank Van Bussel

This note is a stripped down version of a published paper on the Potts partition function, where we concentrate solely on the linear coding aspect of our approach. It is meant as a resource for people interested in coding theory but who do not know much of the mathematics involved and how quantum computation may provide a speed up in the computation of a very important quantity in coding theory. We provide a theorem on the quantum computation of the Weight Enumerator polynomial for a restricted family of cyclic codes. The complexity of obtaining an exact evaluation is $O(k^{2s}(\log q)^{2})$, where $s$ is a parameter which determines the class of cyclic codes in question, $q$ is the characteristic of the finite field over which the code is defined, and $k$ is the dimension of the code. We also provide an overview of cyclotomic cosets and discuss applications including how they can be used to speed up the computation of the weight enumerator polynomial (which is related to the Potts partition function). We also give an algorithm which returns the coset leaders and the size of each coset from the list $\{0,1,2,...,N-1\}$, whose time complexity is soft-O(N). This algorithm uses standard techniques but we include it as a resource for students. Note that cyclotomic cosets do not improve the asymptotic complexity of the computation of weight enumerators.

arXiv:cs/0703129•Mar 26, 2007•2 citations

An algorithm for the T-count

GossetDavid, KliuchnikovVadym, MoscaMichele +1 more

We consider quantum circuits composed of Clifford and T gates. In this context the T gate has a special status since it confers universal computation when added to the (classically simulable) Cliff...

Quantum Information and Computation•Nov 1, 2014•6 citations

The Census Is a Kernel Wall: Certified Weight Enumerators, Stratified Trust, and the #P Frontier

The Institute for Applied Ontological Mathematics

A proof assistant's kernel evaluates by reducing terms symbolically—and that is slow. Asking the kernel to sum a stabilizer code's weight enumerator over its 224 elements is hours of reduction; the same sum, compiled, is milliseconds. This gap is not a footnote. It means a machine-checked certificate is not one thing: for an object too large for the kernel to reduce, certification splits into a ladder. On the first rung the kernel proves the method exact—that bucket elimination equals the flat sum, a small general theorem with no compiler trust. On the second the compiler executes the instance—the actual census over a real code's generators, carrying only the compiler-correctness axiom. On the third the consequences are axiom-free: the quantum MacWilliams identity forces the normalizer spectrum, the code distance, and the sub-threshold error-rate prefactor from the executed spectrum, with an empty footprint. We make this ladder the object of study, draw its trust boundary exactly, and certify the rotated surface code [[25, 1, 5]]—distance 5, prefactor 160—past a census the kernel cannot touch. The ladder has an outer wall that is a theorem, not a limitation: computing an arbitrary code's exact spectrum is #P-hard, so the bounded-treewidth codes—the surface and toric family that hardware actually deploys—are the tractable island by complexity theory, and the determinant shortcut is provably blocked on the coupled CSS enumerator by a local free-fermion obstruction. We also state the discipline the ladder demands: a certificate that reads back a constant it was handed certifies nothing; certification must be tied to the actual object, and we show the difference is a theorem that fails when the tie is cut. Published by The Institute for Applied Ontological Mathematics.

•Oct 11, 2026•0 citations
To predict what a quantum computer will output you have to work out an astronomical sum, and almost every term in it cancels to nothing. This work counts how many actually survive, and shows that number is out of reach of the standard tools: not the Tutte polynomial, not the usual weight counts, not the usual recursions. A binary linear code is a set of bit strings closed under bitwise addition — the object behind error-correcting codes. This paper studies a counting quantity attached to such a code, its survivor count. Where it comes from. Take a quantum circuit built from Clifford gates and T gates and ask for the expected value of its output. That expectation is a signed sum of exponentially many terms — quadratic Gauss sums over the two-element field — indexed by the codewords of a binary linear code. What that sum comes to is a well-studied quantity. This paper asks a different question about the same sum: not what it adds up to, but how many of its terms are really there. The number that survive is the survivor count of the code. What was already known, and what is taken up here. Whether one individual term survives is classical: a quadratic Gauss sum vanishes unless its form is trivial on the radical of its polar form, and is otherwise a power of two carrying the Arf sign. The weight attached to a single support is published as well, as the local isotropic-nullity weight of Bouchet's isotropic systems and of the restricted Tutte–Martin polynomial; the paper treats it as background rather than as a result of its own. What the paper takes up is the whole family at once. The census runs over all 2k codewords of a code, and the questions asked are what determines that total, what exact evaluation costs, which parameters and moduli buy an algorithm, and how far into the planar case each side reaches. What the paper proves. An exact criterion, and a closed form. The class sum at a support vanishes unless a certain half-weight form vanishes on a radical; where it does not vanish, the survivors are counted exactly by a power of two read off the dimensions of the code. One parity obstruction can remove them all. Consequently the survivor count depends only on the code's binary matroid. Separations. It is determined by none of the following: the Tutte polynomial; the cycle and cut weight enumerators taken together on planar graphs; the local marginals. It is not invariant under duality, and it obeys no constant-coefficient deletion–contraction recursion. The standard machinery that classifies graph and matroid invariants therefore does not reach it, and every line drawn below between easy and hard is drawn from the definition instead. A complexity map. Exact evaluation is #P-complete under deterministic polynomial-time Turing reductions, both on explicit generators and on graph cycle codes, and stays hard on four restricted graph families, on linear complementary dual codes, and at each fixed hull dimension. It is polynomial at bounded pathwidth, at bounded treewidth by a proved but unimplemented join step, on several code classes, and modulo 2, 3 and 6. Planar graphs. An exact algorithm running in time 2O(√n log n), conditional on three imported constructors, together with a #P-hardness statement conditional on one named planar Tutte evaluation being #P-hard. A bridge to quantum circuits, in both directions. Every Clifford+T circuit compiles to a single code and a single integer h whose output expectation is exactly (A + B√2)/2h+1, an identity holding exactly in the ring Z[√2], where (A,B) is that code's mod-8 weight census. Separately, a reverse construction makes the sign of such a bias hard for PromiseBQP at an exponentially small threshold, while at inverse-polynomial thresholds the same sign is decided classically with bounded error. Scope, and what is not claimed. Every statement carries exactly the status its proof supports and never a stronger one. Results resting on an unproved hypothesis carry that hypothesis at the head of their own statement, and no hypothesis is discharged anywhere in the paper. Nothing here claims, implies or denies any equality or separation of complexity classes. Where a comparison with the literature was not made, the paper says so at the statement it touches; nothing here asserts priority. Supplementary material. The consolidated record, and the proof files named in the paper's appendix, are deposited separately at doi:10.5281/zenodo.22804078. Abstract, as printed in the paper A Clifford+T circuit's output expectation is a signed sum of quadratic Gauss sums over the codewords of a binary linear code; counted here is how many survive. For C in F_2^m, let K_F be the dual subcode supported in a codeword F and R_F its radical: the survivor count S(C) counts, over all F, the cosets of K_F in the even-weight subspace on F with nonzero Gauss sum. An exact criterion is proved: the class sum at F vanishes unless the half-weight form twisted by the class representative s vanishes on R_F, and survivors at nonzero F number 2^(|F|-1-dim K_F-dim R_F+[F in the dual]), or none under a parity obstruction. So S is a binary-matroid invariant determined by none of the Tutte polynomial, the cycle and cut weight enumerators together on planar graphs, or the local marginals, not duality-invariant, and obeying no constant-coefficient deletion-contraction recursion. Exact evaluation is #P-complete under polynomial-time Turing reductions, and stays hard on four restricted graph families, on linear complementary dual codes and at each fixed hull dimension; it is polynomial at bounded pathwidth, at bounded treewidth by a proved but unimplemented join step, on several code classes and modulo 2, 3, 6. For planar graphs an exact 2^(O(sqrt(n) log n)) algorithm is given, conditional on three imported constructors, with hardness conditional on one named planar Tutte evaluation being #P-hard. Every such circuit compiles to one code and an integer h with output expectation exactly (A+B sqrt 2)/2^(h+1) in Z[sqrt 2], for (A,B) that code's mod-8 weight census; a reverse construction makes that sign PromiseBQP-hard at an exponentially small threshold, while inverse-polynomial ones are decided classically with bounded error. No complexity-class equality or separation is claimed or denied.
Strongly simulating a quantum circuit, that is, computing an output amplitude, can be done by summing the circuit's Feynman paths: a weighted count over assignments to Boolean path variables. The circuit's gates induce correlations among these variables, forming a graph whose structure controls several exact simulation routes. This sum-of-powers (SOP) viewpoint underlies recent simulators built on binary decision diagrams and weighted model counting. For a quadratic SOP with nnn variables, even modulus rrr, and a rank-decomposition of its variable graph of width kkk, our dynamic program (DP) computes an amplitude using only O(4kpoly(n))O(4^kpoly(n))O(4kpoly(n)) arithmetic operations. For Clifford+T+T+T circuits, the amplitude is given by an SOP with modulus 888. Rank-width never exceeds linear rank-width, which governs some decision-diagram approaches, and is at most one greater than the Markov--Shi contraction complexity of the circuit tensor network. Moreover, there are non-Clifford families of bounded rank-width where both competing parameters diverge. We also present a stabilizer-rank optimization, exploiting that the DP tables are stabilizer-type Gauss sums. Each subtree runs at the width price of its cut-ranks or at a magic price that discharges the non-Clifford phases below it. The resulting best total cost never exceeds O(4kpoly(n))O(4^kpoly(n))O(4kpoly(n)), yet is polynomial on mixed families where the pure rank-width and pure TTT-count guarantees are both exponential. Clifford amplitudes take polynomial time on any graph, the exact-amplitude consequence of Gottesman--Knill. A prototype evaluation on standard circuit benchmarks finds treewidth bucket elimination the strongest baseline, with the new rank-width DP complementary: it wins on structured families where treewidth blows up.
Representations of a Clifford+T phase polynomial, modulo Clifford operations, form a coset of the punctured Reed-Muller code RM(h-4, h). The optimization literature decodes this coset for weight: the number of odd-coefficient parities is the T-count, and its exact minimization is NP-hard. We decode the same coset for rank: the F2-dimension d of the span of the odd-parity support, minimized over the coset, which we call the interference dimension, because exact path-sum simulation costs poly x 2^d rather than 2^(T-count). We prove that the subspaces supporting some coset element form an intersection-closed family, so a unique minimal core subspace V0 exists with d = dim V0; that the Clifford-equivalence class is computed by a syndrome map into the shortened code RM(3, h); and that d equals the F2-rank of an explicit h x O(h^2) matrix read off the circuit: polynomial time, in sharp contrast with the NP-hardness of the weight objective. For the standard GF(2^k) multiplier benchmarks the invariant is a convolution tensor and d = 4k-1 exactly; combined with the hierarchy log2(t+1) <= d <= t, where t is the optimal T-count, this yields a linear lower bound on multiplier T-count in the coset model, which meets Karatsuba-type upper bounds at t = Theta(k). A counting argument gives families on which the rank price beats the optimal weight price superpolynomially. Every theorem is machine-verified (exhaustive small-case checks; 142/142 agreement with brute-force coset scans), and the method is benchmarked against the feynman suite and the quizx stabilizer decomposer, with both engines agreeing on every exact amplitude. Optimal T-count is NP-hard; the interference dimension, which is what exact simulation actually pays for, is a matrix rank. Code and machine verification of every proof step: https://github.com/0verflowme/rankprice
Summary Consider an (t1.k.d) binary linear block code specified by a parity-check matrix H. Assume that codewords with equal proba- bility are transmitted through a niemoryless channel. Let Y be the bit-by-bit hard-detected version of the received word, and assume that z, the corresponding syndrome, is nonzero. A set of 1 linearly independent columns of H that adds up to z will be called a /-pat- tern. Thus t does not exceed ni where n1 = ti-k is the number of check bits. A palier'ri is a I-pattern with unspecified 1. Assume, without essential loss of generality, that d t 3. Let r be the set of columns of H; then IF( = ri due to the aforementioned assumption. The ivei,oh/ of a column h of H is defined to be the confidence value (magnitude of the log likelihood ratio) of the bit associated with h. The weigh/ of a subset @ of r is the sum of the weights of the elements of @. An algorithm (I) for carrying out maximum likelihood decoding may now be phrased as follows: I) among all the /-patterns, with 1 ranging up to ni, find (the usually unique) one with least weight, then
This note is a stripped down version of a published paper on the Potts partition function, where we concentrate solely on the linear coding aspect of our approach. It is meant as a resource for people interested in coding theory but who do not know much of the mathematics involved and how quantum computation may provide a speed up in the computation of a very important quantity in coding theory. We provide a theorem on the quantum computation of the Weight Enumerator polynomial for a restricted family of cyclic codes. The complexity of obtaining an exact evaluation is O(k2s(log⁡q)2)O(k^{2s}(\log q)^{2})O(k2s(logq)2), where sss is a parameter which determines the class of cyclic codes in question, qqq is the characteristic of the finite field over which the code is defined, and kkk is the dimension of the code. We also provide an overview of cyclotomic cosets and discuss applications including how they can be used to speed up the computation of the weight enumerator polynomial (which is related to the Potts partition function). We also give an algorithm which returns the coset leaders and the size of each coset from the list {0,1,2,...,N−1}\{0,1,2,...,N-1\}{0,1,2,...,N−1}, whose time complexity is soft-O(N). This algorithm uses standard techniques but we include it as a resource for students. Note that cyclotomic cosets do not improve the asymptotic complexity of the computation of weight enumerators.
A proof assistant's kernel evaluates by reducing terms symbolically—and that is slow. Asking the kernel to sum a stabilizer code's weight enumerator over its 224 elements is hours of reduction; the same sum, compiled, is milliseconds. This gap is not a footnote. It means a machine-checked certificate is not one thing: for an object too large for the kernel to reduce, certification splits into a ladder. On the first rung the kernel proves the method exact—that bucket elimination equals the flat sum, a small general theorem with no compiler trust. On the second the compiler executes the instance—the actual census over a real code's generators, carrying only the compiler-correctness axiom. On the third the consequences are axiom-free: the quantum MacWilliams identity forces the normalizer spectrum, the code distance, and the sub-threshold error-rate prefactor from the executed spectrum, with an empty footprint. We make this ladder the object of study, draw its trust boundary exactly, and certify the rotated surface code [[25, 1, 5]]—distance 5, prefactor 160—past a census the kernel cannot touch. The ladder has an outer wall that is a theorem, not a limitation: computing an arbitrary code's exact spectrum is #P-hard, so the bounded-treewidth codes—the surface and toric family that hardware actually deploys—are the tractable island by complexity theory, and the determinant shortcut is provably blocked on the coupled CSS enumerator by a local free-fermion obstruction. We also state the discipline the ladder demands: a certificate that reads back a constant it was handed certifies nothing; certification must be tied to the actual object, and we show the difference is a theorem that fails when the tie is cut. Published by The Institute for Applied Ontological Mathematics.