目录Contents
速查回顾：五条随身事实Quick recap: five facts to carry
三条来自 Toric Code 教程，两条来自《大码的码距》。每条都链接到原处。 Three from the toric-code guide, two from “Distance for large codes”. Each links to where it was taught.
| # | 事实Fact | 原处Where it was taught |
|---|---|---|
| 1 | 一条奇偶检查问「这几个比特里有奇数个还是偶数个 1」（两个比特时就是「一样吗」），用 ⊕（模 2 加法：1 ⊕ 1 = 0）算出一个 0 或 1；1 是警报。A parity check asks “is the number of 1s among these bits odd or even?” (for two bits: “are they the same?”), computing a 0 or 1 with ⊕ (addition mod 2: 1 ⊕ 1 = 0); 1 is an alarm. | 2.3 节section 2.3 |
| 2 | 逻辑算符 = 与所有检查对易（不触发任何警报）、却不是检查乘积的泡利串；码距 d = 最轻逻辑算符的重量。A logical operator is a Pauli string that commutes with every check (raises no alarm) yet is not a product of checks; the distance d is the weight of the lightest one. | 4.4 节section 4.4 · 5.8 节section 5.8 |
| 3 | toric_L3 是 [[18, 2, 3]]：18 个比特、9 条星检查、9 条面检查、2 个逻辑比特、码距 3。toric_L3 is [[18, 2, 3]]: 18 qubits, 9 star checks, 9 plaquette checks, 2 logical qubits, distance 3. | 5.3 节section 5.3 |
| 4 | 码距记录有两半：上界 d ≤ w 由一条找到的逻辑算符（见证）给出；下界 d ≥ w 要排除所有更轻的候选。A distance record has two halves: the upper bound d ≤ w comes from one found logical (a witness); the lower bound d ≥ w requires excluding every lighter candidate. | 《大码的码距》1.2“Distance for large codes” 1.2 · 1.3 节1.3 |
| 5 | toric_L3 重量 1、2 的候选：纯 Z 串 171 条，纯 X 串 171 条；每个比特 X/Y/Z 三选一时共 1 431 条。全部都会触发某条警报。toric_L3's candidates of weight 1 and 2: 171 pure-Z strings, 171 pure-X strings; 1 431 when each qubit may take X, Y or Z. Every one of them raises some alarm. | 1.3 节1.3 · 5.1 节5.1 |
记号：n = 物理比特数，k = 逻辑比特数，d = 码距，w = 一条泡利串的重量（触碰的比特数），⊕ = 模 2 加法。
Notation: n = number of physical qubits, k = number of logical qubits, d = distance, w = the weight of a Pauli string (qubits touched), ⊕ = addition mod 2.
声明与证书：「我检查过了」和一张谁都能重做的表Claim versus certificate: “I checked” and a table anyone can redo
从三个经典比特开始。先说一句声明，再把同一件事写成一张六行的表，看两者差在哪里。然后把表升级到 toric_L3 的 1 431 行，最后念板上的原文。 Start with three classical bits. State a claim, then write the same fact as a six-line table and see where the two differ. Then upgrade the table to toric_L3's 1 431 lines, and finally read the board's wording.
1.1玩具：三比特重复码的六行表The toy: the six-line table of the 3-bit repetition code
三个比特 b1 b2 b3，合法字只有 000 和 111（Toric Code 教程 2.2 节的重复码）。两条检查：c1 = b1 ⊕ b2，c2 = b2 ⊕ b3。「错误」是把某几个比特翻转；一个错误若两条检查都算出 0，就是无声的。这个码的「码距」是最轻的无声非零错误的重量。声明：「d = 3，我检查过了。」证书：下面这张表。
Three bits b1 b2 b3, with 000 and 111 the only legal words (the repetition code of toric-code guide 2.2). Two checks: c1 = b1 ⊕ b2, c2 = b2 ⊕ b3. An “error” flips some bits; it is silent if both checks compute 0. The code's “distance” is the weight of the lightest silent nonzero error. The claim: “d = 3, I checked.” The certificate: the table below.
| # | 候选（翻转哪些比特）Candidate (bits flipped) | 重量Weight | 分类：触发哪条检查Classification: which check it trips | 核对方法How to recheck |
|---|---|---|---|---|
| 1 | 100 | 1 | c1 | 1 ⊕ 0 = 1 ✓ |
| 2 | 010 | 1 | c1 | 0 ⊕ 1 = 1 ✓ |
| 3 | 001 | 1 | c2 | 0 ⊕ 1 = 1 ✓ |
| 4 | 110 | 2 | c2 | 1 ⊕ 0 = 1 ✓ |
| 5 | 101 | 2 | c1 | 1 ⊕ 0 = 1 ✓ |
| 6 | 011 | 2 | c1 | 0 ⊕ 1 = 1 ✓ |
| 见证witness | 111 | 3 | 两条检查都为 0，且非零both checks 0, and nonzero | 1 ⊕ 1 = 0, 1 ⊕ 1 = 0 ✓ |
记号：bi = 第 i 个比特，cj = 第 j 条检查的读数；候选 110 表示翻转 b1、b2。表的 6 行 = C(3,1) + C(3,2) = 3 + 3 个重量小于 3 的非零候选。
Notation: bi = the i-th bit, cj = the reading of check j; candidate 110 means b1 and b2 flipped. The table's 6 rows are C(3,1) + C(3,2) = 3 + 3 nonzero candidates of weight below 3.
看两者的差别。声明要求你相信说话的人。表不要求：每一行你都可以自己做一次 ⊕，一分钟核对完六行，再确认「重量小于 3 的非零候选恰好这六个，一个不多一个不少」。你不需要懂重复码为什么好，不需要认识写表的人，甚至不需要是人——一个只会做 ⊕ 和数数的程序也能核对。这就是证书certificate：一包数据，配一台通用检查器；检查器从对象本身重新算一遍，要求与数据完全一致。QEC-Bank 契约的标准：「Supplying a rank integer alone is not a certificate」。的定义：数据 + 一台不信任任何人的检查器（表面码形式化教程 1.1 节）。表面码的那篇引了 QEC-Bank 契约文件里的一句标准：「Supplying a rank integer alone is not a certificate」——只写一个数不算证书，必须给出能重算的东西。这里，「d = 3」这个数不是证书，六行表才是。
See the difference. The claim asks you to trust the speaker. The table does not: you can redo one ⊕ per row, check all six in a minute, then confirm “the nonzero candidates of weight below 3 are exactly these six, none missing, none extra”. You need not understand why the repetition code is good, need not know who wrote the table, need not even be human; a program that can only do ⊕ and count can check it. That is the definition of a certificateA package of data plus a generic checker; the checker recomputes from the object itself and demands exact agreement with the data. The QEC-Bank contract's standard: “Supplying a rank integer alone is not a certificate”.: data plus a checker that trusts nobody (surface formal-verification guide 1.1). That guide quotes the QEC-Bank contract's standard: “Supplying a rank integer alone is not a certificate”; a bare number is not a certificate, something recomputable must be given. Here the number “d = 3” is not the certificate; the six-line table is.
1.2升级到 toric_L3：1 431 行，两种分类Upgrade to toric_L3: 1 431 lines, two kinds of classification
量子版的表长得一样，只是多了两点。第一，候选是泡利串，每个选中的比特可以放 X、Y 或 Z，所以 toric_L3 重量 1、2 的候选不是 171 条而是 18 × 3 + 153 × 9 = 1 431 条：重量 1 有 18 个位置、每个位置 3 个字母；重量 2 有 C(18, 2) = 18 × 17 ÷ 2 = 153 对位置、每对 3 × 3 = 9 种字母组合（BB 形式化教程 3.2 节）。第二，「分类」一栏有两种合法写法，因为量子码里有一类特殊候选：不触发任何警报、却无害，因为它本身就是几条检查的乘积（Toric Code 教程 5.5 节的可收缩圈）。QEC-Bank 契约（docs/design-references/2026-08-21-atlas-formal-ir-v1-contract.md）规定每行必须是下面两种之一：
The quantum table looks the same, with two additions. First, candidates are Pauli strings, each chosen qubit may carry X, Y or Z, so toric_L3's candidates of weight 1 and 2 number not 171 but 18 × 3 + 153 × 9 = 1 431: weight 1 has 18 positions with 3 letters each; weight 2 has C(18, 2) = 18 × 17 ÷ 2 = 153 pairs of positions with 3 × 3 = 9 letter combinations each (BB formal-verification guide 3.2). Second, the “classification” column has two legal forms, because quantum codes have a special kind of candidate: one that raises no alarm yet is harmless, being itself a product of checks (the contractible loop of toric-code guide 5.5). The QEC-Bank contract (docs/design-references/2026-08-21-atlas-formal-ir-v1-contract.md) requires every line to be one of:
| 契约原文Contract wording | 人话In plain words | 检查器怎么核对这一行How the checker verifies the line |
|---|---|---|
| {kind: "anticommutes", stabilizer_row} | 「它会触发第 stabilizer_row 条检查」“it trips check number stabilizer_row” | 数这条候选与那条检查在多少个比特上「X 遇 Z」式碰撞（碰撞定理）：奇数 ✓，偶数 ✗。Count on how many qubits the candidate and that check collide “X meets Z” style (the collision theorem): odd ✓, even ✗. |
| {kind: "in-span", coefficients} | 「它是这几条检查的乘积」（coefficients 列出是哪几条）“it is the product of these checks” (coefficients lists which) | 把列出的检查乘起来（模 2 相加），结果必须恰好等于这条候选。Multiply the listed checks (add mod 2); the result must equal the candidate exactly. |
toric_L3 的 1 431 行恰好全是第一种：《大码的码距》5.1 节证明了重量 ≤ 2 的纯 Z 串（和纯 X 串）没有一条是安静的（一条边有两个端点，两条边围不成圈）。混合串也一样：面检查（Z 型）只和候选里的 X、Y 字母碰撞，所以它只看得见候选的「X 部分」（把 Y 算作 X）；星检查（X 型）只看得见「Z 部分」（把 Y 算作 Z）。一条重量 ≤ 2 的非零候选，X 部分和 Z 部分至少有一个非空，而那一部分本身是一条重量 ≤ 2 的纯型串，按同一论证一定触发某条检查。第二种写法要到重量 4 才会用到（一块面的四条边），而那已经超过 d = 3，不在表里。人话：toric_L3 的证书是 1 431 行「触发第几条检查」，每行的核对是数一次碰撞。
All 1 431 lines for toric_L3 happen to be of the first kind: section 5.1 of “Distance for large codes” showed that no pure-Z (or pure-X) string of weight ≤ 2 is silent (one edge has two endpoints, two edges cannot close a loop). Mixed strings fare no better: a face check (Z-type) collides only with the candidate's X and Y letters, so it sees only the candidate's “X part” (counting Y as X); a star check (X-type) sees only the “Z part” (counting Y as Z). A nonzero candidate of weight ≤ 2 has a nonempty X part or Z part, that part is itself a pure string of weight ≤ 2, and by the same argument it trips some check. The second form is first needed at weight 4 (the four edges of one face), already above d = 3 and outside the table. In plain words: toric_L3's certificate is 1 431 lines of “trips check number j”, each verified by counting collisions once.
补课 · 对易、反对易，和「碰撞」怎么数Catch-up · Commuting, anticommuting, and how to count “collisions”
转录的每一行都靠一件事核对：候选和某条检查是对易还是反对易。先在一个比特上看。四个单比特泡利是 I（什么也不做）、X（翻转）、Z（翻相位）、Y（两样都做，Y ∝ XZ）。两个字母相同，或其中一个是 I，先做哪个都一样，叫对易；两个字母都不是 I 且不相同（X 与 Z、X 与 Y、Y 与 Z），交换顺序会多出一个负号，例如 XZ = −ZX，叫反对易。我们把这种位置叫一次碰撞。
Every line of a transcript is checked by one fact: whether the candidate and some check commute or anticommute. Start with one qubit. The four single-qubit Paulis are I (do nothing), X (flip), Z (flip the phase) and Y (both, Y ∝ XZ). If two letters are equal, or one of them is I, the order does not matter: they commute. If both are non-I and different (X with Z, X with Y, Y with Z), swapping them costs a minus sign, for example XZ = −ZX: they anticommute. We call such a position a collision.
两条整串相乘时，每个碰撞位置各贡献一个 −1，所以碰撞数为偶数，两串对易；为奇数，两串反对易。反对易为什么等于「触发警报」：检查 S 在正常状态上读出 +1（S|ψ⟩ = |ψ⟩）；错误 E 与 S 反对易时，S E|ψ⟩ = −E S|ψ⟩ = −E|ψ⟩，读数翻成 −1，这就是警报；对易时读数仍是 +1，检查看不见 E。
When two whole strings are multiplied, each collision contributes one −1, so an even number of collisions means the strings commute, an odd number means they anticommute. Why anticommuting means “trips the alarm”: check S reads +1 on a healthy state (S|ψ⟩ = |ψ⟩); if error E anticommutes with S, then S E|ψ⟩ = −E S|ψ⟩ = −E|ψ⟩ and the reading flips to −1, which is the alarm; if they commute, the reading stays +1 and the check cannot see E.
算一个例子（编号见图 5.1）A worked example (numbering as in Fig. 5.1)
toric_L3 的星检查 s4 是比特 4、7、13、14 上各放一个 X。候选 Z4（比特 4 上放 Z）：只在比特 4 上 X 遇 Z，碰撞 1 次，奇数，所以触发 s4，这一行可以写 stabilizer_row = s4。候选 Z4Z13：在比特 4 和 13 上各碰撞一次，共 2 次，偶数，s4 不亮；换星 s1（比特 1、4、10、11 上的 X），只在比特 4 上碰撞 1 次，触发，这一行写 s1。
Star check s4 of toric_L3 is an X on each of qubits 4, 7, 13, 14. Candidate Z4 (a Z on qubit 4): X meets Z only on qubit 4, one collision, odd, so it trips s4, and the line may read stabilizer_row = s4. Candidate Z4Z13: one collision on qubit 4 and one on 13, two in all, even, so s4 stays quiet; try star s1 (X on qubits 1, 4, 10, 11): one collision, on qubit 4, so it trips, and the line reads s1.
1.3顺序也是证书的一部分The order is part of the certificate
六行表有一个隐含的漏洞：怎么知道写表的人没有漏掉一行？在三比特上你可以自己数；在 1 431 行上呢？契约的办法是把顺序也定死：候选按 weight-then-support-lexicographic-then-X-Y-Z-v1 排列——先按重量，再按触碰的比特编号的字典序（像查字典：先比第一个编号，相同再比第二个），最后按 X、Y、Z 的字母顺序。1.1 节的表已经是这个顺序：重量 1 的 {1}、{2}、{3}，然后重量 2 的 {1, 2}、{1, 3}、{2, 3}。检查器自己按这个规则生成整条候选流，然后要求证书的行与它一一对应；契约原文：「classifications cannot omit, duplicate, or reorder candidates」。人话：检查器不是在读你的表，而是在生成自己的表，再和你的逐行对照。漏一行、重一行、换个顺序，全部不过。下面的小台子让你当一次这台检查器。
The six-line table has a hidden hole: how do we know the writer did not omit a line? On three bits you can count yourself; on 1 431 lines? The contract's answer is to fix the order too: candidates are listed weight-then-support-lexicographic-then-X-Y-Z-v1, by weight first, then by the dictionary order of the qubit indices touched (as in a dictionary: compare the first index, and only on a tie the second), then by the letters X, Y, Z. The table of 1.1 is already in this order: weight 1 as {1}, {2}, {3}, then weight 2 as {1, 2}, {1, 3}, {2, 3}. The checker generates the whole candidate stream itself by this rule and demands that the certificate's lines match it one for one; in the contract's words, “classifications cannot omit, duplicate, or reorder candidates”. In plain words: the checker is not reading your table; it generates its own and compares line by line. Omit one, repeat one, swap two, and it fails. The small bench below lets you play that checker once.
现在可以念题了。「no logical below weight w」就是我们这张表证明的那句话；「a proof assistant can verify」是那台不信任任何人的检查器；「small-n exhaustion transcripts」就是这种逐行的表（转录transcript：把一次穷举的每一步原样记下来的记录，使别人能重放而不必重新思考。）；「relaxation duals」是第 4 章的内容；「feeds Lean L2」第 2 章解释。
Now the problem statement can be read. “No logical below weight w” is the sentence our table proves; “a proof assistant can verify” is the checker that trusts nobody; “small-n exhaustion transcripts” are line-by-line tables like this one (a transcriptA record of every step of an exhaustion exactly as it happened, so that others can replay it without having to think it through again.); “relaxation duals” are the subject of Chapter 4; “feeds Lean L2” is explained in Chapter 2.
certified-lower-bounds · “Machine-checkable distance lower-bound certificates” · status: open · difficulty: open-research
“Certificates for 'no logical below weight w' that a proof assistant can verify (feeds Lean L2); small-n exhaustion transcripts first, relaxation duals later.”
certified-lower-bounds · “Machine-checkable distance lower-bound certificates” · status: open · difficulty: open-research
“Certificates for 'no logical below weight w' that a proof assistant can verify (feeds Lean L2); small-n exhaustion transcripts first, relaxation duals later.”
对。表的每一行都能被一个只会做 ⊕ 的检查器重算，顺序固定所以漏行会被发现。签名要求信任；论文是给人读的证明，检查器不接受「对所有 n」的定理（2.1 节），除非它被写成每个 n 各一份的数据。
Right. Every row can be recomputed by a checker that can only do ⊕, and the fixed order exposes omissions. A signature demands trust; a paper is a proof for humans, and the checker does not accept “for all n” theorems (section 2.1) unless they are written as data for each n separately.
问自己：一台只会做 ⊕ 和数数、不认识任何人的程序，能核对这样东西吗？签名它读不懂；「对所有 n」的证明它也读不懂——它只认对一个有限对象逐行重算的数据。
Ask: could a program that only does ⊕ and counting, and knows nobody, verify this object? It cannot read a signature; nor can it read a proof “for all n”. It only accepts data it can recompute line by line on one finite object.
QEC-Bank 现在是怎么凑合的：一台检查器，一道 65 536 行的门How the QEC-Bank copes today: one checker, one gate of 65 536 lines
QEC-Bank 已经有一台检查器和一种「逐行表」证书，只是那种证书写得下的码很少。先用一段话说清检查器是什么，再看哪些实例拿到了证书、哪些被门挡在外面，最后解释「feeds Lean L2」。 The QEC-Bank already has a checker and a “line-by-line table” certificate class; the class simply fits very few codes. One paragraph on what the checker is, then which instances hold a certificate and which the gate keeps out, then what “feeds Lean L2” means.
“Exact enumeration for small n only, unverified beyond.”
“Exact enumeration for small n only, unverified beyond.”
2.1一段话说清 Lean 是什么What Lean is, in one paragraph
证明助手proof assistant：一种程序，只在一个证明的每一步都严格符合少数几条固定规则时才接受它；不能被说服，只能被满足。Lean 4 是其中一种，Mathlib 是它的数学库。是一种程序，只做一件事：读一份写成形式语言的证明，逐步核对每一步是否严格符合少数几条固定规则；有一步不符就拒绝，无论作者是谁、理由多么动听。Lean 4 是这样一种程序，Mathlib 是用它写成的数学定理库（两个名字都出自 Wanted 板 lean-qec 一项的原文）。QEC-Bank 用 Lean 实现了自己的检查器，取名 qec-atlas-lean-complete-v1，2026-08-21 在 T195 任务中「封存」：源代码字节固定、断网沙箱跑通全部测试、依赖的公理不加证明就接受的起点；别的一切都要从它们推出来。只有 Lean 标准的三条（propext：两个互相推出的命题算同一个命题；Classical.choice：从一个非空的集合里总能取出一个元素；Quot.sound：把一批东西「视为相等」粘成一个整体时的基本规则。这三条是 Lean 自带的，Mathlib 普遍使用；「只有这三条」的意思是检查器没有私加任何别的假设），源码里没有 sorry 这种「先跳过」占位符（表面码形式化教程 1.2 节；原始文件 docs/design-references/2026-08-21-t195-lean-complete-v1-result.md）。它不接受什么，同一份文件写得明白：「It does not accept a per-code theorem, family-distance theorem, decoder, threshold, hardware model, Formal IR compiler, proposal referee, entry backfill, or claim promotion.」人话：这台机器只核对关于一个有限对象的数据，不读「对所有 L 成立」的定理，也不替任何声明升级。
A proof assistantA program that accepts a proof only when every step strictly follows a handful of fixed rules; it cannot be persuaded, only satisfied. Lean 4 is one such program and Mathlib its library of mathematics. is a program that does one thing: it reads a proof written in a formal language and checks step by step that each step strictly follows a handful of fixed rules; one step out of line and it refuses, whoever the author and however persuasive the reasons. Lean 4 is such a program, and Mathlib the library of mathematical theorems written in it (both names appear verbatim in the board's lean-qec item). The QEC-Bank implemented its own checker in Lean, named qec-atlas-lean-complete-v1, “sealed” on 2026-08-21 in task T195: source bytes frozen, all tests passed in an offline sandbox, the only axiomsStarting points accepted without proof; everything else must be derived from them. used being Lean's three standard ones (propext: two propositions that imply each other count as the same proposition; Classical.choice: from a nonempty collection one can always pick an element; Quot.sound: the basic rule for gluing things declared “equal” into one. These three ship with Lean and are used throughout Mathlib; “only these three” means the checker adds no private assumption of its own), and no sorry “skip this for now” placeholders in the source (surface formal-verification guide 1.2; original file docs/design-references/2026-08-21-t195-lean-complete-v1-result.md). What it does not accept, the same file states plainly: “It does not accept a per-code theorem, family-distance theorem, decoder, threshold, hardware model, Formal IR compiler, proposal referee, entry backfill, or claim promotion.” In plain words: this machine checks only data about one finite object; it does not read “for all L” theorems and it promotes no claim.
2.2已有的证书类：small-exact-distance-enumeration，与它的门The existing class, small-exact-distance-enumeration, and its gate
第 1 章那种逐行表在 QEC-Bank 里有正式名字：small-exact-distance-enumeration（表面码形式化教程 3.2 节）。契约给它设了一道门：候选总数不得超过 65 536——
Chapter 1's line-by-line table has an official name in the QEC-Bank: small-exact-distance-enumeration (surface formal-verification guide 3.2). The contract sets a gate on it: the total candidate count may not exceed 65 536:
记号：Σ 读「西格玛」，把 w = 1 到 d − 1 的各项加起来；C(n, w) = 从 n 个比特选 w 个的方法数；3w = w 个选中比特各取 X/Y/Z 的方法数；≤ 读「不超过」。契约原文：sum_{w=1}^{d-1} binomial(n,w) * 3^w <= 65536；这条上限自己的来源标为 {kind: bounded, method: t189-lean-complete-v1-certificate-size-policy}。
Notation: Σ, read “sigma”, adds the terms for w = 1 through d − 1; C(n, w) = ways to choose w of n qubits; 3w = ways for the w chosen qubits to each take X/Y/Z; ≤ reads “at most”. Contract wording: sum_{w=1}^{d-1} binomial(n,w) * 3^w <= 65536; the ceiling's own origin is recorded as {kind: bounded, method: t189-lean-complete-v1-certificate-size-policy}.
第二道门是策略：这类证书只为已经 verified 的精确码距声明生成。formal/ir/README.md 的原话：「A verified exact-distance claim additionally carries the generic small-exact certificate only when its complete lower-weight Pauli enumeration fits the frozen bounded policy; no constructor metadata is promoted into a witness.」表里最后两列用到 QEC-Bank 给每个数写的来源标签，叫证据词QEC-Bank 给每个数标注的来源：verified = 上下两半都由机器算出；bounded = 上界由机器找到的见证给出，下界引自论文（或缺失）。：verified 表示码距的上下两半都是 QEC-Bank 自己的程序算出来的（这里是穷举）；bounded 表示上界来自机器找到的一条见证，下界引自一篇论文，两半数字相等（《大码的码距》2.3 节）。把本系列遇到的五个实例代进公式（候选数由公式算出，QEC-Bank 页面上没有这些数；65 536 是 QEC-Bank 的）：
The second gate is policy: this class is generated only for exact-distance claims already verified. In the words of formal/ir/README.md: “A verified exact-distance claim additionally carries the generic small-exact certificate only when its complete lower-weight Pauli enumeration fits the frozen bounded policy; no constructor metadata is promoted into a witness.” The last two columns use the source label the QEC-Bank attaches to every number, its evidence wordThe QEC-Bank's label for where a number comes from: verified = both halves computed by machine; bounded = the upper bound from a witness the machine found, the lower bound cited from a paper (or missing).: verified means both halves of the distance were computed by the QEC-Bank's own programs (here by enumeration); bounded means the upper half comes from a witness the machine found and the lower half is cited from a paper, the two numbers agreeing (section 2.3 of “Distance for large codes”). Substituting the five instances this series has met (counts computed from the formula and absent from QEC-Bank pages; the 65 536 is the QEC-Bank's):
| 实例Instance | [[n, k, d]] | 候选数Candidates | ≤ 65 536? | d 的证据词Evidence word of d | 精确码距证书Exact-distance certificate |
|---|---|---|---|---|---|
| surface L3 | [[13, 1, 3]] | 13·3 + 78·9 = 741 | 是yes | verified | 有yes |
| toric_L3 | [[18, 2, 3]] | 18·3 + 153·9 = 1 431 | 是yes | verified | 有yes |
| surface L4 | [[25, 1, 4]] | 75 + 2 700 + 62 100 = 64 875 | 是（余 661）yes (661 to spare) | verified | 有yes |
| surface L5 | [[41, 1, 5]] | 8 498 193 | 否 → unsupportedno → unsupported | bounded | 无none |
| gross | [[144, 12, 12]] | ≈ 1.7 × 1021 | 否 → unsupportedno → unsupported | bounded | 无none |
L4 是这道门放进来的最大一个：64 875 行，离上限只差 661。L5 超出一百多倍，gross 超出约 2.6 × 1016 倍。契约对超限有一句话：「Crossing it means unsupported, not false」——超限叫「不支持」，不叫「错」：QEC-Bank 没有说 L5 的 d 不是 5，只是说这台检查器在这版政策下写不下那张表。人话：逐行表这条路，今天的门槛是候选数 65 536 行，而不是某个 n：n = 25 的 L4 进得去，n = 41、d = 5 的 L5 进不去；量子扩展码（两个经典码做「超图积」拼成的量子码）[[125,37,3]] 的 d = 3 虽由 Python 穷举 verified，但 70 125 个候选也超过了门槛，所以没有 Lean 证书。
L4 is the largest the gate admits: 64 875 lines, 661 short of the ceiling. L5 exceeds it by more than a hundredfold, gross by about 2.6 × 1016. The contract has one sentence for crossing it: “Crossing it means unsupported, not false”. The QEC-Bank does not say L5's d is not 5; it says this checker under this policy cannot write down that table. In plain words: the line-by-line road is gated today by the candidate count, 65 536 lines, and not by any n: L4 with n = 25 passes, L5 with n = 41 and d = 5 does not; the quantum expander code (a quantum code assembled from two classical codes by a “hypergraph product”) [[125,37,3]] has d = 3 verified by Python enumeration, yet its 70 125 candidates also exceed the gate, so it holds no Lean certificate.
2.3「unverified beyond」：门外的实例手里有什么“Unverified beyond”: what the instances outside the gate hold
门外的 L5 和 gross 并非一无所有。每个实例都有一份 structural-validity 证书——n、k 与 CSS 条件（X 型检查与 Z 型检查两两碰撞偶数次，即 HXHZT = 0，所以它们能同时测量）的机器版（表面码形式化教程 3.1 节）。它们缺的只是关于 d 的那份。契约里还有一类 distance-upper-bound@1（载荷 {upper: u}，「proves only d <= u」），能把一条见证封成证书；但 BB 形式化教程 3.4 节查过：gross 的 card.yaml 只登记了 structural-validity 一份，那条重量 12 的见证住在 Python 验证器里，没有封成 Lean 证书。于是 current_proxy 那句「unverified beyond」的精确含义是：候选数超过 65 536 的实例（L5、gross 都在其中），没有任何一份关于码距下界的机器证书。
L5 and gross outside the gate are not empty-handed. Every instance carries a structural-validity certificate, the machine version of n, k and the CSS condition (every X-type check collides with every Z-type check an even number of times, HXHZT = 0, so they can all be measured together) (surface formal-verification guide 3.1). What they lack is only the one about d. The contract also has a class distance-upper-bound@1 (payload {upper: u}, “proves only d <= u”) that can seal a witness into a certificate; but BB formal-verification guide 3.4 checked: gross's card.yaml registers structural-validity alone, and the weight-12 witness lives in the Python verifier, not sealed as a Lean certificate. So the precise meaning of “unverified beyond” in current_proxy is: no instance whose candidate count exceeds 65 536 (L5 and gross among them) holds any machine certificate about a distance lower bound, not even L5, whose lower bound has a paper theorem.
还有一句值得记住：证书是加上去的一层。QEC-Bank 形式化页的总纲是「Eligible small exact-distance certificates are additive; claims outside Lean Complete v1 keep their existing evidence origin」（表面码形式化教程 1.2 节）。没有证书的声明保留原有的证据词——所以 L5 和 gross 的 d 写着 bounded，一字未改，那是《大码的码距》2.3 节解释过的两半拼法。
One more sentence to remember: certificates are an additive layer. The QEC-Bank formal page's headline reads “Eligible small exact-distance certificates are additive; claims outside Lean Complete v1 keep their existing evidence origin” (surface formal-verification guide 1.2). Claims without a certificate keep their evidence word, so L5 and gross still read bounded, unchanged, the two-half assembly explained in “Distance for large codes” 2.3.
2.4「feeds Lean L2」：这道题在一座梯子上的位置“Feeds Lean L2”: where this problem sits on a ladder
Wanted 板上还有一项状态为 partial 的 lean-qec，标题 “Lean QEC framework library (L1)”，它不在本系列里（板上原文）。它的 statement 是：“Formalize symplectic GF(2), Pauli/stabilizer/subsystem codes, Knill-Laflamme for Pauli errors, CSS/chain complexes in Lean 4 / Mathlib (spec section 11; outline = foundations/).” 它引用的「spec section 11」把 QEC-Bank 的形式化工作分成四级（原始文件 docs/superpowers/specs/2026-07-04-qec-atlas-design.md 第 11 节）：L1 框架——在 Lean 里定义泡利串、稳定子码、CSS 码这些通用概念，「formalize the framework once; codes enter as instances」；L2 实例证书——对每一个具体实例，机器自动生成可判定的证书（程序能在有限步内给出「是 / 否」的那种），原文说「Cheap today: n, k, and distance upper bounds … Hard and open: certified distance lower bounds beyond small-n exhaustion」；L3 家族定理——如「toric code 对所有 L 有 d = L」；L4 由证明引导的发现。人话：L1 是字典，L2 是每个码各一张的成绩单，L3 是关于整族的定理。本篇的开放问题就是 L2 里明确标为「hard and open」的那一格；「feeds Lean L2」说的是：一旦有了写法，它填进去的正是这一格。lean-qec 的 current_proxy 也印证了现状：已接受的证书类是「structural, logical-witness, upper-bound, and bounded small-exact」四种，没有一种叫下界。
The Wanted board also carries an item with status partial, lean-qec, titled “Lean QEC framework library (L1)”, which is not in this series (board wording). Its statement reads: “Formalize symplectic GF(2), Pauli/stabilizer/subsystem codes, Knill-Laflamme for Pauli errors, CSS/chain complexes in Lean 4 / Mathlib (spec section 11; outline = foundations/).” The “spec section 11” it cites divides the QEC-Bank's formal work into four levels (original file docs/superpowers/specs/2026-07-04-qec-atlas-design.md, section 11): L1, the framework: defining Pauli strings, stabilizer codes, CSS codes and the other general notions in Lean, “formalize the framework once; codes enter as instances”; L2, instance certificates: for each concrete instance the machine auto-generates decidable certificates (ones a program can settle yes or no in finitely many steps), and the text says “Cheap today: n, k, and distance upper bounds … Hard and open: certified distance lower bounds beyond small-n exhaustion”; L3, family theorems, such as “the toric code has d = L for all L”; L4, proof-guided discovery. In plain words: L1 is the dictionary, L2 is one report card per code, L3 is theorems about whole families. This guide's open problem is exactly the cell of L2 marked “hard and open”; “feeds Lean L2” means that once a way to write it exists, that cell is what it fills. lean-qec's current_proxy confirms the present state: the accepted certificate classes are “structural, logical-witness, upper-bound, and bounded small-exact”, none of them a lower bound.
QEC-Bank 今天有一台封存的检查器和四类它认得的证书；关于码距下界的只有一类——逐行表——而且门槛是 65 536 个候选，按候选数而不是按 n 设门。门外的每个实例，包括有纸上定理的 L5，都没有任何一份机器核对过的下界证书。这道题要的是第五类证书：一种写法，让下界在门外也能被这台不信任任何人的机器核对。
Today the QEC-Bank has one sealed checker and four certificate classes it recognises; only one concerns distance lower bounds, the line-by-line table, and its gate is 65 536 candidate lines, set on the candidate count rather than on n. Every instance outside the gate, L5 with its paper theorem included, holds no machine-checked lower-bound certificate at all. This problem asks for a fifth class: a way of writing the lower bound so that, outside the gate too, this machine that trusts nobody can check it.
为什么我们想要答案：没有它，机器说不出「[[144, 12, 12]]」这句话Why we want the answer: without it the machine cannot say “[[144, 12, 12]]”
板上的理由只有一句。展开它：一张名片 [[n, k, d]] 是三句话，机器今天能说前两句半，最后半句要靠这道题。 The board's reason is one sentence. Unfold it: a calling card [[n, k, d]] is three statements, the machine can utter two and a half today, and the last half needs this problem.
“The formal-foundations layer needs LB certificates to state [[n,k,d]] theorems about instances.”
“The formal-foundations layer needs LB certificates to state [[n,k,d]] theorems about instances.”
3.1三句话，两句半Three statements, two and a half
「gross 是一个 [[144, 12, 12]] 码」是三句话叠在一起：n = 144，k = 12，d = 12。前两句是 structural-validity 证书的内容，机器已经核对（BB 形式化教程 3.1 节）。第三句本身又是两半：d ≤ 12 是一条见证，契约有现成的类（distance-upper-bound@1），只是 gross 还没封；d ≥ 12 是一个下界证书（板上缩写 LB = lower bound），契约里没有这一类能写下 n = 144 的情形。于是机器今天最多能替 gross 说出「[[144, 12, ≤ 12]]」——一张缺了半个角的名片。板上那句「to state [[n,k,d]] theorems about instances」，说的就是补上这半个角。
“Gross is a [[144, 12, 12]] code” is three statements stacked: n = 144, k = 12, d = 12. The first two are the content of the structural-validity certificate, already machine-checked (BB formal-verification guide 3.1). The third is itself two halves: d ≤ 12 is a witness, for which the contract has a ready class (distance-upper-bound@1), merely not yet sealed for gross; d ≥ 12 is a lower-bound certificate (LB on the board), and the contract has no class able to write it at n = 144. So the most the machine can say about gross today is “[[144, 12, ≤ 12]]”, a calling card with half a corner missing. The board's “to state [[n,k,d]] theorems about instances” is about filling in that half corner.
机器今天能核对：前三项machine-checkable today: the first three
记号：∧ 读「且」，表示几句话同时成立。
Notation: ∧ reads “and”, meaning the statements hold together.
3.2哪些词会翻，哪些不会Which words flip, and which do not
这道题解决后，会发生的事有严格的顺序。第一步，契约多出一类证书，暂且叫它 distance-lower-bound。第二步，对每个能写出这类证书的实例，Lean 核对它，把命题记入 discharges（契约里「已核对的命题清单」）。第三步——也是最容易误会的一步——证据词不会自动翻。契约写明成功的证书「does not rewrite the source origin」（BB 形式化教程 3.4 节）。gross 的 d 从 bounded 到 verified，需要 QEC-Bank 的验证流水线把机器下界接进 instances.yaml 的记录里，那是另一道工序。人话：这道题给机器一张能核对的纸，纸上写着 d ≥ 12；把这张纸换成条目上的一个词，是随后的事。
Once this problem is solved, what happens follows a strict order. Step one, the contract gains a new certificate class, call it distance-lower-bound for now. Step two, for every instance for which such a certificate can be written, Lean checks it and records the proposition among the discharges (the contract's “list of checked propositions”). Step three, and the easiest to misread: the evidence word does not flip automatically. The contract states that a successful certificate “does not rewrite the source origin” (BB formal-verification guide 3.4). Taking gross's d from bounded to verified requires the QEC-Bank verification pipeline to wire the machine lower bound into the instances.yaml record, a separate step. In plain words: this problem gives the machine a checkable sheet saying d ≥ 12; turning that sheet into a word on the entry is what follows.
还要分清它与《大码的码距》第 3 章的关系。那一篇要的是找到下界的方法；没有那个方法，gross 就没有任何下界可写。这一篇要的是写法；没有写法，就算论文里有下界、就算 L5 有定理，机器也说不出来。两道题缺一不可：gross 的 d 要翻成 verified，需要先有人算出 d ≥ 12，再有人把它写成检查器认得的证书。L5 的情况说明第二道题不是第一道的附属品——L5 的下界人类早就知道，机器仍然说不出，缺的只是写法。
Its relation to Chapter 3 of “Distance for large codes” also needs separating. That guide asks for a method to find the lower bound; without it gross has no lower bound to write at all. This guide asks for the way of writing it; without that, even with a bound in a paper, even with L5's theorem, the machine cannot say it. Neither problem suffices alone: to flip gross's d to verified, someone must first compute d ≥ 12 and someone must then write it as a certificate the checker recognises. L5 shows that the second problem is not an appendix to the first: humans have long known L5's lower bound, the machine still cannot state it, and only the way of writing is missing.
3.3一类用户今天做不到的事Something a class of users cannot do today
想象一个想在 Lean 里继续做证明的人——比如证明「用 gross 存 12 个逻辑比特，再做某个操作，出错概率不超过多少」。这种证明的第一行就要用到 d ≥ 12。今天他只能把它当作公理写进去：「假设 gross 的码距至少 12」。整个后续证明的可信度就系在这条假设上，而假设的来源是一篇论文。有了下界证书，这一行变成一个已核对的引理，后续证明才算真正建立在机器核对之上。板上「formal-foundations layer needs」的「needs」，就是这个意思：上层的每一个定理都要从这半个角出发。
Imagine someone who wants to keep proving things in Lean, say “storing 12 logical qubits in gross and performing some operation fails with probability at most so much”. The first line of such a proof needs d ≥ 12. Today they can only write it in as an axiom: “assume gross has distance at least 12”. The credibility of everything that follows hangs on that assumption, whose source is a paper. With a lower-bound certificate the line becomes a checked lemma, and the later proofs genuinely rest on machine checking. That is what “needs” in the board's “formal-foundations layer needs” means: every theorem in the layers above starts from that half corner.
一个合格的答案长什么样，为什么难What a qualifying answer looks like, and why it is hard
板上给了两个阶段：先把穷举转录做好，再做「松弛对偶」。这一章用一个高中恒等式解释「对偶」为什么可以比穷举短得多，再说清这道题和上一篇的分工，最后诚实列出难点。 The board gives two stages: exhaustion transcripts first, then “relaxation duals”. This chapter uses one high-school identity to explain why a dual can be far shorter than exhaustion, separates this problem's job from the previous guide's, and then lists the difficulties honestly.
4.1阶段一：把转录写得更省Stage one: writing transcripts more economically
「small-n exhaustion transcripts first」——第一阶段并不是从零开始，而是让逐行表走得更远。今天的表对每个候选写一行，X、Y、Z 都算。《大码的码距》1.3 节的折叠框证明了：对 CSS 码，最轻的逻辑算符总可取纯 X 或纯 Z。理由分三步。从一条非平凡的逻辑算符 P 出发（它与每条检查对易，又不是检查的乘积），把它拆成 X 部分（P 里写 X 或 Y 的位置放 X）和 Z 部分（写 Z 或 Y 的位置放 Z）。第一步：CSS 码的每条检查要么全是 X、要么全是 Z；一条全 X 的检查只在 P 写 Z 或 Y 的位置上碰撞，也就是只看得见 P 的 Z 部分，所以 P 与它对易，就等于 P 的 Z 部分与它对易；Z 部分与全 Z 的检查根本不碰撞。于是 Z 部分与每条检查对易，X 部分同理。第二步：两部分里至少有一个本身就是逻辑算符，否则两部分都是检查的乘积，它们的乘积（相差一个相位就是 P）也是。第三步：每一部分的重量都不超过 P 的重量。若检查器认这条引理，表就只需列纯型串：L5 的行数从 8 498 193 降到 2 × (C(41,1) + C(41,2) + C(41,3) + C(41,4)) = 2 × 112 791 = 225 582——少了 38 倍，但仍在 65 536 之上。同一条引理对 d 小的码立刻有用：[[125,37,3]] 的 70 125 行变成 2 × (125 + 7 750) = 15 750 行，进得了门。gross 则从约 1.7 × 1021 行变成约 2.0 × 1016 行，还是差得远。这个例子说明两件事：转录可以靠引理变短，而引理本身要先在 L1 里被 Lean 接受；即便如此，省行数改变不了表长怎么增长。码距 d 固定时，表的行数 Σw<d C(n,w)·3w 是 n 的 d − 1 次多项式：n 很大时，n 翻倍，行数大约乘 2d−1（d = 3 时乘 4，d = 12 时乘约 2 000，本篇脚本核对）。真正要命的是 d 跟着 n 一起长的码族：表面码 d 约为 √n，gross 在 n = 144 时 d 已是 12（论文给出的值），这时行数的增长快过 n 的任何多项式（d 与 n 成正比的码族则是指数式的）。所以靠省行数走不到 n = 144、d = 12。
“Small-n exhaustion transcripts first”: stage one does not start from zero but pushes the line-by-line table further. Today's table writes one line per candidate, X, Y and Z included. The folded box of “Distance for large codes” 1.3 proved that for CSS codes the lightest logical can always be taken pure X or pure Z. The reason takes three steps. Start from a nontrivial logical operator P (it commutes with every check and is not a product of checks) and split it into its X part (an X wherever P has X or Y) and its Z part (a Z wherever P has Z or Y). Step one: every check of a CSS code is all-X or all-Z; an all-X check collides with P only where P has Z or Y, so it sees only the Z part of P, and P commutes with it exactly when the Z part does; the Z part never collides with an all-Z check at all. So the Z part commutes with every check, and likewise the X part. Step two: at least one of the two parts is itself a logical, since otherwise both are products of checks and so is their product, which is P up to a phase. Step three: neither part weighs more than P. If the checker accepted that lemma, the table would list only pure-type strings: L5's line count would fall from 8 498 193 to 2 × (C(41,1) + C(41,2) + C(41,3) + C(41,4)) = 2 × 112 791 = 225 582, 38 times fewer yet still above 65 536. For codes with small d the same lemma pays at once: the 70 125 lines of [[125,37,3]] become 2 × (125 + 7 750) = 15 750 and fit through the gate. Gross goes from about 1.7 × 1021 lines to about 2.0 × 1016, still hopelessly far. The example shows two things: transcripts can be shortened by lemmas, and a lemma must first be accepted by Lean in L1; even so, saving lines does not change how the table grows. For a fixed distance d the line count Σw<d C(n,w)·3w is a polynomial of degree d − 1 in n: for large n, doubling n multiplies it by about 2d−1 (4 for d = 3, about 2 000 for d = 12; checked by this guide's script). The real trouble is a family whose d grows with n: for surface codes d is about √n, gross already has d = 12 at n = 144 (the paper's value), and then the count grows faster than any polynomial in n (exponentially for a family with d proportional to n). So saving lines will not reach n = 144, d = 12.
225 582、15 750 和 2.0 × 1016 这几个数是本篇按公式算的，用来说明省行数的量级；它不是 QEC-Bank 的任何政策或记录，QEC-Bank 现行契约仍按 X/Y/Z 三选一计数。
The numbers 225 582, 15 750 and 2.0 × 1016 were computed for this guide from the formula to illustrate the order of saving; it is no QEC-Bank policy or record, and the current contract still counts X/Y/Z three ways.
4.2阶段二：对偶——比穷举短得多的证书Stage two: the dual, a certificate far shorter than exhaustion
回到《大码的码距》4.2 节的高中题：证明对所有正数 x，x + 1/x ≥ 2。穷举不可能（正数有无穷多个），但一行恒等式就够：x + 1/x − 2 = (√x − 1/√x)²。现在换个角度看这一行：它不是「怎么想到的」，而是一份证书。检查器不需要任何灵感，只要把右边的平方展开，核对它等于左边——纯算术。找到这行恒等式是难的（那是研究者的工作）；核对它是容易的（那是机器的工作）。而且它的长度与 x 的个数无关：无穷多个 x，一行证书。
Return to the high-school exercise of “Distance for large codes” 4.2: prove x + 1/x ≥ 2 for every positive x. Exhaustion is impossible (infinitely many x), but one identity suffices: x + 1/x − 2 = (√x − 1/√x)². Now look at that line differently: it is not “how one thought of it” but a certificate. The checker needs no inspiration; it only expands the square on the right and confirms it equals the left, pure arithmetic. Finding the identity is hard (the researcher's job); checking it is easy (the machine's job). And its length has nothing to do with the number of x's: infinitely many x, a one-line certificate.
「松弛对偶」是这个想法在码距问题上的版本。上一篇说过，松弛是把「所有 0/1 串」放大成「允许分数」的连续区域，用线性规划（在一组一次不等式划出的区域里求一个一次式的最小值）求最小重量。先看一个能手算的小例子。三个变量 x1, x2, x3，取 1 表示选中这个比特；三条约束 x1 + x2 ≥ 1，x2 + x3 ≥ 1，x1 + x3 ≥ 1（每一对里至少选一个）。问：最少选几个？穷举要看 23 = 8 种选法。证书只要三个数 y = (½, ½, ½)：把每条约束乘以 ½ 再相加，左边 ½(x1 + x2) + ½(x2 + x3) + ½(x1 + x3) = x1 + x2 + x3，右边 ½ + ½ + ½ = 3/2，所以选中的个数 ≥ 3/2；个数是整数，于是 ≥ 2。核对只用了乘法、加法和一次向上取整，8 种选法一种也没列。注意这份论证对分数也成立（x = (½, ½, ½) 恰好取到 3/2）：它证的是放大后区域的下界 3/2，是「个数是整数」这一步把它收紧到 2，而真正的最小值确实是 2（选 x1 = x2 = 1）。
A “relaxation dual” is this idea in the distance setting. The previous guide explained relaxation: enlarge “all 0/1 strings” into a continuous region allowing fractions, and minimise the weight by linear programming (minimising a first-degree expression over a region cut out by first-degree inequalities). First a small example you can do by hand. Three variables x1, x2, x3, where 1 means the bit is chosen; three constraints x1 + x2 ≥ 1, x2 + x3 ≥ 1, x1 + x3 ≥ 1 (at least one of each pair). How few can be chosen? Exhaustion looks at 23 = 8 choices. The certificate is three numbers, y = (½, ½, ½): multiply each constraint by ½ and add; the left side is ½(x1 + x2) + ½(x2 + x3) + ½(x1 + x3) = x1 + x2 + x3, the right side ½ + ½ + ½ = 3/2, so the number chosen is ≥ 3/2; it is a whole number, hence ≥ 2. The check used multiplication, addition and one rounding up, and listed none of the 8 choices. Note that the argument holds for fractions too (x = (½, ½, ½) attains 3/2): it proves the bound 3/2 on the enlarged region, the step “the count is a whole number” tightens it to 2, and the true minimum is indeed 2 (choose x1 = x2 = 1).
线性规划有一条定理（这里只陈述，不证明）：若放大后区域上的最小值是 w，就一定存在一组非负的乘数 y1, y2, …，每条约束一个，使得「把第 i 条约束乘以 yi 再全部相加」得出的不等式，左边每个变量的系数都不超过它在重量里的系数，右边恰好是 w；因为变量都不是负数，这就推出「重量 ≥ w」。上面的 (½, ½, ½) 就是这样一组数。这组乘数就叫对偶dual：线性规划的下界证书——每条约束配一个非负乘数，加权相加后直接读出下界。核对只需乘法和加法；找到它需要求解整个规划。。它的作用与那行平方恒等式一模一样：找到它难，核对它只是乘法和加法；而且它的长度是约束的条数，不是候选的条数（1021）。那么码距问题要多少条约束？这里要小心。最直接能写出的是局部检查约束：「串与这条检查碰撞偶数次」，写成一次不等式后每条检查一条到几十条（看松弛怎么写），再加每个变量的上下限；gross 的 144 条检查合起来是 102 到 104 条。但只有这些约束的规划证不出任何东西：全零的串（一个比特也不选）满足每一条「碰撞偶数次」，最小重量是 0，证出的下界也是 0。一个有效的松弛还必须排除全零串，并排除检查的乘积（4.4 节「退化」一行说明为什么后者是难点）。一种有效的写法是：取 k 条 Z 型逻辑算符作一组基，对其中每一条 z 单独写一个规划，在局部检查约束之外再要求串与 z 碰撞奇数次；每条非平凡的 X 型逻辑算符至少对其中一条 z 如此（若它与全部 k 条都碰撞偶数次，它就与每个 Z 型逻辑算符和每条 Z 检查都对易，只能是 X 检查的乘积），所以 k 个规划的最小值里最小的那个就是 dX 的下界。这样的完整证书有多长、证出的下界能不能到 12，本篇没有算，QEC-Bank 也没有记录。所以 102–104 只是局部检查约束的条数，是一个假设性的量级，不是任何一份有效证书的长度。板上「relaxation duals later」的指望是：存在一份长度随检查条数增长、而不随候选数（1021）增长的下界证书；这样的证书今天还没有人写出来给 QEC-Bank。
Linear programming has a theorem (stated here, not proved): if the minimum over the enlarged region is w, there exist non-negative multipliers y1, y2, …, one per constraint, such that “multiply constraint i by yi and add everything up” gives an inequality whose left side has every variable's coefficient no larger than its coefficient in the weight and whose right side is exactly w; since no variable is negative, “weight ≥ w” follows. The (½, ½, ½) above is such a set. That set of multipliers is called the dualThe lower-bound certificate of a linear program: one non-negative multiplier per constraint, whose weighted sum reads off the bound directly. Checking needs only multiplication and addition; finding it needs solving the whole program.. It plays exactly the role of the squared identity: hard to find, checkable by multiplication and addition alone; and its length is the number of constraints, not the number of candidates (1021). How many constraints does the distance problem need? Care is needed here. The ones you can write down directly are the local check constraints: “the string collides with this check an even number of times”, which becomes one to a few dozen first-degree inequalities per check depending on how the relaxation is written, plus lower and upper limits on each variable; for the 144 checks of gross that makes 102 to 104. But a program with only these constraints proves nothing: the all-zero string (no bit chosen) collides evenly with every check, so the minimum weight is 0 and so is the bound. A valid relaxation must also exclude the zero string and exclude products of checks (the “degeneracy” row of 4.4 explains why the latter is the hard part). One valid way: take k Z-type logicals forming a basis and write a separate program for each such z that adds, to the local check constraints, the requirement that the string collide with z an odd number of times; every nontrivial X-type logical does so for at least one z (if it collided evenly with all k, it would commute with every Z-type logical and every Z check, and could only be a product of X checks), so the smallest of the k minima is a lower bound on dX. How long that full certificate is, and whether its bound reaches 12, this guide has not computed and the QEC-Bank does not record. So 102–104 is only the count of local check constraints, a hypothetical order of magnitude, not the length of any valid certificate. The hope behind the board's “relaxation duals later” is that a lower-bound certificate exists whose length grows with the number of checks, not with the number of candidates (1021); nobody has yet written one for the QEC-Bank.
对偶证书：每条约束一个数 yi ≥ 0；
仅局部检查约束就有 ≈ 102–104 条，
有效松弛还要更多（未算）exhaustion certificate: one line per candidate,
≈ 1021 lines
dual certificate: one number yi ≥ 0 per constraint;
the local check constraints alone number ≈ 102–104,
a valid relaxation needs more (not computed)
记号：yi = 第 i 条约束的乘数，i 从 1 数到约束条数；≥ 0 表示乘数不能是负数（负数会把不等号翻转）。102–104 是本篇对局部检查约束条数的假设性估算（144 条检查，每条 1 到几十条约束，另加 2 × 144 条变量上下限），不是 QEC-Bank 的任何记录，也不是一份有效证书的长度：只有这些约束时全零串可行，下界是 0。
Notation: yi = the multiplier of constraint i, i running from 1 to the number of constraints; ≥ 0 means a multiplier may not be negative (a negative one would flip the inequality). 102–104 is this guide's hypothetical estimate of the number of local check constraints (144 checks, one to a few dozen constraints each, plus 2 × 144 variable limits); it is no QEC-Bank record and not the length of a valid certificate: with these constraints alone the zero string is feasible and the bound is 0.
4.3两道题的分工How the two problems divide the work
| 大码的码距（fast-distance）Distance for large codes (fast-distance) | 本篇（certified-lower-bounds）This guide (certified-lower-bounds) | |
|---|---|---|
| 问的是Asks | 怎么算出一条下界 wHow to compute a lower bound w | 怎么把下界写成检查器能核对的数据How to write the bound as data a checker can verify |
| 输出Output | 一个数，加一个论证A number plus an argument | 一包数据 + 契约里的一类证书 + Lean 的一次通过A data package + a contract certificate class + one Lean pass |
| 对 toric_L3On toric_L3 | 三句几何论证（5.1 节）Three sentences of geometry (5.1) | 1 431 行「触发第 j 条检查」1 431 lines of “trips check j” |
| 对 grossOn gross | 尚无：引文 bravyi2024bicycleNone yet: the citation bravyi2024bicycle | 尚无：契约无此类；即便有了论证，也没有写法None yet: no such contract class; even given an argument, no way to write it |
| 两者的交点Where they meet | 对偶：算法算出它（上一篇），检查器核对它（本篇）。同一组数字，两种用途。The dual: the algorithm computes it (previous guide), the checker verifies it (this guide). The same numbers, two uses. | |
4.4为什么是 open-researchWhy open-research
板上给的难度是 open-research：没人知道怎么做，而不是知道怎么做但要做很多。诚实地列出难点：
The board rates it open-research: nobody knows how, rather than known but laborious. The difficulties, honestly:
| 难点Difficulty | 人话In plain words |
|---|---|
| 对偶要「够紧」The dual must be tight enough | 对偶证明的是放大后集合的下界；若放大得太松，它证出的 w 可能只有 6，而 gross 需要 12。这一点属于上一篇，但直接决定本篇有没有东西可写。A dual proves a bound for the enlarged set; if the enlargement is too loose, the w it proves may be 6 where gross needs 12. This belongs to the previous guide but decides whether this one has anything to write. |
| 退化不是一次不等式Degeneracy is not a first-degree inequality | 一个码能纠正的两个不同错误，若对码字的作用完全一样（两者之积是一个不等于恒等的检查乘积），这个码就叫退化degeneracy：能纠正的两个不同错误对码字作用相同，即两者之积是非恒等的检查乘积（Preskill 讲义 7.9.1 节）。常用的码距版说法：有比码距 d 还轻的非恒等检查乘积。的（Preskill 讲义 7.9.1 节；同一处也给出常用的码距版说法：检查乘积里有比码距 d 还轻的非恒等元素）。toric_L3 不退化：最轻的非恒等检查乘积是一颗星或一块面，重量 4，比 d = 3 重；它能纠正重量 ≤ 1 的错误，两个这样的错误之积重量 ≤ 2，不可能是检查乘积。toric_L5 退化：d = 5，能纠正重量 ≤ 2 的错误，而一颗星（重量 4）恰好拆成两个重量 2 的错误——星上两条横边放 X，或两条竖边放 X——两者之积就是这颗星，所以它们触发同样的警报，对码字的作用也一样（本篇脚本核对）。这为什么让对偶难写：对不退化的码，安静且非零的串最轻就有 d 那么重，下界只需排除全零串；对退化的码（gross 的检查重量 6，比 12 轻），有比 d 轻的安静串（检查乘积）必须排除，而「不是检查乘积」不能直接写成一次不等式，标准的线性规划对偶不能照搬，要先找到合适的松弛。A code is called degenerateTwo different correctable errors act identically on the codewords: their product is a nonidentity product of checks (Preskill's notes, 7.9.1). The common distance version: some nonidentity product of checks is lighter than the distance d. when two different errors it can correct act identically on the codewords, their product being a nonidentity product of checks (Preskill's notes, 7.9.1; the same place gives the common distance version: some nonidentity product of checks is lighter than the distance d). toric_L3 is not degenerate: its lightest nonidentity check product is one star or one face, weight 4, heavier than d = 3; it corrects errors of weight ≤ 1, and the product of two such errors weighs ≤ 2, so it cannot be a check product. toric_L5 is degenerate: d = 5, it corrects errors of weight ≤ 2, and one star (weight 4) splits exactly into two weight-2 errors, X on the star's two horizontal edges or X on its two vertical edges; their product is the star, so they raise the same alarms and act identically on the codewords (checked by this guide's script). Why this makes the dual hard: for a nondegenerate code a silent nonzero string already weighs at least d, so the bound only has to exclude the zero string; for a degenerate code (gross has checks of weight 6, lighter than 12) there are silent strings lighter than d, the check products, that must be excluded, and “not a check product” is not directly a first-degree inequality, so the standard LP dual cannot be copied and a suitable relaxation must first be found. |
| 检查器要先认得字典The checker must first know the dictionary | 要让 Lean 核对「这组乘数推出 d ≥ 12」，Lean 里得先有「逻辑算符」「对易」「松弛」这些定义和把对偶与码距连起来的引理——这些都是 L1 的内容，而 L1 本身状态是 partial。For Lean to check “these multipliers imply d ≥ 12”, Lean must first contain the definitions of “logical operator”, “commute”, “relaxation” and the lemma connecting the dual to the distance; all of this is L1 content, and L1 itself is partial. |
| 算术要精确The arithmetic must be exact | 求解线性规划的程序用的是带舍入的小数；证书里的乘数必须是精确的分数，让检查器的乘加没有任何误差。把一个舍入过的解「修圆」成精确证书，本身是一件要小心的事。LP solvers work in rounded decimals; the multipliers in a certificate must be exact fractions so that the checker's multiply-and-add has no error at all. Turning a rounded solution into an exact certificate is itself a delicate step. |
| 检查器要保持小而封存The checker must stay small and sealed | Lean Complete v1 的可信来自它只依赖三条公理、源码封存。每加一类证书都要重新审计、重新封存，并保证「Crossing it means unsupported, not false」这类边界依然说得清。Lean Complete v1 is trusted because it relies on three axioms only and its source is sealed. Every added certificate class means re-auditing, re-sealing, and keeping boundaries such as “Crossing it means unsupported, not false” statable. |
4.2 节里「线性规划的下界一定有一组乘数作证」是一条定理（线性规划对偶定理），本篇只陈述、不证明，它超出高中数学。「对偶证书长度等于约束条数」是这条定理的直接后果；gross 上要多少条约束，本篇只给了局部检查约束的假设性计数，不是 QEC-Bank 的任何记录。QEC-Bank 的契约今天没有任何一类叫 distance-lower-bound 的证书；3.2 节和 4.3 节里这个名字是本篇为了讲清楚而临时取的。本篇没有运行 Lean，也没有运行 QEC-Bank 的验证器；所有数字抄自仓库文件或按契约公式算出。
In 4.2, “a linear-programming lower bound always has a set of multipliers as witness” is a theorem (LP duality), stated here without proof and beyond high-school mathematics. “A dual certificate is as long as the number of constraints” is its direct consequence; for how many constraints gross needs, this guide gives only a hypothetical count of the local check constraints, no QEC-Bank record. The QEC-Bank contract today has no certificate class named distance-lower-bound; the name in 3.2 and 4.3 is a placeholder coined by this guide for clarity. Neither Lean nor the QEC-Bank verifier was run for this guide; every number is copied from repository files or computed from the contract's formula.
从这里出发能做什么：亲手写两份证书What you can do from here: write two certificates by hand
第一份是上界证书：在实验台上画出 toric_L3 的一条逻辑算符，那一刻你手里就是契约里 distance-upper-bound@1 的载荷。第二份是下界转录的一角：用一条规则写出 toric_L3 的 18 行重量 1 候选，再想想 153 行重量 2 怎么写。最后是往哪里走。 The first is an upper-bound certificate: draw one logical operator of toric_L3 on the bench and you hold the payload of the contract's distance-upper-bound@1. The second is a corner of the lower-bound transcript: write toric_L3's 18 weight-1 lines from one rule, then think about how the 153 weight-2 lines go. Then, where to go next.
5.1上界证书：一条见证，一个数The upper-bound certificate: one witness, one number
下面的构造器预设为 toric_L3（A = 1 + x，B = 1 + y，正是 3 × 3 环面码，BB 直觉教程 5.1 节）。A、B 是 BB 码的写法：1 表示原地，x 表示向右一格，y 表示向上一格；A = 1 + x 说每条 X 检查碰左层里原地和右边一格的两个比特，B = 1 + y 说它碰右层里原地和上面一格的两个比特。对 toric_L3，左层就是图 5.1 的横边（比特 0–8），右层是竖边（比特 9–17），X 检查就是星。按「搜索低重逻辑算符」，它穷举出一条重量 3 的 X 型逻辑算符，在画面上用红圈标出它碰的比特，并在下方列出列号。契约里 distance-upper-bound@1 的载荷只有 {upper: u}，见证本身通过 witness_refs 引用；检查器要做的是：重算这条串与每条 Z 检查的碰撞数（全为偶数；纯 X 串和 X 检查不会碰撞），确认它不是 X 检查的乘积，数它的重量，核对等于 u。第二件事靠数秩：把 HX 的每一行看成一串 0/1，按位异或当加法，秩就是最多能挑出几行、使其中任何几行加起来都不为零。toric_L3 的 9 颗星只有 8 行独立（9 颗星全乘起来是恒等，所以任意 8 颗的积等于剩下那颗），秩是 8；把见证（比特 0、1、2 上放 X）作为第 10 行加进去，秩变成 9（本篇脚本核对，读数里也会显示）。如果见证是某几颗星的乘积，它就是某几行的和，加进去不会多出新的方向，秩应当还是 8；秩多了 1，就证明了它不是任何几颗星的乘积。红圈标出的那几个比特，加上一个数 u，就是这样一份证书的全部内容——它「proves only d <= u」，只证明码距不超过 u。
The builder below is preset to toric_L3 (A = 1 + x, B = 1 + y, precisely the 3 × 3 toric code, BB intuition guide 5.1). A and B are BB-code notation: 1 means stay, x one step right, y one step up; A = 1 + x says every X check touches the left-layer qubits at its own site and one step right, B = 1 + y that it touches the right-layer qubits at its own site and one step up. For toric_L3 the left layer is the horizontal edges of Fig. 5.1 (qubits 0–8), the right layer the vertical edges (qubits 9–17), and the X checks are the stars. Press “Search a low-weight logical”: it enumerates and finds an X-type logical of weight 3, rings the qubits it touches in red on the canvas and lists their column numbers below. The contract's distance-upper-bound@1 payload is just {upper: u}, with the witness itself referenced through witness_refs; the checker's job is to recompute the string's collision count with every Z check (all even; a pure-X string never collides with an X check), confirm it is not a product of X checks, count its weight and match it to u. The second job is done by counting a rank: read each row of HX as a string of 0s and 1s with bitwise XOR as addition; the rank is the largest number of rows none of whose nonempty subsets adds up to zero. The 9 stars of toric_L3 have only 8 independent rows (all 9 multiply to the identity, so any 8 multiply to the remaining one), so the rank is 8; append the witness (X on qubits 0, 1, 2) as a tenth row and the rank becomes 9 (checked by this guide's script; the readout shows it too). Were the witness a product of some stars, it would be the sum of those rows, appending it would add no new direction, and the rank would stay 8; the rank went up by 1, which proves it is not a product of any stars. The ringed qubits plus one number u are the entire content of such a certificate; it “proves only d <= u”, that the distance is at most u.
5.2下界转录的一角：18 行，用一条规则A corner of the lower-bound transcript: 18 lines from one rule
按图 5.1 给 toric_L3 的每条边编号 0 到 17。重量 1 的纯 Z 候选有 18 条：「第 e 条边上放 Z」。每一条的分类都是同一句话：{kind: "anticommutes", stabilizer_row: 边 e 的任一端点的星检查编号}。核对：Z 与那颗星在恰好一个比特（边 e）上碰撞，1 是奇数 ✓。你可以真的写下 18 行，也可以写下这条规则——但注意，检查器只收 18 行，不收规则；把规则变成它认得的东西，是 L1 的工作。重量 2 的 153 条纯 Z 候选同理：两条边若相邻（共用一个端点），写任一条边另一端的星，不能写共用端点的星，因为它碰撞两次；若不相邻，写任一端点的星（本篇用脚本把 153 条逐一核对过）。这就是 4.1 节说的「转录可以靠引理变短」——你脑子里的规则，是机器还没有的引理。
Number toric_L3's edges 0 to 17 as in Fig. 5.1. The weight-1 pure-Z candidates are 18: “Z on edge e”. Every one has the same classification: {kind: "anticommutes", stabilizer_row: the star check at either endpoint of edge e}. Check: Z and that star collide on exactly one qubit (edge e), and 1 is odd ✓. You may really write the 18 lines, or write the rule; but note that the checker takes only the 18 lines, never the rule; turning the rule into something it recognises is L1's job. The 153 weight-2 pure-Z candidates go likewise: for two adjacent edges (sharing an endpoint) write the star at the other end of either edge, never the shared one, which collides twice; for non-adjacent edges, the star at any endpoint (this guide checked all 153 by script). This is 4.1's “transcripts can be shortened by lemmas”: the rule in your head is a lemma the machine does not yet have.
对照一下 QEC-Bank 自己在表面码 L3 上留下的机器见证（codes/surface/pedagogy/distance-proof.md 第 4 节原文）：logical X support: [0, 1, 2]、logical Z support: [0, 3, 6]、exact_distance(L=3): 3 (exact-css-enum)——一条横跨串、一条竖跨串、一次穷举。那两行支撑就是见证。那次穷举只列纯 X、纯 Z 串，它排除重量 1、2 的那部分展开来是 2 × (13 + 78) = 182 行；Lean 证书的转录把 X、Y、Z 三种字母都列上，是 741 行。
Compare the machine witnesses the QEC-Bank itself left on surface L3 (codes/surface/pedagogy/distance-proof.md, section 4, verbatim): logical X support: [0, 1, 2], logical Z support: [0, 3, 6], exact_distance(L=3): 3 (exact-css-enum): one string spanning across, one spanning down, one exhaustion. The two support lines are the witnesses. That exhaustion lists only pure-X and pure-Z strings; the part ruling out weights 1 and 2, unrolled, is 2 × (13 + 78) = 182 lines; the Lean certificate's transcript lists all three letters X, Y, Z and has 741 lines.
5.3往哪里走Where to go next
相关条目。这道题的 yaml 里 related 是空的：它不属于某一个码，而属于形式化层。最贴近的教程是两个条目的形式化篇：表面码 1.1 证书 = 数据 + 检查器、3.2 逐行表、3.3 L5 为什么没有、4.2 默认验证不需要 Lean；BB 3.2 toric_L3 的 1 431 个候选、3.3 gross 为什么没有。仓库里的边界文件：formal/ir/README.md（一段话说明默认验证「never invokes Lean or the network」，只重生成投影、独立核对每份证书、比对字节）。
Related entries. This problem's yaml has an empty related list: it belongs to no single code but to the formal layer. The nearest guides are the two entries' formal-verification pages: surface 1.1, certificate = data + checker, 3.2 the line-by-line table, 3.3 why L5 has none, 4.2 default verification needs no Lean; BB 3.2, toric_L3's 1 431 candidates, 3.3 why gross has none. The boundary file in the repository: formal/ir/README.md (one paragraph stating that default verification “never invokes Lean or the network”, only regenerating the projection, checking every certificate independently and comparing bytes).
同一系列。找到下界的那一半：《大码的码距：便宜的上界，昂贵的下界》。同样撞上 2n 墙的另一道题（穿了衣服的码距）：《不在乎的比特，与穿了衣服的码距》。板上的 partial 项 lean-qec。
Same series. The finding half: “Distance for large codes: cheap upper bounds, expensive lower bounds”. Another problem that hits the same 2n wall (the dressed distance): “Don't-care qubits and the dressed distance”. The partial board item lean-qec.
一张表、一道门、半个角One table, one gate, half a corner
回放一遍。声明要人信，证书让机器算：每个候选一行，写明它触发哪条检查或它是哪些检查的乘积，顺序固定，检查器自己生成候选流逐行对照。QEC-Bank 的检查器 Lean Complete v1 已封存，认得四类证书；关于下界的只有逐行表 small-exact-distance-enumeration，门槛 Σ C(n,w)·3w ≤ 65 536：L3 741 行、toric_L3 1 431 行、L4 64 875 行进了门，L5 的 8 498 193 行和 gross 的 1021 行在门外，「unsupported, not false」。没有下界证书，机器只能说 [[144, 12, ≤ 12]]，上层的每个定理都得把 d ≥ 12 当公理。合格的答案分两步：先用引理把转录写短，再找到像 (√x − 1/√x)² 那样一行顶无穷的对偶证书——指望它的长度随检查条数走，不随候选数（1021）走；光是局部检查约束就有几百到几千条，而一份有效证书还需排除零串和检查乘积，长度没人算过。难在对偶要紧、退化不线性、字典（L1）未全、算术要精确、检查器要小。状态 open，难度 open-research。
Replay. A claim asks for trust; a certificate lets a machine compute: one line per candidate saying which check it trips or which checks multiply to it, in a fixed order, with the checker generating the candidate stream itself and comparing line by line. The QEC-Bank checker Lean Complete v1 is sealed and recognises four certificate classes; the only one about lower bounds is the line-by-line small-exact-distance-enumeration, gated by Σ C(n,w)·3w ≤ 65 536: L3's 741 lines, toric_L3's 1 431 and L4's 64 875 pass, L5's 8 498 193 and gross's 1021 stay outside, “unsupported, not false”. Without a lower-bound certificate the machine can only say [[144, 12, ≤ 12]], and every theorem above must take d ≥ 12 as an axiom. A qualifying answer comes in two steps: shorten transcripts with lemmas, then find a dual certificate like (√x − 1/√x)², one line covering infinitely many cases, hoping for a length set by the number of checks rather than by the candidates (1021); the local check constraints alone number hundreds to thousands, and a valid certificate must also exclude the zero string and check products, at a length nobody has computed. Hard because the dual must be tight, degeneracy is not linear, the dictionary (L1) is incomplete, the arithmetic must be exact and the checker must stay small. Status open, difficulty open-research.
符号与读法Symbols & how to read them
| 符号Symbol | 名称与读法Name & how to read it | 在本篇中的含义Meaning in this guide |
|---|---|---|
| [[n, k, d]] | 双方括号，读「n k d 码」Double brackets, read “an n k d code” | n 个物理比特、k 个逻辑比特、码距 d；3.1 节把它拆成四句话。n physical qubits, k logical qubits, distance d; 3.1 splits it into four statements. |
| w, u | 读「重量」「上界」Read “weight”, “upper” | w = 候选的重量，也是「no logical below weight w」里的那个数；u = distance-upper-bound@1 载荷 {upper: u} 里的见证重量。w = a candidate's weight, also the number in “no logical below weight w”; u = the witness weight in the distance-upper-bound@1 payload {upper: u}. |
| bi, cj | 读「第 i 个比特」「第 j 条检查」Read “bit i”, “check j” | 1.1 节三比特玩具：c1 = b1 ⊕ b2，c2 = b2 ⊕ b3。The three-bit toy of 1.1: c1 = b1 ⊕ b2, c2 = b2 ⊕ b3. |
| ⊕ | 圆圈加，读「异或」Circled plus, read “xor” | 模 2 加法：1 ⊕ 1 = 0；一条奇偶检查就是几个比特的 ⊕。Addition mod 2: 1 ⊕ 1 = 0; a parity check is the ⊕ of a few bits. |
| C(n, w), 3w, Σ | 读「n 选 w」「3 的 w 次方」「西格玛」Read “n choose w”, “3 to the w”, “sigma” | 候选数公式 Σw=1d−1 C(n,w)·3w：挑 w 个比特的方法数 × 每个取 X/Y/Z 的方法数，对 w 求和。The candidate formula Σw=1d−1 C(n,w)·3w: ways to pick w qubits × ways for each to take X/Y/Z, summed over w. |
| ≤, ≥ | 读「不超过 / 不小于」Read “at most / at least” | d ≤ u 上界，d ≥ w 下界；候选数 ≤ 65 536 是政策门。d ≤ u upper bound, d ≥ w lower bound; candidates ≤ 65 536 is the policy gate. |
| ∧ | 读「且」Read “and” | 几句话同时成立；[[144,12,12]] = (n = 144) ∧ (k = 12) ∧ (d ≤ 12) ∧ (d ≥ 12)。Statements holding together; [[144,12,12]] = (n = 144) ∧ (k = 12) ∧ (d ≤ 12) ∧ (d ≥ 12). |
| yi | 读「第 i 个乘数」Read “multiplier i” | 对偶证书里每条约束配的非负数；加权相加后读出下界。The non-negative number attached to constraint i in a dual certificate; the weighted sum reads off the bound. |
| √x | 读「根号 x」Read “root x” | 4.2 节的一行证书：x + 1/x − 2 = (√x − 1/√x)²。The one-line certificate of 4.2: x + 1/x − 2 = (√x − 1/√x)². |
| @1, v1 | 读「第 1 版」Read “version 1” | 契约给每类证书和每条排序规则的版本号：distance-upper-bound@1、…-X-Y-Z-v1、Lean Complete v1。版本会变，变之前页面上的词不变。The contract's version tags on each certificate class and ordering rule: distance-upper-bound@1, …-X-Y-Z-v1, Lean Complete v1. Versions may move; until they do, the words on the pages stay. |
| L1 / L2 / L3 | 读「第一、二、三级」Read “level one, two, three” | QEC-Bank 形式化梯子：框架字典 / 每个实例的证书 / 整族的定理。本篇的题在 L2。The QEC-Bank formal ladder: framework dictionary / per-instance certificates / whole-family theorems. This guide's problem sits in L2. |
本篇新增词汇New terms in this guide
| 术语Term | 白话定义Plain definition |
|---|---|
| 声明 / 证书claim / certificate | 要人相信的一句话 / 一包数据加一台不信任任何人的检查器，检查器重算并要求完全一致。A sentence to be trusted / a data package plus a checker that trusts nobody, recomputing and demanding exact agreement. |
| 转录（transcript）transcript | 把一次穷举的每一步原样记下，供别人重放；逐行表就是转录。Every step of an exhaustion recorded as it happened, for others to replay; the line-by-line table is one. |
| 分类（anticommutes / in-span）classification (anticommutes / in-span) | 转录每行的两种合法内容：它触发第几条检查 / 它是哪些检查的乘积。The two legal contents of a transcript line: which check it trips / which checks multiply to it. |
| 候选流与排序candidate stream and ordering | 检查器按 weight-then-support-lexicographic-then-X-Y-Z-v1 自己生成的全部候选，与转录逐行对照；不能漏、重、换序。All candidates the checker itself generates in weight-then-support-lexicographic-then-X-Y-Z-v1 order, compared line by line with the transcript; no omission, duplication or reordering. |
| 证明助手 / Lean / Mathlibproof assistant / Lean / Mathlib | 只在每一步都合规则时才接受证明的程序 / 一种这样的程序 / 用它写成的数学库。A program accepting a proof only when every step follows the rules / one such program / the mathematics library written in it. |
| 封存（sealed）/ 公理 / sorrysealed / axiom / sorry | 源码字节固定并审计完毕 / 不加证明就接受的起点（Lean Complete v1 只用三条）/ Lean 里「先跳过」的占位符（源码中没有）。Source bytes frozen and audited / a starting point accepted without proof (Lean Complete v1 uses three) / Lean's “skip for now” placeholder (absent from the source). |
| structural-validitystructural-validity | n、k 与 CSS 条件的机器证书；每个实例都有。The machine certificate of n, k and the CSS condition; every instance has one. |
| small-exact-distance-enumerationsmall-exact-distance-enumeration | 逐行表证书类；门槛候选数 ≤ 65 536，且只为 verified 的精确码距声明生成。The line-by-line certificate class; gated at ≤ 65 536 candidates and generated only for verified exact-distance claims. |
| distance-upper-bound@1distance-upper-bound@1 | 把一条见证封成证书的类，载荷 {upper: u}，「proves only d ≤ u」。The class sealing one witness into a certificate, payload {upper: u}, “proves only d ≤ u”. |
| unsupported，不是 falseunsupported, not false | 超出政策门的声明被标为「不支持」，不是「错」。A claim beyond the policy gate is marked “unsupported”, not “wrong”. |
| 对偶（dual）dual | 线性规划下界的证书：每条约束一个非负乘数，加权相加读出下界；核对只需乘加。The certificate of an LP lower bound: one non-negative multiplier per constraint, weighted sum reading off the bound; checking needs only multiply-and-add. |
| discharges / 不改写来源discharges / no origin rewrite | 证书通过后记入的已核对命题清单；证据词不因此自动改变。The list of checked propositions a passing certificate is recorded in; the evidence word does not change automatically. |
| 对易 / 反对易 / 碰撞commute / anticommute / collision | 一个比特上两字母都不是 I 且不同算一次碰撞；整串碰撞数偶数则对易（检查看不见），奇数则反对易（触发警报）。A position where both letters are non-I and different is a collision; an even total means the strings commute (the check cannot see it), odd means they anticommute (the alarm fires). |
| 字典序dictionary (lexicographic) order | 先比第一个编号，相同再比第二个：{1,2}、{1,3}、{2,3}。契约的顺序是先按重量、同重量内再按字典序（1.3 节），所以三比特表的顺序是 {1}、{2}、{3}、{1,2}、{1,3}、{2,3}；单纯的字典序会把 {1,2} 排在 {2} 之前。Compare the first index, on a tie the second: {1,2}, {1,3}, {2,3}. The contract's order is weight first, then dictionary order within each weight (1.3), so the three-bit table runs {1}, {2}, {3}, {1,2}, {1,3}, {2,3}; plain dictionary order would put {1,2} before {2}. |
| 证据词 verified / boundedevidence word verified / bounded | QEC-Bank 给每个数标的来源：上下两半都由机器算出 / 上界来自机器找到的见证、下界引自论文。The QEC-Bank label for where a number comes from: both halves computed by machine / upper half from a machine-found witness, lower half cited from a paper. |
| 线性规划linear programming | 在一组一次不等式划出的区域里求一个一次式的最小值；它的对偶给出可以只用乘加核对的下界。Minimising a first-degree expression over a region cut out by first-degree inequalities; its dual gives a lower bound checkable with multiplication and addition alone. |
| 退化degeneracy | 能纠正的两个不同错误对码字作用相同（两者之积是非恒等的检查乘积）；码距版说法：有比 d 轻的非恒等检查乘积。toric_L3 不退化（最轻 4 > d = 3），toric_L5 退化（最轻 4 < d = 5）。Two different correctable errors act identically on the codewords (their product is a nonidentity check product); distance version: some nonidentity check product is lighter than d. toric_L3 is nondegenerate (lightest 4 > d = 3), toric_L5 degenerate (lightest 4 < d = 5). |
延伸阅读Further reading
- QEC-Bank: the Wanted items
wanted/certified-lower-bounds.yaml（六个字段的原文；related 为空，无论文引用）与 wanted/lean-qec.yaml（partial 项，L1 的现状与四类已接受证书）。这道题的 yaml 没有列出任何论文，本篇因此不引任何论文。wanted/certified-lower-bounds.yaml (the six fields verbatim; related empty, no paper cited) and wanted/lean-qec.yaml (the partial item, the state of L1 and the four accepted classes). The problem's yaml lists no paper, so this guide cites none. - QEC-Bank: the contract and the sealed checker
docs/design-references/2026-08-21-atlas-formal-ir-v1-contract.md（两种分类、排序规则、65 536 门与其来源、「unsupported, not false」、「Supplying a rank integer alone is not a certificate」）；docs/design-references/2026-08-21-t195-lean-complete-v1-result.md（封存、三条公理、「does not accept …」清单）；formal/ir/README.md（默认验证不调用 Lean 与网络）。docs/design-references/2026-08-21-atlas-formal-ir-v1-contract.md (the two classifications, the ordering rule, the 65 536 gate and its origin, “unsupported, not false”, “Supplying a rank integer alone is not a certificate”); docs/design-references/2026-08-21-t195-lean-complete-v1-result.md (sealing, three axioms, the “does not accept …” list); formal/ir/README.md (default verification invokes neither Lean nor the network). - QEC-Bank: the ladder and the small-n witnesses
docs/superpowers/specs/2026-07-04-qec-atlas-design.md 第 11 节（L1–L4 的定义，「Hard and open: certified distance lower bounds beyond small-n exhaustion」）；codes/surface/pedagogy/distance-proof.md（L3 的机器见证与 L5 的 bounded 记录）；codes/bivariate_bicycle/instances.yaml、codes/surface/instances.yaml（本篇表中的 [[n,k,d]] 与证据词）。docs/superpowers/specs/2026-07-04-qec-atlas-design.md section 11 (the L1–L4 definitions, “Hard and open: certified distance lower bounds beyond small-n exhaustion”); codes/surface/pedagogy/distance-proof.md (L3's machine witnesses and L5's bounded record); codes/bivariate_bicycle/instances.yaml, codes/surface/instances.yaml (the [[n,k,d]] and evidence words in this guide's tables).
状态原文：open；难度原文：open-research。逐字引用的：statement、why_it_matters、current_proxy（第 1、2、3 章的框），lean-qec 的 statement 与 current_proxy 片段，契约与 T195 文件的引句，设计规范第 11 节的 L1–L4 句子，distance-proof.md 第 4 节的三行见证。QEC-Bank 自己的数：65 536、三条公理、四类证书、五个实例的 [[n,k,d]] 与证据词。本篇自己算的、QEC-Bank 页面上没有的数：741、1 431、64 875、8 498 193、≈ 1.7 × 1021、倍数 2.6 × 1016、6 行、18 与 153 行、112 791 与 225 582、182、15 750、≈ 2.0 × 1016，以及 102–104：这是局部检查约束条数的假设性计数，一份完整证书的长度没有计算（4.2 节）。本篇临时取名、QEC-Bank 契约里不存在的：distance-lower-bound。只陈述、未证明、超出高中数学的：线性规划对偶定理、Lean 的内部工作方式。没有在本机运行 Lean、QEC-Bank 验证器或任何搜索。
Status verbatim: open; difficulty verbatim: open-research. Quoted word for word: statement, why_it_matters, current_proxy (the boxes of Chapters 1, 2, 3), the statement and current_proxy fragments of lean-qec, the sentences from the contract and T195 files, the L1–L4 sentences of design-spec section 11, the three witness lines of distance-proof.md section 4. QEC-Bank's own numbers: 65 536, three axioms, four certificate classes, the [[n,k,d]] and evidence words of five instances. Computed for this guide and absent from QEC-Bank pages: 741, 1 431, 64 875, 8 498 193, ≈ 1.7 × 1021, the factor 2.6 × 1016, 6 lines, 18 and 153 lines, 112 791 and 225 582, 182, 15 750, ≈ 2.0 × 1016, and 102–104, a hypothetical count of local check constraints; the length of a complete certificate was not computed (section 4.2). Coined by this guide and absent from the QEC-Bank contract: distance-lower-bound. Stated only, not proved, beyond high-school mathematics: LP duality and Lean's inner workings. Neither Lean, the QEC-Bank verifier nor any search was run on this machine.
开放问题总览 · 大码的码距：便宜的上界，昂贵的下界 · 一张机器能核对的「没有更轻逻辑算符」证书（本篇） · 同一个码穿不同的衣服 · 拓扑替我们算出门 · 有些码还没有「标准译码器」 · 用费米子的语言写电路 · 检查每一轮都在变，码距该怎么数 · 从理想症状到真实电路 · 两张测量时间表是不是同一回事 · 不在乎的比特，与穿了衣服的码距 · 在 Wanted 板上查看 →
All open problems · Distance for large codes: cheap upper bounds, expensive lower bounds · A machine-checkable certificate that nothing lighter exists (this guide) · The same code in different clothes · Topology computes the gates · Some codes still have no standard decoder · Writing circuits in the language of fermions · When the checks change every round, how do you count distance? · From ideal syndromes to real circuits · Are two measurement schedules the same thing? · Don't-care qubits and the dressed distance · See it on the Wanted board →
Surface Code · 条目总览（形式化 1.1：证书 = 数据 + 检查器 · 3.2：逐行表 · 3.3：为什么 L5 没有） · BB 码 · 条目总览（形式化 3.2：1 431 个候选 · 3.4：seed 5 的见证是什么，不是什么） · 《从高考数学到 Toric Code》4.4：稳定子 · 2.3：奇偶检查
Surface Code · Entry overview (formal 1.1: certificate = data + checker · 3.2: the line-by-line table · 3.3: why L5 has none) · BB codes · Entry overview (formal 3.2: 1 431 candidates · 3.4: what the seed-5 witness is and is not) · “From Exam Maths to the Toric Code” 4.4: stabilizers · 2.3: parity checks