How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Repetition-code syndrome, known erasures, and unlocated errors
Example
Use the binary repetition code and . A single middle-bit error in gives and a syndrome identifying that error. Two known erasures at coordinates still leave a unique completion when coordinate is received. By contrast, two unlocated errors in can produce , which lies closer to the wrong codeword .
Facts & Assumptions
Given: The binary repetition code , the parity-check matrix above, a received word , known erasures in zero-based coordinates, and the alternative unlocated-error word .
Rectangular matrix multiplication and the identity matrix , including zero-sized shapes: Matrix multiplication uses finite coordinate sums over the field.
Generator and parity-check matrices over a finite field: A parity-check matrix has independent rows and nullspace equal to .
Hamming weight and distance of a finite-field linear code: Weight counts nonzero coordinates, and is the minimum nonzero codeword weight.
Syndrome of a received word over a finite field: The syndrome of a received word is .
Classical distance gives error detection, unique decoding, and erasure recovery: Distance uniquely decodes one unknown error and gives unique erasure completion on every known support of size less than .
Verification
The codewords are and , and [L2] gives . For , multiplication gives , so exactly when and . The first two columns of form , an invertible triangular matrix over , so the rows of are independent. Therefore is a parity-check matrix by [L1]; the field operations are valid by [F1].
Direct multiplication gives the weight-at-most-one syndromes , , , and , all distinct. For , [L3] gives , so the unique matching error is and . The distinct syndromes give the one-error correction in [L4].
If coordinates are erased in , the received value at coordinate is , so is compatible and is not. More generally, two compatible codewords would differ only in , so their distance would be at most , contradicting [L4]. Hence is the unique completion.
If instead is sent, the two-bit error produces . Then but , so is the unique radius-one decoding candidate. The unique-radius-one rule therefore miscorrects this word; [L4] gives no correction guarantee for the two-bit error.
Remarks
Coordinates are zero-based. The example distinguishes a single unknown error from two known erasures and from two unknown errors; the code is guaranteed to correct one unknown error, while known locations carry stronger information.
Depends on
- Rectangular matrix multiplication and the identity matrix $I_n$, including zero-sized shapes
- Syndrome of a received word over a finite field
- Generator and parity-check matrices over a finite field
- Hamming weight and distance of a finite-field linear code
- Classical distance gives error detection, unique decoding, and erasure recovery
- For every prime $p$, the two operations on $\mathbb{Z}/p$ make it a field
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
24 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Richard Cleve, Quantum Information Processing course notes, §§36.1 and 37.1–37.1.3 (standard reference, not scraped)
- John Preskill, Quantum Computation, Chapter 7, §§7.6 and 7.4.1 (standard reference, not scraped)