大码的码距：
便宜的上界，昂贵的下界 Distance for large codes:
cheap upper bounds, expensive lower bounds

记号：n = 物理量子比特数，k = 逻辑量子比特数，d = 码距，L = 环面的边长（每行每列的格数）。Toric Code 教程的 4.4 节里 k 记的是独立检查条数；本篇和 QEC-Bank 一样，k 直接记逻辑比特数。

Notation: n = number of physical qubits, k = number of logical qubits, d = distance, L = side length of the torus (cells per row and per column). In section 4.4 of the toric-code guide k counted independent checks; here, as in the QEC-Bank, k counts logical qubits directly.

取 L = 3 的环面码。QEC-Bank 把它登记为 BB 条目的第二个实例，标签 toric_L3，名片是 [[18, 2, 3]]双方括号是量子码的记法：n = 18 个物理比特，k = 2 个逻辑比特，码距 d = 3。三个数在 QEC-Bank 的 instances.yaml 里都标 verified。：18 条边上各住一个量子比特，9 个顶点各配一条星检查（X 型），9 块面各配一条面检查（Z 型），存 2 个逻辑比特。下面的沙盘就是它。先做一件事：沿着某一行，把那一行的 3 条横边全点上 Z 错误。

Take the toric code with L = 3. The QEC-Bank registers it as the second instance of the BB entry under the label toric_L3, with calling card [[18, 2, 3]]Double brackets denote a quantum code: n = 18 physical qubits, k = 2 logical qubits, distance d = 3. All three numbers are marked verified in the QEC-Bank instances.yaml.: one qubit on each of 18 edges, a star check (X type) at each of 9 vertices, a plaquette check (Z type) on each of 9 faces, storing 2 logical qubits. The sandbox below is that code. Do one thing first: pick a row and put a Z error on all 3 horizontal edges of that row.

没有一盏灯亮。为什么：那一行的每个顶点恰好碰到这条链的两条边（左一条、右一条），2 是偶数，星检查安静；别的顶点一条都碰不到。这条链没有端点，因为在环面上，第 3 条边绕回来接上了第 1 条。它也不是面检查的乘积，因为它绕了环面一圈，收缩不掉（5.6 节的缠绕圈）。所以它是一条逻辑算符，重量 3。人话：三个比特上的操作就能改写逻辑信息而不触发任何警报。

No lamp lights. Why: every vertex on that row touches exactly two edges of the chain (one to its left, one to its right), 2 is even, the star stays quiet; no other vertex touches any. The chain has no endpoints because on the torus the 3rd edge wraps around and joins the 1st. Nor is it a product of plaquette checks, because it winds around the torus and cannot be shrunk (the winding loop of section 5.6). So it is a logical operator of weight 3. In plain words: an operation on three qubits can rewrite the logical information without raising a single alarm.

码距 d 是所有逻辑算符中最轻那条的重量。你刚找到一条重量 3 的，于是最轻的那条不可能比 3 重：d ≤ 3。这叫一条上界upper bound：一个保证「真值不超过它」的数。对码距来说，任何一条找到的逻辑算符的重量都是上界。。注意你并没有证明 d = 3——也许还有一条重量 2 的你没看见。上界的价格：一个例子。谁找到一条逻辑算符，谁就拿到了一条上界，不需要任何别的论证。Wanted 板原文把这一半叫「cheap」，就是这个意思。

The distance d is the weight of the lightest logical operator among all of them. You just found one of weight 3, so the lightest cannot be heavier than 3: d ≤ 3. This is an upper boundA number guaranteed to be no smaller than the true value. For the distance, the weight of any logical operator you find is an upper bound.. Note that you have not shown d = 3: there might be a weight-2 one you have not noticed. The price of an upper bound: one example. Whoever finds a logical operator holds an upper bound, no further argument needed. When the Wanted board calls this half “cheap”, that is what it means.

记号：w = 某条泡利串的重量，即它触碰的比特数；⇒ 读「推出」。

Notation: w = the weight of a Pauli string, the number of qubits it touches; ⇒ reads “implies”.

现在要说反过来的话：「不存在重量 1 或 2 的逻辑算符」，也就是 d ≥ 3，一条下界lower bound：一个保证「真值不小于它」的数。对码距来说，它等价于「所有更轻的泡利串都不是逻辑算符」。。这句话不能靠一个例子，它是关于所有轻串的断言。最笨也最可靠的办法叫穷举exhaustive enumeration：把所有候选一个不漏地列出来，逐个检查。QEC-Bank 的方法名是 exact-css-enum。：把重量 1 和 2 的串全部列出来，逐个验证「要么触发某条警报，要么本身就是检查的乘积」，两者之一成立它就不是逻辑算符。先只数纯 Z 串（每个比特上要么放 Z 要么不放）：

Now we want the converse: “no logical operator of weight 1 or 2 exists”, that is d ≥ 3, a lower boundA number guaranteed to be no larger than the true value. For the distance, it is equivalent to “every lighter Pauli string fails to be a logical operator”.. No single example can establish this; it is a statement about all light strings. The dumbest and most reliable method is exhaustionListing every candidate without omission and checking each one. The QEC-Bank method name is exact-css-enum.: list every string of weight 1 and 2 and verify for each that it either trips some alarm or is itself a product of checks; either way it is not a logical operator. Count pure-Z strings first (each qubit either carries a Z or does not):

记号：C(n, w) 读「n 选 w」，是从 n 个比特里挑出 w 个的方法数（组合数）：C(18, 1) = 18，C(18, 2) = 18 × 17 ÷ 2 = 153。

Notation: C(n, w), read “n choose w”, is the number of ways to pick w of n qubits (a binomial coefficient): C(18, 1) = 18, C(18, 2) = 18 × 17 ÷ 2 = 153.

171 条纯 Z 串，再加同样多的纯 X 串（把星和面的角色对换），共 342 条。每条要做的事都在 Toric Code 教程的能力之内：数它的端点。一下午可以手算完。QEC-Bank 的 Python 验证器（qeclib/distance.py 里的 exact_distance）做的正是这件事的机器版：从重量 1 开始，对每个重量列出全部纯 X 串和纯 Z 串，检查它是否与对面那一族检查全部对易、且不是本族检查的乘积；第一次找到就停下，返回 (3, "exact-css-enum")。这就是 instances.yaml 里 toric_L3 那行 d, exact: 3, verified 的来历。

171 pure-Z strings, plus as many pure-X strings (swap the roles of stars and plaquettes), 342 in all. What must be done for each is within the toric-code guide's means: count its endpoints. An afternoon's hand work. The QEC-Bank Python verifier (exact_distance in qeclib/distance.py) does the machine version of exactly this: starting at weight 1, for each weight it lists every pure-X and pure-Z string, tests whether it commutes with the whole opposite family of checks and is not a product of its own family, and stops at the first hit, returning (3, "exact-css-enum"). That is where the line d, exact: 3, verified for toric_L3 in instances.yaml comes from.

QEC-Bank 的 BB 条目还有一个实例：gross，[[144, 12, 12]]（BB 参数教程的实例表）。同样的两件事在它身上价格如何？上界仍然便宜：QEC-Bank 的搜索程序在 144 个比特上找到了一条重量 12 的逻辑算符（第 2 章细讲）。下界呢？纯 Z 串一共有 2ⁿ 条（每个比特「放或不放」两种选择，n 个比特连乘）：

The QEC-Bank BB entry has one more instance: gross, [[144, 12, 12]] (the instance table of the BB parameters guide). What do the same two tasks cost there? The upper bound stays cheap: the QEC-Bank search program found a weight-12 logical on 144 qubits (Chapter 2 has the details). The lower bound? Pure-Z strings number 2ⁿ in all (two choices per qubit, “Z or not”, multiplied over n qubits):

记号：2ⁿ = 2 自乘 n 次；10⁴³ = 1 后面 43 个零。两个数都是本篇算的，不在 QEC-Bank 页面上。

Notation: 2ⁿ = 2 multiplied by itself n times; 10⁴³ = a 1 followed by 43 zeros. Both numbers were computed for this guide and appear on no QEC-Bank page.

当然不必数全部串，只需数重量小于 d 的。但 gross 的 d = 12，重量 1 到 11 的纯 Z 串仍有 C(144,1) + … + C(144,11) ≈ 1.0 × 10¹⁶ 条（一亿亿条），若像验证器那样 X、Y、Z 都算，是约 1.7 × 10²¹ 条。按 1.3 节手算的速度（一下午 342 条，约 40 秒一条），仅纯 Z 串就要约 3 个地球年龄；换成每秒核对十亿条的计算机，纯 X、纯 Z 串合起来约 8 个月，X、Y、Z 都算约 5 万年。对 gross 这还是「很贵」而不是「不可能」；可是再大一号，穷举就真的不可能了：BB 家族里的 [[288, 12, 18]]，重量 1 到 17 的纯型串约 2.4 × 10²⁷ 条，同一台计算机要约 8 × 10¹⁰ 年。（穷举不可能，不等于这两个码的 d 没人算过：2.3 节会说，Bravyi 等人用整数规划算出了它们的码距。）这就是 Wanted 板说「the lower bound is the open half」的算术背景。可以正式念题了。

Of course one need not count every string, only those of weight below d. But gross has d = 12, and pure-Z strings of weight 1 through 11 still number C(144,1) + … + C(144,11) ≈ 1.0 × 10¹⁶ (ten million billion); counting X, Y and Z as the verifier does, about 1.7 × 10²¹. At the hand speed of 1.3 (342 strings an afternoon, about 40 s each) the pure-Z strings alone would take about 3 ages of the Earth; a computer checking a billion candidates per second needs about 8 months for the pure-X and pure-Z strings together and about 50 000 years counting X, Y and Z. For gross that is “very expensive” rather than “impossible”; one size up, exhaustion becomes impossible: for the BB family's [[288, 12, 18]] the pure strings of weight 1 to 17 number about 2.4 × 10²⁷, about 8 × 10¹⁰ years on the same computer. (Exhaustion being impossible does not mean nobody has computed these two distances: 2.3 explains that Bravyi et al. computed them by integer programming.) That is the arithmetic behind the board's phrase “the lower bound is the open half”. We can now read the problem statement.

逐词翻译。qLDPC：量子低密度奇偶检查码——每条检查只碰少数几个比特、每个比特只被少数几条检查碰的量子码；环面码（每条检查碰 4 个）和 gross（每条碰 6 个）都是（qLDPC 教程 1.2 节）。n >~ 100：一百个左右及以上的比特，穷举开始失效的地方。beyond exhaustive range：超出能逐个列举的范围。Exactness NOT required：不要求算出 d 的精确值，只要一条有证明的下界就算完整答案。relaxation-based … LP/SDP-style, symmetry-reduced, spectral/expansion：几种可能的证明路线的名字，第 4 章逐个解释。人话：我们不缺「找到一条」的方法，缺的是「证明没有更轻的」的方法，而且只要下界，不要精确值。

Word by word. qLDPC: quantum low-density parity-check codes, where each check touches only a few qubits and each qubit is touched by only a few checks; the toric code (4 per check) and gross (6 per check) both qualify (qLDPC guide section 1.2). n >~ 100: about a hundred qubits and up, where exhaustion starts to fail. beyond exhaustive range: past what can be listed one by one. Exactness NOT required: the exact value of d is not demanded; a proven lower bound alone counts as a full answer. relaxation-based … LP/SDP-style, symmetry-reduced, spectral/expansion: names of possible proof routes, explained one by one in Chapter 4. In plain words: we do not lack ways to find one; we lack ways to prove nothing lighter exists, and only the lower bound is asked for, not the exact value.

就是 1.3 节你手算的那件事的机器版，方法名 exact-css-enum。它给出的是精确值——上界与下界同时到手，因为它一路排除到 d − 1，又在 d 处亲手找到一条。QEC-Bank 里靠它拿到 verified 的实例，本系列教程遇到过这些：

This is the machine version of what you did by hand in section 1.3, method name exact-css-enum. It yields the exact value: upper and lower bound arrive together, because it excludes everything up to d − 1 and then finds one at d. The instances that earn verified this way, among those this series has met:

注意 n 的范围：18、13、25。表面码的 L3 是 Toric Code 剪开后的平面版，13 个比特。验证器的穷举函数默认只搜到重量 8（w_max = 8），超过就报「无法验证」而不是猜一个数。人话：能数得完的，QEC-Bank 就数完并写 verified；数不完的，绝不冒充。

Note the range of n: 18, 13, 25. Surface L3 is the toric code cut open into a planar patch, 13 qubits. The verifier's exhaustion routine searches only up to weight 8 by default (w_max = 8); beyond that it reports “unverifiable” rather than guessing. In plain words: what can be counted to the end, the QEC-Bank counts to the end and writes verified; what cannot, it never fakes.

rand-lowweight-v1QEC-Bank 的种子化随机搜索：从随机起点出发反复尝试，寻找尽量轻的逻辑算符；参数 seed（随机数种子）和 iters（尝试次数）写进登记，保证任何人重跑都得到同一条。 是一个随机搜索程序：反复从随机起点出发，试着把一条逻辑算符越改越轻，记下找到的最轻那条。它的登记带两个参数：seed（随机数发生器的起始数，定了它，「随机」就变成可以一字不差重跑的确定过程）和 iters（尝试的轮数）。它能给的只有 1.2 节那种东西：一条找到的逻辑算符，一条上界。它对「有没有更轻的」不置一词。QEC-Bank 有两个实例靠它撑起上界：

rand-lowweight-v1The QEC-Bank's seeded random search: it starts from random points repeatedly, looking for the lightest logical it can; the parameters seed (random-number seed) and iters (number of attempts) are recorded so that anyone rerunning it gets the same operator. is a random search program: again and again it starts from a random point, tries to make a logical operator lighter and lighter, and records the lightest it found. Its record carries two parameters: seed (the starting number of the random-number generator; fixing it turns “random” into a deterministic procedure anyone can rerun to the letter) and iters (the number of rounds). All it can give is the object of section 1.2: one found logical, one upper bound. It says nothing about whether anything lighter exists. Two QEC-Bank instances rest their upper bound on it:

两行都抄自各自的 instances.yaml。bravyi2024bicycle = Bravyi、Cross、Gambetta、Maslov、Rall、Yoder，“High-Threshold and Low-Overhead Fault-Tolerant Quantum Memory”（2024）；dennis2002topological = Dennis、Kitaev、Landahl、Preskill，“Topological quantum memory”（2002）。两篇都在 QEC-Bank 的参考文献登记表 registry/refs.yaml 里。

Both rows are copied from the respective instances.yaml. bravyi2024bicycle = Bravyi, Cross, Gambetta, Maslov, Rall and Yoder, “High-Threshold and Low-Overhead Fault-Tolerant Quantum Memory” (2024); dennis2002topological = Dennis, Kitaev, Landahl and Preskill, “Topological quantum memory” (2002). Both are registered in the QEC-Bank reference registry registry/refs.yaml.

上表的「下界」一列是第三样工具。bounded 这个词的准确含义（BB 参数教程 3.3 节、表面码参数教程 3.3 节）：上界是机器自己重跑出来的，下界是引用一篇论文；两半的数字恰好相等，所以 d 的值是确定的，但两半的来源不同。（子系统码的账本里还有只有上界一半、没有任何下界的 bounded，见不在乎的比特 · 2.3 节；那里会注明 upper-bound-only。）两个实例的引文性质还不一样，值得分清：

The “lower half” column of the table above is the third tool. The precise meaning of bounded (BB parameters guide 3.3, surface parameters guide 3.3): the upper half is rerun by the machine itself, the lower half cites a paper; the two halves happen to agree, so the value of d is settled, but the two halves have different sources. (The subsystem-code ledger also has bounded entries with an upper half only and no lower bound at all, see Don't-care qubits · 2.3; those are marked upper-bound-only.) The two citations are of different natures, worth separating:

表面码 L5。下界 d ≥ 5 有一个对所有 L 成立的纸上定理：QEC-Bank 自己的推导页 codes/surface/pedagogy/distance-proof.md 写出了证明——L 条互不相交的竖列，每一条与 Z 类反对易的算符都必须在每一列上至少落一个脚，所以至少 L 个比特。（第 5 章会把这个论证的 L = 3 版本教给你。）也就是说，人类知道为什么，只是机器没有逐条核对这个论证。所以 L5 的 bounded 缺的不是「找到下界的方法」，而是「让机器相信一个论证的方法」，那是证书篇的题目。

Surface L5. The lower bound d ≥ 5 has a paper theorem valid for every L: the QEC-Bank's own derivation page codes/surface/pedagogy/distance-proof.md writes out the proof, using L pairwise disjoint columns, each operator anticommuting with the Z class having to set at least one foot on every column, hence at least L qubits. (Chapter 5 teaches you the L = 3 version of this argument.) In other words humans know why; only the machine has not checked the argument line by line. So what L5's bounded lacks is not “a way to find the lower bound” but “a way to make a machine believe an argument”, which is the topic of the certificate guide.

gross。QEC-Bank 只登记了引文 bravyi2024bicycle，没有登记论文用什么方法得到 d ≥ 12，也没有重放。论文本身写明了方法：它的表 3（BB 码实例表，gross 在其中）的注释说 “Code distance was computed by the mixed integer programming approach of Ref. [55]”（[55] 是 Landahl、Anderson、Rice 的 arXiv:1108.5738），第 6 节又说候选码先用一个随机的 BP-OSD 上界筛选，“The actual distance of each candidate code was computed using the integer linear programming method [55]”。整数规划integer programming：把问题写成「若干个取整数值（这里是 0 或 1）的变量、若干条一次等式或不等式、求一个一次函数的最小值」，交给专门的求解程序。求解器用分支定界系统地排除大片候选；只有当它证明了最优（上下界之差为零）、而且数值容差没有出问题时，报告的才是精确的最小值。就是把「每个比特放不放」写成 0/1 变量、把「骗过所有检查而且是非平凡逻辑算符」写成一次约束（4.3 节有一个三变量的小例子），让求解器求最小重量。要把结果当作精确的 d，需要两样东西：一个重量为 d 的可行解（见证），加上一个排除所有更小整数重量的、经过验证的下界；求解器报告「最优、间隙为零」就是在声称后者。所以 gross 的 d = 12 是论文报告的一次精确计算结果，不只是一句断言。能确定缺的是另一件事：QEC-Bank 的机器没有自己排除过重量 11 及以下的候选，也没有一份它能核对的证书——整数规划求解器是一个很大的程序，它的「跑完了、最优值是 12」要靠信任这个程序，而不是一份任何人都能用加法和乘法复核的数据；这种计算能否推广到更大的码、能否被 QEC-Bank 重放，也都还没有答案。这一半就是 Wanted 板上「open」的那一半。

gross. The QEC-Bank registers only the citation bravyi2024bicycle; it does not register how the paper obtained d ≥ 12, nor does it replay it. The paper itself states its method: the note to its Table 3 (the table of BB instances, gross among them) says “Code distance was computed by the mixed integer programming approach of Ref. [55]” ([55] is Landahl, Anderson and Rice, arXiv:1108.5738), and its section 6 says candidate codes were first screened with a randomized BP-OSD upper bound and that “The actual distance of each candidate code was computed using the integer linear programming method [55]”. Integer programmingWriting a problem as “some variables taking integer values (here 0 or 1), some first-degree equations or inequalities, minimize a first-degree function”, and handing it to a dedicated solver. The solver excludes large groups of candidates systematically by branch and bound; what it reports is the exact minimum only when it has proved optimality (a zero gap between its upper and lower bounds) and its numerical tolerances did not interfere. means writing “a Z or not on each qubit” as 0/1 variables and “passes every check and is a nontrivial logical” as first-degree constraints (4.3 has a three-variable example), then letting a solver minimize the weight. Taking the result as the exact d needs two things: a feasible solution of weight d (the witness) and a validated lower bound excluding every smaller integer weight; a solver reporting “optimal, zero gap” is claiming the latter. So gross's d = 12 is the paper's reported exact result of an actual computation, not just an assertion. What is missing is something else: the QEC-Bank machine has not itself shown that every string of weight 11 and below is either detected or a mere product of checks (stabilizers are silent and allowed; what must be excluded is nontrivial logicals), and it has no certificate it can check: an integer-programming solver is a large program, and its “finished, the optimum is 12” rests on trusting that program, not on data anyone can recheck with additions and multiplications; whether such computations scale to larger codes and whether the QEC-Bank can replay them are also open. That half is the “open” half on the board.

板上没提、但账本里常见的还有一种：claimed——照抄文献，机器连上界也没算。gross 的四个亲戚就是：[[72,12,6]]、[[90,8,10]]、[[108,8,10]]、[[288,12,18]]，各住在 QEC-Bank 的条目 bb72、bb90、bb108、bb288 里，d 全是 claimed（BB 参数教程 4.1 节的八张卡；BB 直觉教程 4.4 节讲了「两份证书」的概念）。下面这张现场账本把这一家人排在一起，看「证据」一列：只有 toric_L3 和 bb5 是穷举出来的。点「再加低重搜索」，浏览器会在几秒钟内替每个码找一条尽量轻的逻辑算符——你会亲眼看到那只是一个上界，而且常常比文献值还松。

One more situation, absent from the board but common in the ledger: claimed, copied from the literature with not even an upper bound computed by machine. Gross's four relatives are exactly this: [[72,12,6]], [[90,8,10]], [[108,8,10]], [[288,12,18]], living in the QEC-Bank entries bb72, bb90, bb108, bb288, all with d claimed (the eight cards of BB parameters guide 4.1; BB intuition guide 4.4 introduces the “two certificates” idea). The live ledger below lines the family up; look at the “evidence” column: only toric_L3 and bb5 are exhausted. Press “Also run the low-weight search” and the browser will look for the lightest logical it can for each code within seconds; you will see with your own eyes that this is only an upper bound, often looser than the literature value.

gross 的 d 记录今天是 lower: 12（引文）· upper: 12（机器）· origin: bounded。若有了一台能在 n = 144 上给出「没有重量 ≤ 11 的逻辑算符」并附证明的机器，下界一半就从「引文」变成「机器」，两半齐了，这个字段的词就从 bounded 翻成 verified。别的数字一个都不用改——12 还是 12——变的只是我们对它的把握程度。「and beyond」说的是：同一台机器会对每一个 n ≈ 100 以上的条目做同样的事，不只 gross。

Today gross's d record reads lower: 12 (citation) · upper: 12 (machine) · origin: bounded. Given a machine that at n = 144 delivers “no logical of weight ≤ 11” with a proof attached, the lower half turns from “citation” into “machine”, both halves are in, and the word on the field flips from bounded to verified. Not one other number changes, 12 stays 12; what changes is how firmly we hold it. “And beyond” means the same machine would do the same for every entry with n around 100 or more, not only gross.

值得强调什么不会翻。表面码 L5 的下界有定理撑着，但这道题的机器也不会自动把它翻成 verified——除非那台机器的输出被写成机器能核对的证书。找到下界与写下证书是两道题，本系列分成两篇（证书篇）。

Worth stressing what would not flip. Surface L5's lower bound rests on a theorem, yet this problem's machine would not automatically flip it to verified either, unless the machine's output is written as a certificate a checker can verify. Finding the bound and writing the certificate are two problems, and this series treats them in two guides (the certificate guide).

QEC-Bank 拿 BB 码和表面码比较时用的数是 k·d²/n（BB 参数教程 5.1 节）：gross 是 12 × 12² ÷ 144 = 12；表面码的数取决于变体和数比特的约定：旋转的表面码补丁（rotated patch）只数数据比特时 n = d²，k·d²/n = 1，于是有「十二倍」的说法；QEC-Bank 登记的未旋转实例 L5 是 n = 5² + 4² = 41、k = 1、d = 5，给出 25/41 ≈ 0.61。这个数里 d 是平方出现的。假如 gross 的真实码距其实是 11（也就是说，论文的下界错了，存在一条重量 11 的逻辑算符），这个数就变成 12 × 11² ÷ 144 ≈ 10.1。本篇不认为论文错了；要说的是，比较表的每一格都把引文当成了事实，而 QEC-Bank 的整套设计是让机器替读者核对事实。只要下界还是引文，比较表就只能诚实地写 bounded；四个亲戚的格子更只能写 claimed。板上那句「comparison tables stay bounded/claimed」说的就是这张表。

When the QEC-Bank compares BB codes with surface codes it uses k·d²/n (BB parameters guide 5.1): gross gives 12 × 12² ÷ 144 = 12; for the surface code the number depends on the variant and on which qubits are counted: a rotated patch counting only data qubits has n = d², so k·d²/n = 1, hence the “twelve-fold” phrase; the unrotated instance L5 registered in the QEC-Bank has n = 5² + 4² = 41, k = 1, d = 5, giving 25/41 ≈ 0.61. In that number d appears squared. If gross's true distance were in fact 11 (that is, if the paper's lower bound were wrong and a weight-11 logical existed), the number would become 12 × 11² ÷ 144 ≈ 10.1. This guide does not suggest the paper is wrong; the point is that every cell of the comparison table treats a citation as a fact, whereas the whole design of the QEC-Bank is to have the machine check facts for the reader. As long as the lower half is a citation the table can only honestly say bounded, and the four relatives' cells only claimed. That table is what the board's “comparison tables stay bounded/claimed” refers to.

记号：k·d²/n 读「k 乘 d 平方除以 n」，是 QEC-Bank 用来比较码「性价比」的数；10.1 这个数是本篇按公式算的假设值，不是 QEC-Bank 的记录。

Notation: k·d²/n, read “k times d squared over n”, is the figure of merit the QEC-Bank uses to compare codes; 10.1 is a hypothetical computed for this guide from the formula, not a QEC-Bank record.

想象一个 QEC-Bank 用户要选一个码去做实验，条件是「d ≥ 10，而且 d 必须是 verified 的」。今天他会两手空空：本系列遇到的 BB 家族的 verified 码距里，最大的 n 是 bb5 的 30（[[30,4,5]]，BB 参数教程 4.1 节），d 只有 5；QEC-Bank 全库里 d 小的大码另有 verified 的例子（量子扩展码 [[125,37,3]]，d = 3），同样满足不了 d ≥ 10。所有 d ≥ 10 的码——gross、bb90、bb108、bb288——旁边的词不是 bounded 就是 claimed。他要么放宽条件接受引文，要么自己去读论文重做证明。QEC-Bank 想替他省下的正是第二件事。人话：没有这道题的答案，QEC-Bank 在最有用的那一段（大码）只能当一本带注释的文献索引，当不了一台核对机。

Imagine a QEC-Bank user choosing a code for an experiment with the condition “d ≥ 10, and d must be verified”. Today they come away empty-handed: of the BB-family verified distances this series has met, the largest n is 30, for bb5 ([[30,4,5]], BB parameters guide 4.1), with d only 5; elsewhere in the QEC-Bank a large code with small d is verified (the quantum expander [[125,37,3]], d = 3), which fails d ≥ 10 just the same. Every code with d ≥ 10, gross, bb90, bb108, bb288, carries bounded or claimed beside it. The user must either relax the condition and accept citations, or go read the papers and redo the proofs. The second is exactly what the QEC-Bank wants to spare them. In plain words: without this problem's answer, the QEC-Bank can only be an annotated bibliography in its most useful range, large codes, and not a checking machine.

合格的答案是一个程序，输入 gross 的检查矩阵（或任何 n ≈ 100 以上的 qLDPC 码），输出两样东西：一个数 w，和一份证明「没有任何重量小于 w 的逻辑算符」。对 gross 来说 w = 12 最理想，但 w = 10 也是合格的答案——它把下界一半从引文换成了机器，只是可能比论文的数松一点。不要求同时找到精确值：上界一半 QEC-Bank 已经有了。人话：要的是「保证没有更轻的」的机器，哪怕保证得保守一点。

A qualifying answer is a program that takes the check matrices of gross (or any qLDPC code with n around 100 or more) and outputs two things: a number w, and a proof that “no logical operator of weight below w exists”. For gross, w = 12 would be ideal, but w = 10 is also a qualifying answer: it replaces the lower half's citation by a machine, merely a little looser than the paper's number. The exact value is not demanded; the QEC-Bank already has the upper half. In plain words: what is wanted is a machine that guarantees “nothing lighter”, even if the guarantee is a bit conservative.

先看一道高中题：证明对所有正数 x，都有 x + 1/x ≥ 2。没有人会代入每一个 x——正数有无穷多个。做法是一行恒等式：x + 1/x − 2 = (√x − 1/√x)²，而平方永远 ≥ 0。这一行同时处理了所有的 x。它证明的是「最小值不小于 2」，即一条下界；并且 x = 1 处取到 2，所以这个下界还是精确的。码距问题的形状一模一样：要证「在所有骗过检查的非平凡串里，重量的最小值 ≥ 12」，我们想要的不是一亿亿次检查，而是一行能同时覆盖所有候选的论证。

A high-school exercise first: prove that x + 1/x ≥ 2 for every positive x. Nobody substitutes every x; there are infinitely many. The method is one identity: x + 1/x − 2 = (√x − 1/√x)², and a square is never negative. That one line handles every x at once. It proves “the minimum is at least 2”, a lower bound, and since x = 1 attains 2 the bound is even exact. The distance problem has the same shape: to prove “among all non-trivial strings that fool the checks, the minimum weight is ≥ 12” we want not ten million billion checks but one argument covering every candidate at once.

找这样的论证有一个通用套路，叫松弛relaxation：把「在集合 S 上求最小值」换成「在一个更大、更容易处理的集合 T ⊇ S 上求最小值」。更大的集合上的最小值不会更大，所以它是原问题的下界。。它靠一个高中生能验证的事实：范围放大，最小值只会变小或不变。一个省的最低点不会比省内任何一个市的最低点更高。所以，如果我们能证明「放大后的集合里最小值 ≥ 12」，原集合里的最小值也 ≥ 12。放大的目的是让最小值能算：原集合是「每个比特上放或不放」的离散选择，天文数字个点；放大后允许每个比特「放 0.3 个」这样的分数，集合变成一块连续的区域。光是「连续」还不够让问题好算；好算的是两类有结构的凸区域（凸 = 区域里任意两点连线上的点都还在区域里）：由有限条一次不等式围成的多面体（线性规划，LP），和「一个由变量排成的对称矩阵必须半正定」这类条件围成的区域（半定规划，SDP）。在这两类区域上求一次函数的最小值，已有随规模多项式增长的算法。还要分清一件事：求解器给出的是浮点数值结果，本身不是证明；要成为一条核对过的下界，得把它的对偶解（一组乘数）拿出来，用精确的有理数算术验证一遍，这就是证书篇 4.2 节讲的那种证书。

There is a general recipe for finding such an argument, called relaxationReplacing “minimize over the set S” by “minimize over a larger, easier set T ⊇ S”. The minimum over a larger set can only be smaller or equal, so it is a lower bound for the original problem.. It rests on a fact a high-school student can verify: enlarge the range and the minimum can only go down or stay. The lowest point of a province is never higher than the lowest point of any city inside it. So if we can prove “the minimum over the enlarged set is ≥ 12”, the minimum over the original set is ≥ 12 too. The purpose of enlarging is to make the minimum computable: the original set is the discrete choice “Z or not” per qubit, an astronomical number of points; after enlarging we allow fractions such as “0.3 of a Z” on a qubit and the set becomes a continuous region. Being continuous is not enough to make the problem easy; what is easy are two kinds of structured convex regions (convex = the segment between any two points of the region stays inside it): polyhedra bounded by finitely many first-degree inequalities (linear programming, LP), and regions cut out by the condition that a symmetric matrix built from the variables be positive semidefinite (semidefinite programming, SDP). Over these two kinds of region a first-degree function can be minimized by algorithms whose cost grows polynomially with size. One more distinction: a solver returns a floating-point number, which is not itself a proof; to become a checked lower bound its dual solution (a set of multipliers) must be taken out and verified in exact rational arithmetic, the kind of certificate described in 4.2 of the certificates guide.

记号：S = 原来的候选集合（所有骗过检查的非平凡泡利串），T = 放大后的集合，⊆ 读「包含于」，f = 要最小化的量（这里是重量），min_T f 读「f 在 T 上的最小值」，w = 我们想证明的下界。

Notation: S = the original candidate set (all non-trivial Pauli strings fooling the checks), T = the enlarged set, ⊆ reads “is contained in”, f = the quantity to minimize (here the weight), min_T f reads “the minimum of f over T”, w = the lower bound we want to prove.

代价也要说清：放大之后最小值可能真的变小。若放大得太宽松，算出来的下界也许只有 6，那对 gross 没有帮助（引文已经说 12）。松弛方法的全部技艺，就在于把 T 放得刚好够大到能算、又刚好够小到下界不塌。松弛算出的下界怎样写成一份只用乘法和加法就能核对的「对偶」证书，证书篇 4.2 节有一个三个变量、手算即可的例子。

The cost must be stated too: after enlarging, the minimum may genuinely drop. If T is too loose, the computed bound may be only 6, which is no help for gross (the citation already says 12). The whole art of relaxation lies in making T just large enough to compute and just small enough that the bound does not collapse. How a relaxation's bound becomes a “dual” certificate checkable by multiplication and addition alone is worked by hand on three variables in section 4.2 of the certificates guide.

记号：l、m = BB 码环面的宽与高（gross 为 12 与 6），l × m = 平移的总数。这一节只描述这些方法是什么，不推导它们；真正做出来是研究工作，超出高中数学。

Notation: l, m = width and height of the BB torus (12 and 6 for gross), l × m = the total number of translations. This section only describes what these methods are, without deriving them; carrying them out is research work beyond high-school mathematics.

一个三变量的例子：LP 松弛缺了什么、补上之后得到什么。取 3 比特重复码，检查 Z₁Z₂、Z₂Z₃，找最轻的 X 型逻辑错误。记 e_i = 1 表示比特 i 上有 X。骗过检查：e₁ + e₂ 与 e₂ + e₃ 都是偶数。只有这两条，e = (0, 0, 0) 就满足，最小重量是 0，什么也没证明。补上非平凡的条件：X 错误要改写逻辑比特，就必须与逻辑 Z̄ = Z₁Z₂Z₃ 反对易，即 e₁ + e₂ + e₃ 为奇数。三条模 2 条件下唯一的 0/1 解是 (1, 1, 1)，重量 3，这就是这个码对 X 错误的码距。现在松弛：把每条模 2 条件换成围住它全部 0/1 解的一次不等式（「偶数」对两个变量就是 e₁ = e₂、e₂ = e₃；「三个里奇数个」给出 e₁ + e₂ + e₃ ≥ 1 以及三条 e_i + e_j − e_k ≤ 1），再让 e_i 取 0 到 1 之间的分数。于是 e₁ = e₂ = e₃ = t，t ≥ 1/3，最小重量 3t = 1，在 (1/3, 1/3, 1/3) 取到。结论有两个：必须有「非平凡」那条约束，否则下界是 0；有了它，松弛给出的下界 1 仍比真值 3 松（若改用同一个逻辑的另一个代表 Z̄ = Z₁，约束变成 e₁ ≥ 1，松弛就给出 3——写法的选择直接影响松紧）。有 k 个逻辑比特时，「与某一个逻辑 Z̄_j 反对易」不是一条一次约束，通常对每个 j 各解一次、取最小。本篇的检验脚本在 1/60 的网格上核对了最小值 1。

A three-variable example: what the LP relaxation lacks, and what it gives once completed. Take the 3-qubit repetition code with checks Z₁Z₂ and Z₂Z₃, and look for the lightest X-type logical error. Write e_i = 1 for an X on qubit i. Passing the checks: e₁ + e₂ and e₂ + e₃ are both even. With only these two, e = (0, 0, 0) qualifies, the minimum weight is 0, and nothing is proved. Add the nontrivial condition: an X error that changes the logical qubit must anticommute with the logical Z̄ = Z₁Z₂Z₃, that is e₁ + e₂ + e₃ is odd. Under the three mod-2 conditions the only 0/1 solution is (1, 1, 1), weight 3, the code's distance against X errors. Now relax: replace each mod-2 condition by the first-degree inequalities that enclose all its 0/1 solutions (“even” on two variables is e₁ = e₂ and e₂ = e₃; “an odd number of the three” gives e₁ + e₂ + e₃ ≥ 1 and the three inequalities e_i + e_j − e_k ≤ 1), and let each e_i be a fraction between 0 and 1. Then e₁ = e₂ = e₃ = t with t ≥ 1/3, and the minimum weight 3t = 1 is reached at (1/3, 1/3, 1/3). Two conclusions: the “nontrivial” constraint is indispensable, otherwise the bound is 0; and with it the relaxation's bound 1 is still looser than the true value 3 (using the other representative Z̄ = Z₁ of the same logical turns the constraint into e₁ ≥ 1 and the relaxation gives 3, so the choice of formulation directly affects how tight it is). With k logical qubits, “anticommutes with some logical Z̄_j” is not a single first-degree constraint; one usually solves once for each j and takes the minimum. This guide's check script confirmed the minimum 1 on a grid of step 1/60.

Wanted 板给每道题标难度。hard-engineering 是「知道怎么做，但要做很多」——比如把一个已有算法接到 QEC-Bank 的验证器上。open-research 是「没人知道怎么做」：4.3 节的三条路线都是方向，不是已经在 n = 144 上给出 w = 12 的现成程序——Bravyi 等人用整数规划算出了 gross 的 d = 12（2.3 节，论文表 3 注与第 6 节），说明具体实例上做得到；开放的是可扩展、输出能被核对（可认证）、能被 QEC-Bank 重放的方法。这道题标的是 open-research。诚实地说难在哪里：

The Wanted board rates each problem's difficulty. hard-engineering means “we know how, but there is a lot to do”, such as wiring an existing algorithm into the QEC-Bank verifier. open-research means “nobody knows how”: the three routes of 4.3 are directions, not ready programs that deliver w = 12 at n = 144 — Bravyi et al. computed d = 12 for gross by integer programming (2.3; the note to the paper's Table 3 and its section 6), so single instances can be done; what is open is a method that scales, whose output can be checked (certified), and that the QEC-Bank can replay. This problem is rated open-research. Honestly, where the difficulty lies:

表中 gross 的候选数由本篇按公式 Σ_w=1¹¹ C(144, w)（纯 Z）和 Σ_w=1¹¹ C(144, w)·3^w（X、Y、Z 三选一）算出；Σ 读「西格玛」，表示把 w 从 1 到 11 的各项加起来；3^w 是 w 个选中的比特各取 X、Y 或 Z 的方法数。后一个公式是 QEC-Bank 形式化契约中的候选数公式（BB 形式化教程 3.3 节）。

The gross counts in the table were computed for this guide from Σ_w=1¹¹ C(144, w) (pure Z) and Σ_w=1¹¹ C(144, w)·3^w (X, Y or Z per qubit); Σ, read “sigma”, adds the terms for w from 1 to 11; 3^w is the number of ways the w chosen qubits can each take X, Y or Z. The second formula is the candidate-count formula of the QEC-Bank formal contract (BB formal-verification guide 3.3).

用第 0 章的事实 4：纯 Z 串是一条链，报警的星恰是链的端点。重量 1：一条边有两个端点，两盏灯必亮。重量 2：两条边若不相邻，四盏灯亮；若共用一个顶点，链的两头各是一个端点，两盏灯亮。唯一能让灯全灭的是「没有端点」，即闭合圈；而在 3 × 3 的环面上，两条边围不成圈——从一个顶点出发走一步再走一步，回不到起点，因为同一对顶点之间只有一条边。于是每一条重量 ≤ 2 的纯 Z 串都触发警报，不可能是逻辑算符。对纯 X 串把「边—顶点」换成「边—面」，一字不改地重来一遍。再加上 1.3 节折叠框里「最轻的逻辑算符总可取纯 X 或纯 Z」，得到 d ≥ 3。三句话，342 个候选全部覆盖，没有列举任何一条。

Use fact 4 of Chapter 0: a pure-Z string is a chain, and the stars that fire are exactly its endpoints. Weight 1: one edge has two endpoints, two lamps must light. Weight 2: two non-adjacent edges light four lamps; two edges sharing a vertex leave one endpoint at each end of the chain, two lamps. The only way to keep every lamp dark is “no endpoints”, a closed loop; and on the 3 × 3 torus two edges cannot close a loop, since one step and then another from a vertex never returns to it, there being only one edge between any pair of vertices. Hence every pure-Z string of weight ≤ 2 raises an alarm and cannot be a logical operator. For pure-X strings replace “edge–vertex” by “edge–face” and repeat verbatim. Add the folded box of section 1.3, “the lightest logical can always be taken pure X or pure Z”, and you have d ≥ 3. Three sentences, all 342 candidates covered, not one of them listed.

合上 1.2 节的上界，d = 3，与 QEC-Bank 的 exact: 3, verified 相符——只是 QEC-Bank 是数出来的，你是证出来的。这正是 4.2 节想要的那种东西：一个覆盖全部候选的论证。表面码的推导页 distance-proof.md 把同一个想法做成了对所有 L 成立的定理（L 条互不相交的列，每条与 Z 类反对易的算符必须踩到每一列）。那么为什么这条路没有直接解决 gross？因为它靠的是环面的几何：链、端点、圈。gross 的检查图没有这样一张能画在纸上的地图（BB 直觉教程 1.2 节：放弃局域），「两条边围不成圈」这类话在它身上没有现成的对应物。要在没有几何的图上说出「所有小集合都触发警报」，就是 4.3 节的 expansion 路线，而它至今没有在 n = 144 上给出 12。

Close with the upper bound of 1.2 and d = 3, agreeing with the QEC-Bank record exact: 3, verified, except that the QEC-Bank counted while you proved. This is exactly the kind of object 4.2 asks for: one argument covering every candidate. The surface-code derivation page distance-proof.md turns the same idea into a theorem for every L (L pairwise disjoint columns; every operator anticommuting with the Z class must step on each). So why has this route not simply settled gross? Because it leans on the geometry of the torus: chains, endpoints, loops. Gross's check graph has no such map one can draw on paper (BB intuition guide 1.2: giving up locality), and sentences like “two edges cannot close a loop” have no ready counterpart there. Saying “every small set raises an alarm” on a graph without geometry is the expansion route of 4.3, and it has not yet delivered 12 at n = 144.

下面的实验台预设为 gross。它能现场重算 n = 144 和 k = 12（那是两次高斯消元，机器擅长），也有一个低重量搜索按钮。按一下：它从固定的种子 5 出发跑满 3 000 轮（普通电脑上约 0.3 秒），找到一条重量 16 的逻辑算符，于是 d ≤ 16；读数会写出实际跑了几轮。再按还是 16：种子和轮数都固定，结果可以一字不差地重跑。这句「可重跑」只在跑满 3 000 轮时成立：为了不让很慢的机器卡住，搜索另有 10 秒的时间上限，若时间先到，读数会注明轮数不足，那时的结果可能更重，也不能拿来和别人的 16 对比。把轮数加到 10 万，同一个程序会找到 12（本篇在浏览器里跑过）；QEC-Bank 登记的 rand-lowweight-v1（seed 5、iters 2000）是 QEC-Bank 自己的另一个程序，它找到的也是 12。每找到一条你就多拿到一条上界，但无论按多少次，你都不会拿到「没有重量 11 的」这句话——这台机器在结构上就给不出它。这就是 rand-lowweight-v1 的处境，也是 Wanted 板把下界叫作「the open half」的全部理由。

The bench below is preset to gross. It recomputes n = 144 and k = 12 live (two Gaussian eliminations, which machines are good at) and has a low-weight search button. Press it once: starting from the fixed seed 5 it runs the full 3 000 rounds (about 0.3 s on an ordinary computer) and finds a logical of weight 16, so d ≤ 16; the readout states how many rounds actually ran. Press again and it is 16 again: seed and round count are fixed, so the result can be rerun exactly. That reproducibility holds only when all 3 000 rounds run: so that a very slow machine does not hang, the search also has a 10-second time limit, and if the time runs out first the readout says the round count fell short; such a result may be heavier and cannot be compared with someone else's 16. With 100 000 rounds the same program finds 12 (this guide ran it in the browser); the QEC-Bank's registered rand-lowweight-v1 (seed 5, iters 2000) is a different program of the QEC-Bank's own, and it too finds 12. Every one found hands you one more upper bound, but however many times you press you will never receive the sentence “there is no weight-11 one”; this machine is structurally unable to produce it. That is the situation of rand-lowweight-v1, and the whole reason the board calls the lower bound “the open half”.

先读懂实验台上的记号。gross 住在 12 × 6 的环面上：格点记作 (i, j)，i = 0…11 横着数，j = 0…5 竖着数（图的上方和左边标了刻度）；每个格点有一个左层比特、一个右层比特、一条 X 检查和一条 Z 检查。A = x³ + y + y² 和 B = y³ + x + x² 是两张「走法表」：单项式 x^ay^b 表示「向右走 a 格、向上走 b 格」，走出边界就从对面回来。格点 (i, j) 上的 X 检查，按 A 的三项各走一步落到三个左层比特，按 B 的三项落到三个右层比特。以格点 (0, 0) 为例：

First, the notation on the bench. gross lives on a 12 × 6 torus: sites are written (i, j), with i = 0…11 counted across and j = 0…5 counted up (the ticks are on the top and left of the picture); each site holds one left-layer qubit, one right-layer qubit, one X check and one Z check. A = x³ + y + y² and B = y³ + x + x² are two “move tables”: the monomial x^ay^b means “a steps right, b steps up”, re-entering from the opposite side at an edge. The X check at site (i, j) takes one move per term of A to reach three left-layer qubits, and one per term of B to reach three right-layer qubits. For site (0, 0):

列号 = 层 × 72 + 6i + j（左层记 0，右层记 1），与实验台见证读数里的数字同一套编号。

Column = layer × 72 + 6i + j (left layer 0, right layer 1), the same numbering as the witness readout on the bench.

把这一条检查写成一行 144 个 0/1，就是矩阵 H_X 的第 0 行：第 1、2、18、75、78、84 列是 1，其余是 0。H_X = [A | B] 说的就是「左半边 72 列由 A 决定，右半边 72 列由 B 决定」，每个格点一行。Z 检查用反方向的走法：H_Z = [Bᵀ | Aᵀ]，这里的转置 ᵀ 就是把每一步倒过来走（x³ 变成向左 3 格），所以 (0, 0) 的 Z 检查落在左层 (0, 3)、(11, 0)、(10, 0) 和右层 (9, 0)、(0, 5)、(0, 4)。倒着走保证 H_XH_Zᵀ = AB + BA = 0（x、y 的乘法可以交换次序，AB = BA，两份相加模 2 为 0），也就是每条 X 检查和每条 Z 检查重叠偶数次、互相对易。读数里的 GF(2) 指只有 0 和 1 两个数、加法只看奇偶（1 + 1 = 0）的算术；秩（rank）是矩阵里真正独立的行数：若干行在 GF(2) 里相加得全 0，其中就有一行是多余的。gross 的 H_X 有 72 行、秩 66，H_Z 也是 66（本篇的检验脚本按同样的约定算过），所以 k = 144 − 66 − 66 = 12：144 个比特扣掉 132 条独立检查。实验台读数里的 n、k 就是这样现场算出来的。

Written as a row of 144 zeros and ones, this one check is row 0 of the matrix H_X: columns 1, 2, 18, 75, 78, 84 hold a 1, all others 0. H_X = [A | B] says exactly “the left 72 columns are set by A, the right 72 by B”, one row per site. Z checks use the reversed moves: H_Z = [Bᵀ | Aᵀ], where the transpose ᵀ means taking every move backwards (x³ becomes 3 steps left), so the Z check at (0, 0) reaches left-layer (0, 3), (11, 0), (10, 0) and right-layer (9, 0), (0, 5), (0, 4). The reversal guarantees H_XH_Zᵀ = AB + BA = 0 (multiplication by x and y can be done in either order, AB = BA, and two copies add to 0 mod 2), that is, every X check overlaps every Z check an even number of times and they commute. GF(2) in the readout is the arithmetic with only the numbers 0 and 1, where addition keeps only the parity (1 + 1 = 0); the rank is the number of truly independent rows of a matrix: if some rows add up to all zeros in GF(2), one of them is redundant. gross's H_X has 72 rows and rank 66, and H_Z also 66 (this guide's check script computed both with the same conventions), so k = 144 − 66 − 66 = 12: 144 qubits minus 132 independent checks. That is how the bench computes n and k live.

研究现场。Wanted 板的 yaml 为这道题登记了一个正在进行的仓库：github.com/Xun-Gao/fast-code-distance-estimator，yaml 的注释写着 “active research on the certified lower-bound half”。本篇没有阅读或运行这个仓库，只转述登记。

The research front. The problem's yaml registers a working repository: github.com/Xun-Gao/fast-code-distance-estimator, with the yaml comment “active research on the certified lower-bound half”. This guide has neither read nor run that repository; it only relays the registration.

相关条目。yaml 的 related 列出两个：bivariate_bicycle（gross 与 toric_L3 所在的 BB 条目）和 surface（L3、L4、L5 所在的表面码条目）。它们的教程：BB 参数教程 2.4 节「d：两份证书，不是一个标签」、表面码参数教程 2.3 节「d = L：一条上界，一条下界」，以及两个条目的形式化教程（BB 3.3 节：gross 为什么没有精确码距证书、表面码 3.3 节：为什么 L5 没有）。

Related entries. The yaml's related list names two: bivariate_bicycle (the BB entry housing gross and toric_L3) and surface (the surface-code entry housing L3, L4, L5). Their guides: BB parameters 2.4, “d: two certificates, not one label”, surface parameters 2.3, “d = L: one upper bound, one lower bound”, and the two entries' formal-verification guides (BB 3.3: why gross has no exact-distance certificate, surface 3.3: why L5 has none).

同一系列的下一篇。找到下界只是一半；把它写成机器能核对的证书是另一道开放问题：《一张机器能核对的「没有更轻逻辑算符」证书》。

Next in this series. Finding the bound is one half; writing it as a certificate a machine can check is another open problem: “A machine-checkable certificate that nothing lighter exists”.

回放一遍。码距 d 是最轻逻辑算符的重量。上界一半便宜：找到一条重量 w 的逻辑算符就有 d ≤ w；toric_L3 上一分钟手算，gross 上 rand-lowweight-v1（seed 5，iters 2000）找到 12。下界一半贵：要排除所有更轻的候选；toric_L3 有 171 条纯 Z 串（342 条纯型串，1 431 条 X/Y/Z 串），一下午或三句话；gross 有约 10¹⁶ 条纯 Z 串；按 1.4 节的假设（每秒核对十亿条），纯 X、纯 Z 串合起来约 8 个月，X、Y、Z 都算约 5 万年，大一号的 [[288, 12, 18]] 要约 8 × 10¹⁰ 年。QEC-Bank 于是用三样工具拼记录：穷举（verified，只在穷举算得完的范围内）、随机搜索（上界）、引文（下界），并在 gross 与 L5 旁边诚实地写 bounded，在四个亲戚旁边写 claimed。gross 这一个实例的 d 已经有人用整数规划算出（Bravyi 等人），只是 QEC-Bank 没有重放、也没有可核对的证书。有了一台在 n ≈ 100 以上都能给出有证明、能被 QEC-Bank 核对的下界的机器，gross 的词会翻成 verified，比较表会变得可信；这样的机器今天还不存在，难度是 open-research。

Replay. The distance d is the weight of the lightest logical operator. The upper half is cheap: one logical of weight w gives d ≤ w; a minute by hand on toric_L3, rand-lowweight-v1 (seed 5, iters 2000) finding 12 on gross. The lower half is expensive: every lighter candidate must be excluded; toric_L3 has 171 pure-Z strings (342 pure-type, 1 431 X/Y/Z strings), an afternoon or three sentences; gross has about 10¹⁶ pure-Z strings; under the assumption of 1.4 (a billion candidates checked per second) the pure-X and pure-Z strings together take about 8 months, all X, Y, Z strings about 50 000 years, and the next size up, [[288, 12, 18]], about 8 × 10¹⁰ years. So the QEC-Bank assembles records from three tools, exhaustion (verified, only as far as enumeration reaches), random search (upper), citation (lower), and honestly writes bounded beside gross and L5, claimed beside the four relatives. The d of the single instance gross has been computed by integer programming (Bravyi et al.), but the QEC-Bank has not replayed it and holds no checkable certificate. Given a machine delivering proven lower bounds that the QEC-Bank can check, at n around 100 and beyond, gross's word would flip to verified and the comparison table would become trustworthy; such a machine does not exist today, and the difficulty is open-research.