两个多项式，一次拼装，
和机器真正核对过的那部分 Two polynomials, one assembly,
and the part a machine actually checked

先回忆证据词。QEC-Bank 是一个量子纠错码的资料库（本系列的「条目导读」都在讲它的条目）；它的证据词QEC-Bank 给每条声明标注来源的固定词：verified = QEC-Bank 的程序独立重算、结果一致；bounded = 上下界分别有来源，没有被同一台穷举程序合拢；claimed = 照录文献，程序没有重算。有三种：verified 是「QEC-Bank 的程序自己重算过，结果一致」；bounded 是「上界与下界各有来源，但没有被同一次穷举合拢」（gross 的 d：上界是程序找到的例子，下界是论文的结论）；claimed 是「照录文献，程序没算」。本篇问的是：verified 的那几个数字背后，有没有一份任何人都能自己核对的东西？有，叫证书。

First, recall the evidence words. The QEC-Bank is a database of quantum error-correcting codes (the “entry guides” of this series each explain one of its entries). Its evidence wordsThe fixed words the QEC-Bank attaches to each claim to record its source: verified = recomputed independently by the QEC-Bank's programs, with matching results; bounded = upper and lower bounds have separate sources and were not closed by one exhaustive program; claimed = copied from the literature, not recomputed. come in three kinds: verified means “the QEC-Bank's programs recomputed it and got the same answer”; bounded means “the upper and lower bounds each have a source, but no single exhaustive search closed them” (gross's d: the upper bound is an example a program found, the lower bound a paper's result); claimed means “copied from the literature, not computed”. This guide asks: behind the verified numbers, is there something anyone can check for themselves? There is, and it is called a certificate.

证书 = 数据 + 一个不信任任何人的检查程序。设想你要让一个陌生人相信「gross 的 H_X 秩是 66」。只写「秩 = 66」，他只能信你。证书certificate：绑定在一个有限对象上的一包数据，配一个通用检查程序；检查程序从对象本身把每一项重算一遍，与数据逐位比对，一致才算通过。换一种做法：写下一包带细节的数据（例如「这个矩阵化简后是这些行、主元在这些列」），再配一个通用的检查程序；检查程序不接受任何现成的数字，从矩阵本身把每一项重算一遍，与数据逐位比对，一致才算通过。好处是信任换了对象：你不必相信写这一页的人，只需相信一个短小、公开、对码一无所知的程序——同一个程序对 BB 码、表面码、任何码都做一模一样的事，它的通过才有说服力。QEC-Bank 的规矩是「只给一个秩的整数不算证书」，必须附上能逐位比对的中间结果；下面的补课用一个 3 × 4 的小矩阵把这件事完整走一遍。

Certificate = data + a checking program that trusts nobody. Suppose you want a stranger to believe “the rank of gross's H_X is 66”. Write only “rank = 66” and they have to take your word. A certificateA package of data bound to one finite object, with a generic checking program; the program recomputes every item from the object itself and compares bit by bit; only full agreement passes. works differently: you write down a package of detailed data (for instance “this matrix reduces to these rows, with pivots in these columns”) and pair it with a generic checking program, which accepts no ready-made number, recomputes every item from the matrix itself and compares bit by bit; only full agreement passes. The gain is that trust moves: you need not trust the author of this page, only a short, public program that knows nothing about codes. The same program does exactly the same thing for BB codes, surface codes or any code, which is why its passing means something. The QEC-Bank rule is that “a rank integer alone is not a certificate”: the intermediate result that can be compared bit by bit must be included. The catch-up below walks through this on a small 3 × 4 matrix.

检查程序是用 Lean 写的。Lean一种「定理证明器」：既是编程语言，又能让计算机逐步检查数学证明；用它写的程序，其依赖的数学公理可以一条条列出来审计。是一种定理证明器：既是编程语言，又能让计算机逐步检查数学证明，用它写的程序依赖哪些公理可以一条条列出来。QEC-Bank 的检查程序叫 qec-atlas-lean-complete-v1（BB 条目的数据卡片 card.yaml——QEC-Bank 每个条目一张、用 YAML 文本格式写成的清单——里 lean.checker 一栏的原文），下文简称 Lean Complete v1。它已被「封存」：源代码固定下来不再修改，依赖的公理只有 Lean 标准的三条。它明文列出自己不接受的东西：对某一个码单独写的定理（per-code theorem）、对整个码族成立的码距定理（family-distance theorem）、译码器、阈值、硬件模型等。换句话说，它只核对一个个具体的、有限大小的矩阵。

The checking program is written in Lean. LeanA “proof assistant”: a programming language in which a computer can also check mathematical proofs step by step; for a program written in it, the mathematical axioms it relies on can be listed and audited one by one. is a proof assistant: a programming language in which a computer can also check mathematical proofs step by step, and for any program written in it one can list exactly which axioms it relies on. The QEC-Bank checker is named qec-atlas-lean-complete-v1 (the literal lean.checker field of the BB entry's data card card.yaml, the list, one per QEC-Bank entry and written in the YAML text format), called Lean Complete v1 below. It has been “sealed”: its source code is frozen, and the only axioms it relies on are Lean's three standard ones. It states explicitly what it does not accept: a theorem written for one particular code (per-code theorem), a distance theorem for a whole family of codes (family-distance theorem), decoders, thresholds, hardware models and so on. In other words, it checks only individual matrices of definite, finite size.

身份：矩阵本身的指纹。证书得说清「对哪个对象」。「gross」只是个名字，名字会被改、会被重用。QEC-Bank 为每个实例生成一份数据文件，叫 Formal IRformal intermediate representation：QEC-Bank 为每个已发布实例生成的 JSON 数据文件（格式名 qec-atlas-formal-ir-v1），把数学对象、构造步骤、声明、见证、证书和附件分放在固定字段里。（「形式化中间表示」，一种 JSON 格式的文本），其中 semantic 字段只放数学对象本身——对 BB 码就是 H_X、H_Z 两块 0/1 矩阵；引文、证书、电路都放在别的字段。实例的身份是它的语义哈希semantic_hash：把 Formal IR 的 semantic 字段按固定规则写成唯一的字节串，前面接上文本 qec-atlas-formal-ir-v1 和一个零字节，做 SHA-256 得到的 64 位十六进制串。：把 semantic 字段按固定规则写成唯一的一串字节（规范字节canonical bytes：按 RFC 8785 的 JSON 规范写法（键按字母排序、不留空白、UTF-8 编码）得到的唯一字节串；同一个对象无论谁来写，字节都相同。），前面接上一段固定文本 qec-atlas-formal-ir-v1 和一个零字节（这段域前缀domain prefix：拼在被哈希的字节前面的一段固定文本，标明「这是 Formal IR 的对象」，使别处用途的字节串不会恰好算出同一个指纹。标明用途），再做 SHA-256，得到一个 64 位十六进制数：

Identity: a fingerprint of the matrix itself. A certificate must say which object it is about. “gross” is only a name, and names get changed and reused. For each instance the QEC-Bank generates a data file called the Formal IRFormal intermediate representation: the JSON data file the QEC-Bank generates for each shipped instance (format name qec-atlas-formal-ir-v1), with the mathematical object, construction steps, claims, witnesses, certificates and attachments in fixed fields. (“formal intermediate representation”, a JSON text file), whose semantic field holds only the mathematical object, for a BB code the two 0/1 matrices H_X and H_Z; citations, certificates and circuits live in other fields. An instance's identity is its semantic hashsemantic_hash: the semantic field of the Formal IR written as a unique byte string by fixed rules, prefixed with the text qec-atlas-formal-ir-v1 and one zero byte, and hashed with SHA-256; 64 hex digits.: the semantic field is written as one unique byte string by fixed rules (the canonical bytesThe unique byte string obtained by RFC 8785's canonical JSON writing (keys sorted alphabetically, no whitespace, UTF-8); whoever writes the same object gets the same bytes.), prefixed with a fixed text qec-atlas-formal-ir-v1 and one zero byte (this domain prefixA fixed text placed before the bytes being hashed, marking them as a Formal IR object, so that byte strings used for other purposes cannot produce the same fingerprint by coincidence. marks the purpose), and hashed with SHA-256, which yields a 64-digit hexadecimal number:

于是：多一篇引文、多一份证书，semantic 字段不变，哈希不变；矩阵里改一个比特，哈希面目全非。两个补课把这两句话落到手算的例子上。

So: add a citation or a certificate and the semantic field, hence the hash, is unchanged; flip one bit of the matrix and the hash becomes unrecognisable. The two catch-ups below put these two sentences into hand-sized examples.

BB 条目的形式化页只有两行，页面的总纲一句话：「Each shipped finite instance has one canonical Formal IR semantic identity and a Lean-checked structural certificate. Eligible small exact-distance certificates are additive; claims outside Lean Complete v1 keep their existing evidence origin.」人话：每个发布的实例有一个身份和一份结构证书；够小的实例另加一份精确码距证书；Lean 管不到的声明保留原有证据词。两行的「native branch」（原生分支）都是 css-chain。Formal IR 有四种描述对象的原生方式，叫四条分支branch：Formal IR 描述有限对象的四种原生方式之一：static stabilizer（直接列出全部检查）、css-chain（CSS 码：给出 H_X、H_Z 两块矩阵）、subsystem/gauge（带「规范」自由度的子系统码）、measurement schedule（按测量时序描述）。：直接列出全部检查、给出 CSS 码的两块矩阵、描述子系统码、按测量时序描述。CSS 码每条检查要么全由 X 组成、要么全由 Z 组成的码；于是只需两块 0/1 矩阵 H_X、H_Z 就能写下全部检查。是每条检查要么全是 X、要么全是 Z 的码，BB 码就是这样，所以走 css-chain：对象由 H_X、H_Z 两块矩阵给出（名字里的 chain 指的是把这两块矩阵看成两步映射的写法，即 BB 教程 4.4 节的链复形；本篇用不到它）。哈希前 16 位取自页面，完整 64 位取自 card.yaml 的 formalization.instances：

The BB entry's formal-verification page has just two rows, with one headline sentence: “Each shipped finite instance has one canonical Formal IR semantic identity and a Lean-checked structural certificate. Eligible small exact-distance certificates are additive; claims outside Lean Complete v1 keep their existing evidence origin.” Plainly: every shipped instance has one identity and one structural certificate; instances small enough get an exact-distance certificate in addition; claims Lean cannot reach keep their evidence word. Both rows read css-chain for “native branch”. The Formal IR has four native ways of describing an object, its four branchesOne of the four native ways the Formal IR describes a finite object: static stabilizer (list every check), css-chain (a CSS code: give the two matrices H_X, H_Z), subsystem/gauge (subsystem codes with “gauge” freedom), measurement schedule (describe by the timing of measurements).: list every check, give the two matrices of a CSS code, describe a subsystem code, or describe a measurement schedule. A CSS codeA code in which every check consists only of X or only of Z; all checks can then be written as two 0/1 matrices H_X and H_Z. is one whose every check is all-X or all-Z; BB codes are like that, so they use css-chain: the object is given by the two matrices H_X and H_Z (the “chain” in the name refers to reading the two matrices as two successive maps, the chain complex of BB guide section 4.4; this guide does not need it). The first 16 hash digits are as on the page; the full 64 come from formalization.instances in card.yaml:

证书自己也有由内容决定的名字，格式 certificate:<对象哈希>:<类别>:<证书内容哈希>@1：第一段说关于哪个对象，第二段说哪一类证书，第三段是证书载荷payload：证书里那包数据本身，例如 1.1 节补课里的 {rref, pivots}。（那包数据本身）的 SHA-256，所以证书的名字也由内容决定。card.yaml 里 BB 条目恰好登记了三个这样的名字，一个不多：

Certificates too carry content-determined names, in the format certificate:<object hash>:<kind>:<payload hash>@1: the first segment says which object, the second which class of certificate, the third is the SHA-256 of the certificate's payloadThe package of data inside a certificate, for example the {rref, pivots} of the catch-up in section 1.1. (the data package itself), so a certificate's name is also fixed by its content. card.yaml registers exactly three such names for the BB entry, not one more:

先说「重放」是什么意思。条目自己有一段构造程序（constructor.py），从四个变量算出矩阵。「重放」是另一段独立写的程序照着一张写死的配方把矩阵重新算一遍，再和构造程序的结果逐元素比对；两段程序各写各的，同一个疏忽同时出现在两边的机会很小。配方写在 card.yaml 的 construction 块里（这块数据遵守的格式名叫 qec-atlas-construction-v1），翻成人话是三句：① 输入口 A：调用生成器generator：配方里一个带版本号的步骤，「从几个参数生成一个数学对象」；用 {namespace, kind: generator, id, version} 这样的结构化名字指明，不用文件路径或函数名。（配方里一个带版本号的「从参数生成矩阵」的步骤）bivariate_polynomial 版本 1，参数 l、m、terms 分别取实例的 l、m、a_terms，输出一个 parity_check（校验矩阵，就是矩阵 A）；② 输入口 B：同一个生成器，terms 取 b_terms，输出矩阵 B；③ 操作construction-op：配方里把生成器的输出拼成一个码的带版本号步骤。 bivariate_bicycle 版本 1 吃进 A、B，输出一个 checkmatrix（检查矩阵对象），比对规则叫 exact-checkmatrix-v1。derivations.md（条目的推导说明文档）一句话总结：「The construction: block pins bivariate_polynomial@1 for both polynomial factors and bivariate_bicycle@1 for the CSS block assembly.」

First, what “replay” means. The entry has its own construction program (constructor.py) that computes the matrices from the four variables. “Replay” is a second, independently written program that recomputes the matrices from a fixed recipe and compares them element by element with the construction program's result; with two programs written separately, the chance that the same slip appears in both is small. The recipe lives in the construction block of card.yaml (the format this block follows is named qec-atlas-construction-v1), three sentences in plain words: (1) input port A: call the generatorA versioned step of the recipe that “produces a mathematical object from a few parameters”; named by a structured reference {namespace, kind: generator, id, version}, never by a file path or function name. (a versioned “make a matrix from parameters” step of the recipe) bivariate_polynomial version 1 with parameters l, m, terms taken from the instance's l, m, a_terms, producing one parity_check (a check matrix: the matrix A); (2) input port B: the same generator with terms taken from b_terms, producing the matrix B; (3) the operationconstruction-op: a versioned step of the recipe that assembles generator outputs into a code. bivariate_bicycle version 1 consumes A and B and outputs one checkmatrix (a check-matrix object), compared under the rule exact-checkmatrix-v1. derivations.md (the entry's derivation notes) sums it up: “The construction: block pins bivariate_polynomial@1 for both polynomial factors and bivariate_bicycle@1 for the CSS block assembly.”

版本号买到了什么。配方里只有带版本号的名字，没有程序文件路径、没有函数名。契约（QEC-Bank 规定 Formal IR 规则的设计文档）原话：「A moving branch, import path, callable name, or unversioned operation is not an identity」——会变动的代码分支、导入路径、函数名或不带版本号的操作，都不能当作身份。于是 bivariate_polynomial@1 的规则一旦发布就不再改；谁要改，就得叫 @2。这样十年后的人照着同一张配方，仍能得到同一个矩阵、算出同一个哈希。

What the version numbers buy. The recipe contains only versioned names: no program file path, no function name. The contract (the QEC-Bank design document that fixes the Formal IR rules) says: “A moving branch, import path, callable name, or unversioned operation is not an identity”. So once the rules of bivariate_polynomial@1 are published they never change; a change must be called @2. Someone following the same recipe ten years later still gets the same matrix and computes the same hash.

重放用的代码在 constructions/bivariate_bicycle_replay.py，与 constructor.py 是两份独立的实现。生成器 bivariate_polynomial@1 的规则很严：参数必须恰好是 {l, m, terms}（多一个少一个都报错），l、m 必须是正整数，每一项必须是一对整数并按 mod l、mod m 约化（例如 x 方向走 13 步等于走 1 步，因为环面绕一圈是 12 步），然后对每一对 (a, b) 算出单项式 x^ay^b 的矩阵——「从每个格点向右走 a 步、向上走 b 步」这个移动写成的 0/1 矩阵——再异或（XOR，逐位模 2 相加：1 + 1 = 0）进结果，正是BB 教程 2.3 节那件事。下面的实验台就是这个生成器的可视化。它的预设是 gross 的多项式 A = x³ + y + y²，但画在 6 × 6 的小环面上，好看清楚；把 l 的滑块拖到 12，就是 gross 真正的 12 × 6 环面和 72 × 72 的 A。点一个起点，看三个箭头落在哪里：右边矩阵里高亮的那一行有三个 1，就是生成器输出的这一行。

The replay code lives in constructions/bivariate_bicycle_replay.py, an implementation independent of constructor.py. The generator bivariate_polynomial@1 is strict: parameters must be exactly {l, m, terms} (one more or one fewer is an error), l and m must be positive integers, every term must be a pair of integers reduced mod l and mod m (13 steps in x equal 1 step, since going once round the torus takes 12), and for each pair (a, b) it computes the matrix of the monomial x^ay^b, the 0/1 matrix of the move “from every site go a steps right and b steps up”, and XORs it into the result (XOR = add digit by digit mod 2: 1 + 1 = 0), exactly the operation of BB guide section 2.3. The bench below visualises this generator. Its preset is gross's polynomial A = x³ + y + y², drawn on a small 6 × 6 torus so it stays legible; drag the l slider to 12 and you have gross's actual 12 × 6 torus and 72 × 72 A. Click a source site and see where the three arrows land: the highlighted row of the matrix on the right has three ones, and that is the generator's output row.

操作 bivariate_bicycle@1 只做一件事：检查 A、B 是同形的方阵后，拼出 H_X = [A | B]、H_Z = [Bᵀ | Aᵀ]，交给 CheckMatrix.from_css 并 validate()（QEC-Bank 代码库里「把两块矩阵装成一个 CSS 检查矩阵对象」和「做基本自检」的两个函数）。然后验证器把这个重放出来的矩阵和条目自己的构造器（constructor.py）算出来的矩阵放在一起，按 exact-checkmatrix-v1 比较。代码里的说明文字（docstring）把「exact」说得很直白：「Equality is intentionally presentation-sensitive: stabilizer, gauge, row, and qubit ordering are all part of the replay witness.」人话：不是「两个矩阵代表同一个码」就算过；必须是同一个数组，同样的行顺序、同样的列（比特）编号、左右两块同样的先后。若形状不同，报「stabilizer shape mismatch」；形状相同而任何一个元素不同，报「stabilizer values or row/qubit ordering mismatch」，整条重放失败。derivations.md：「Replay must reconstruct the exact ordinary-constructor matrix—including row, qubit, and two-block ordering—for both gross and toric_L3.」

The operation bivariate_bicycle@1 does one thing: after checking that A and B are square matrices of equal shape, it assembles H_X = [A | B], H_Z = [Bᵀ | Aᵀ], hands them to CheckMatrix.from_css and calls validate() (the two functions of the QEC-Bank code base that “package two blocks as a CSS check-matrix object” and “run basic self-checks”). The verifier then places this replayed matrix next to the one the entry's own constructor (constructor.py) produces and compares them under exact-checkmatrix-v1. The code's built-in description (its docstring) states what “exact” means: “Equality is intentionally presentation-sensitive: stabilizer, gauge, row, and qubit ordering are all part of the replay witness.” Plainly: “the two matrices represent the same code” does not pass; it must be the same array, same row order, same column (qubit) numbering, same order of the left and right blocks. A shape difference reports “stabilizer shape mismatch”; equal shape with any differing element reports “stabilizer values or row/qubit ordering mismatch”, and the replay fails. derivations.md: “Replay must reconstruct the exact ordinary-constructor matrix—including row, qubit, and two-block ordering—for both gross and toric_L3.”

为什么要这么苛刻？因为语义哈希是对这个数组算的（1.1 节补课：两行对调，写出来的字节就不同，指纹就不同）。同一个码换一种行序或比特编号，就成了另一个身份。所以「精确到比特序」不是吹毛求疵，而是让哈希这个名字有意义的最低要求。怎样抓住编号上的走样？靠几个写死的具体数字，叫「约定锚点」（convention anchors）：reproduce.py（条目的复现脚本，第 4 章）逐字断言 gross 第 0 条 X 检查碰到的比特是 [1, 2, 18, 75, 78, 84]，第 0 条 Z 检查是 [3, 60, 66, 76, 77, 126]（参数导读 1.3 节也数过）。这两行数字可以手算出来，下表就是算法。

Why so strict? Because the semantic hash is computed over this array (catch-up of section 1.1: swap two rows and the written bytes differ, so the fingerprint differs). The same code with another row order or qubit numbering becomes a different identity. So “exact to qubit order” is not pedantry; it is the minimum that gives the hash-as-name any meaning. How is a slip in numbering caught? By a few hard-coded concrete numbers called “convention anchors”: reproduce.py (the entry's reproduction script, Chapter 4) asserts literally that gross's X check 0 touches the qubits [1, 2, 18, 75, 78, 84] and Z check 0 the qubits [3, 60, 66, 76, 77, 126] (also counted in section 1.3 of the parameters guide). Both lines can be computed by hand; the table below shows how.

现在看锚点怎样抓住走样。换块的顺序：若有人写成 H_X = [B | A]，码还是那个码（只是把两层的名字对调），但第 0 行变成 [3, 6, 12, 73, 74, 90]。换移动方向：若把循环移位矩阵 S 的方向写反（于是 x 成了「向左一步」、y 成了「向下一步」），第 0 行变成 [4, 5, 54, 75, 132, 138]；只把 x 写反、y 不动，也会变成 [1, 2, 54, 75, 132, 138]。三种情况断言都当场失败，哈希也会是另一个。（这三行由本篇的 notes 脚本算出，也可以用上表的办法手算。）

Now see how the anchors catch a slip. Swap the block order: if someone writes H_X = [B | A], the code is the same code (the two layers merely trade names), but row 0 becomes [3, 6, 12, 73, 74, 90]. Reverse the direction of the moves: if the cyclic shift matrix S is written the wrong way round (so x becomes “one step left” and y “one step down”), row 0 becomes [4, 5, 54, 75, 132, 138]; reversing only x and leaving y alone gives [1, 2, 54, 75, 132, 138]. In all three cases the assertion fails on the spot, and the hash would be a different one. (All three lines were computed by this guide's notes script; the table's method reproduces them by hand.)

为什么 BB 条目在 144 比特的 gross 之外，还要带一个 18 比特的小实例？条目的直觉说明文档 intuition.md 的话：它「providing a small toric anchor that checks the conventions without claiming every BB block decomposes into toric codes」——提供一个小环面锚点来检验约定，同时不声称每个 BB 块都能拆成环面码。人话：l = m = 3、A = 1 + x、B = 1 + y 这组参数走同一条配方（同样两个生成器、同一个操作），得到两块 9 × 18 的矩阵（每条检查碰 4 个比特），两个秩各 8，于是 r = 8 + 8 = 16 条独立检查、k = 18 − 16 = 2，穷举得 d = 3——它就是 3 × 3 的环面码；这是环面码教程里手数过的那本账，任何约定上的疏忽都会在这里露馅（BB 教程 5.1 节：忘掉转置，检查就不再对易）。把预设切到 toric_L3，看四腿检查和 [[18,2,3]]。

Why does the BB entry carry an 18-qubit instance besides the 144-qubit gross? In the words of the entry's intuition notes intuition.md, it is “providing a small toric anchor that checks the conventions without claiming every BB block decomposes into toric codes”. Plainly: the parameters l = m = 3, A = 1 + x, B = 1 + y go through the same recipe (same two generators, same operation) and yield two 9 × 18 matrices (each check touches 4 qubits), both of rank 8, so r = 8 + 8 = 16 independent checks and k = 18 − 16 = 2, with d = 3 by enumeration: it is the 3 × 3 toric code; this is the ledger counted by hand in the toric-code guide, and any slip in convention shows up here (BB guide section 5.1: forget the transpose and the checks stop commuting). Switch the preset to toric_L3 to see the four-legged checks and [[18,2,3]].

契约规定每个发布的实例都必须带一份 structural-validity@1（结构有效性证书）。它的检查程序做的正是参数导读 2.3 节那道算术的机器版，分四步：① 把 H_X 和 H_Z 分别用模 2 高斯消元化成行最简形（1.1 节补课那套操作，主元从左往右找），两边的主元个数相加就是独立检查的条数 r = rank H_X + rank H_Z；② 从 H_X（或 H_Z）的列数读出比特数 n，每一列是一个数据比特；③ 由 k = n − r 得到逻辑比特数 k（k 数逻辑比特，与 [[n, k, d]] 的写法一致）；④ 验证每条 X 检查与每条 Z 检查两两对易，即 H_XH_Z^T = 0（模 2）。落到 gross 上：H_X 的 72 行里只有 66 行独立（另外 6 行都是其他行的和），H_Z 同样 66 行，所以 r = 66 + 66 = 132 个主元，n = 144，k = 144 − 132 = 12，css = true。toric_L3：r = 8 + 8 = 16，n = 18，k = 2，css = true。

The contract requires every shipped instance to carry a structural-validity@1 (structural-validity certificate). Its checking program is the machine edition of the arithmetic in section 2.3 of the parameters guide, in four steps: (1) bring H_X and H_Z separately to reduced row echelon form by Gaussian elimination mod 2 (the operations of the catch-up in section 1.1, pivots found left to right); the two pivot counts added give the number of independent checks r = rank H_X + rank H_Z; (2) read the number of qubits n from the number of columns of H_X (or H_Z), one column per data qubit; (3) get the number of logical qubits from k = n − r (k counts logical qubits, as in [[n, k, d]]); (4) verify that every X check commutes with every Z check, i.e. H_XH_Z^T = 0 (mod 2). For gross: only 66 of the 72 rows of H_X are independent (the other 6 are sums of other rows), likewise 66 for H_Z, so r = 66 + 66 = 132 pivots, n = 144, k = 144 − 132 = 12, css = true. toric_L3: r = 8 + 8 = 16, n = 18, k = 2, css = true.

为什么两个秩可以直接相加。一条 X 检查的行和一条 Z 检查的行虽然都写成 144 位的 0/1 串，意思却不同：前者的 1 表示「这个比特上放 X」，后者的 1 表示「放 Z」。X 和 Z 不会互相抵消（X 乘 Z 得到 Y，差一个相位，不是 I），所以一组检查的乘积等于 I，当且仅当其中的 X 检查自己乘出 I、Z 检查也自己乘出 I。于是 X 检查之间的依赖和 Z 检查之间的依赖各算各的，独立条数就是两个秩之和。反过来，如果把两块矩阵直接上下叠成一个 144 × 144 的矩阵再求秩，就等于把「放 X」和「放 Z」当成同一件事，gross 会得到 112 而不是 132（toric_L3 得到 12 而不是 16）——这是一个容易犯的错。要一个矩阵装下两类检查，正确的写法是每行 288 位：前 144 位记 X 部分、后 144 位记 Z 部分，X 检查的行是 (H_X | 0)，Z 检查的行是 (0 | H_Z)，这个矩阵的秩正是 66 + 66 = 132；此时 n 仍是 144，不是 288。（三个秩都由本篇 notes 里的脚本算出。）

Why the two ranks simply add. A row of H_X and a row of H_Z are both written as strings of 144 zeros and ones, but they mean different things: a 1 in the first says “put X on this qubit”, a 1 in the second “put Z”. X and Z never cancel each other (X times Z gives Y up to a phase, not I), so a product of checks equals I exactly when its X checks multiply to I among themselves and its Z checks do too. Dependencies among X checks and among Z checks are therefore counted separately, and the number of independent checks is the sum of the two ranks. If instead you stack the two blocks into one 144 × 144 matrix and take its rank, you treat “put X” and “put Z” as the same thing, and gross gives 112 rather than 132 (toric_L3 gives 12 rather than 16); this is an easy mistake to make. To hold both kinds of check in one matrix, write each row with 288 bits: the first 144 record the X part, the last 144 the Z part; X checks are rows (H_X | 0), Z checks rows (0 | H_Z), and this matrix has rank exactly 66 + 66 = 132, while n is still 144, not 288. (All three ranks were computed by the script in this guide's notes.)

第 ③ 步有一个前提：检查两两对易还不够，还不能有哪几条检查的乘积等于 −I（那样就没有任何状态能同时通过全部检查，「剩下 k 个逻辑比特」无从谈起；例如 XZZ、ZXZ、ZZX、XXX 四条两两对易，乘起来却是 −I）。CSS 码自动满足这个前提：全 X 的检查相乘仍是全 X、不带负号，全 Z 的同理，所以乘积只可能是「一串 X 乘一串 Z」，不可能是 −I。这正是第 ④ 步的 css = true 在这里的用处。

Step (3) has a precondition: pairwise commuting checks are not enough; no product of checks may equal −I (then no state passes all checks at once and “k logical qubits remain” means nothing; for example XZZ, ZXZ, ZZX and XXX commute pairwise, yet their product is −I). CSS codes satisfy this automatically: a product of all-X checks is still all-X with no minus sign, likewise for all-Z, so any product is “a string of X times a string of Z” and never −I. This is what the css = true of step (4) is good for here.

这份证书解除discharge：一份证书通过后，QEC-Bank 把它覆盖的命题记为「已由这份证书核对」。（discharge，即通过后记为「已由证书核对」）的命题是 validity, n, k, css；契约同样写明它「never discharges distance, decoder, circuit, or family claims」——永不涉及码距、译码器、电路或整个码族的声明。参数页上共有七个 verified：两个实例各自的 n、k、css（六个），加上 toric_L3 的 d。前六个由两份结构证书核对；第七个由下一节的码距证书核对。

The propositions this certificate dischargesWhen a certificate passes, the QEC-Bank records the propositions it covers as “checked by this certificate”. (records as “checked by a certificate” once it passes) are validity, n, k, css; the contract equally states it “never discharges distance, decoder, circuit, or family claims”. The parameters page has seven verifieds in all: n, k and css of each of the two instances (six), plus toric_L3's d. The first six are checked by the two structural certificates; the seventh by the distance certificate of the next section.

先把要证的话说清。一个 Pauli 算符在每个比特上放 I（什么也不做）、X、Y、Z 之一的算符；Y 同时含有 X 与 Z 两种成分。它的重量 = 不是 I 的比特个数。在每个比特上放 I、X、Y、Z 之一（Y 同时含 X 与 Z 两种成分），它的重量是非 I 的比特个数。码距 d 是最轻的逻辑算符能骗过全部检查（与每条检查对易）、却又不是检查乘积的 Pauli 算符；它悄悄改写被保护的信息。的重量；逻辑算符要满足两条：(a) 与每条检查对易——不触发任何警报；(b) 不是若干条检查的乘积——否则它对编码信息什么也不做。判断对易只需数「撞车」：一条 X 检查与候选算符在「检查放 X、候选放 Z 或 Y」的比特上撞车，Z 检查在「检查放 Z、候选放 X 或 Y」的比特上撞车；撞车次数为奇数就是反对易，这条检查测出来会报警。

First, the statement to be proved. A Pauli operatorAn operator placing one of I (do nothing), X, Y, Z on each qubit; Y contains both an X part and a Z part. Its weight = the number of qubits that are not I. places one of I, X, Y, Z on each qubit (Y contains both an X part and a Z part), and its weight is the number of non-I qubits. The distance d is the weight of the lightest logical operatorA Pauli operator that fools every check (commutes with each) yet is not a product of checks; it silently rewrites the protected information., which must satisfy two things: (a) it commutes with every check, raising no alarm; (b) it is not a product of checks, which would do nothing to the encoded information. Commuting is decided by counting “collisions”: an X check collides with the candidate on qubits where the check has X and the candidate has Z or Y; a Z check collides where the check has Z and the candidate has X or Y. An odd number of collisions means the two anticommute, and that check would raise an alarm.

证书的两半。设要证的码距是 u（toric_L3 的 u = 3）。上界「d ≤ u」：给出一个重量恰为 u 的逻辑算符（见证），检查程序核对它满足 (a)(b)、数它的重量。下界「d ≥ u」：对每一个重量小于 u 的非恒等 Pauli 算符（叫候选），给出一条「分类」——要么「它与第几条检查反对易」（违反 (a)），要么「它是哪几条检查的乘积」（违反 (b)）。每个更轻的候选都被分了类，就没有一个是逻辑算符，于是最轻的逻辑算符至少重 u。两半合起来 d = u。候选必须按固定顺序排好，顺序名叫 weight-then-support-lexicographic-then-X-Y-Z-v1：先按重量，重量相同按所占比特的编号从小到大（像字典排词），比特相同再按 X、Y、Z 的字母顺序。检查程序自己把整条候选流重新生成一遍，「classifications cannot omit, duplicate, or reorder candidates」——分类不能漏、不能重、不能乱序。

The two halves of the certificate. Let u be the distance to be proved (u = 3 for toric_L3). Upper bound “d ≤ u”: exhibit one logical operator of weight exactly u (the witness); the checker confirms (a) and (b) and counts its weight. Lower bound “d ≥ u”: for every non-identity Pauli of weight below u (a candidate), give one “classification”: either “it anticommutes with check number so-and-so” (violating (a)) or “it is the product of these checks” (violating (b)). If every lighter candidate is classified, none of them is logical, so the lightest logical operator weighs at least u. Together, d = u. The candidates must come in a fixed order, named weight-then-support-lexicographic-then-X-Y-Z-v1: first by weight, then, at equal weight, by the indices of the qubits they occupy, smallest first (like words in a dictionary), then, on the same qubits, by the letters X, Y, Z in that order. The checker regenerates the whole candidate stream itself, and “classifications cannot omit, duplicate, or reorder candidates”.

手算一个最小的例子。4 个比特，两条检查 XXXX、ZZZZ（这是一个 [[4, 2, 2]] 码：n = 4，r = 2，k = 2，d = 2）。重量 1 的候选有 4 × 3 = 12 个。X_q 与 ZZZZ 在第 q 个比特撞车一次 → 反对易；Z_q 与 XXXX 撞车一次 → 反对易；Y_q 与两条都撞一次。12 个全部分完类，所以 d ≥ 2。见证 X₀X₁：与 ZZZZ 撞车两次（偶数）→ 对易，与 XXXX 不撞车 → 对易；而检查的乘积只有 I、XXXX、ZZZZ 和它俩相乘得到的 YYYY（差一个符号），里面没有 X₀X₁，所以它是逻辑算符，d ≤ 2。两半合起来 d = 2。

A smallest example by hand. Four qubits, two checks XXXX and ZZZZ (a [[4, 2, 2]] code: n = 4, r = 2, k = 2, d = 2). There are 4 × 3 = 12 candidates of weight 1. X_q collides once with ZZZZ, on qubit q → anticommutes; Z_q collides once with XXXX → anticommutes; Y_q collides once with each. All 12 are classified, so d ≥ 2. Witness X₀X₁: two collisions with ZZZZ (even) → commutes, none with XXXX → commutes; and the only products of checks are I, XXXX, ZZZZ and their product YYYY (up to a sign), none of which is X₀X₁, so it is logical and d ≤ 2. Together, d = 2.

toric_L3 上的数目。候选总数是 Σ_w=1^d−1 C(n,w)·3^w：选 w 个比特（C(n, w) 种），每个放 X、Y 或 Z（3^w 种），w 从 1 加到 d − 1。契约给它设了上限 65 536（= 2¹⁶）。toric_L3：n = 18、d = 3，候选数 = 18·3 + C(18,2)·9 = 54 + 153·9 = 54 + 1377 = 1431，远在上限之内；而且它的 d 声明是 verified 的精确值（exact: 3），两道门都过，于是它拿到了那份 small-exact-distance-enumeration（小规模精确码距枚举证书）。下面的实验台把这条候选流一个一个摆出来。为什么 1431 个全部落在「反对易」一类、没有一个是「检查乘积」？检查的乘积可以是 I：每个比特恰好被两条 X 检查碰到，所以九条 X 检查全乘起来，每个比特上的 X 都出现两次、全部相消（九条 Z 检查同理）。但只要乘积不是 I，它至少碰 4 个比特：把 9 条 X 检查的 511 种非空组合逐一乘出来，除了「九条全选」那一种得到 I，其余的最轻也碰 4 个比特，Z 检查同样（本篇 notes 脚本枚举）；X、Z 混合的乘积里，X 部分或 Z 部分至少有一个不是 I，碰到的比特只会更多。所以重量 1、2 的候选都不是检查乘积。见证是左层一整列上的 X₀X₁X₂，绕环面一圈：它与全部 9 条 Z 检查对易；把它作为第 10 行加到 H_X 下面，秩从 8 升到 9，说明它不是任何几条 X 检查的和；而它只含 X，任何带 Z 检查的乘积要变成纯 X，Z 部分必须自己乘出 I，结果仍是 X 检查的乘积。所以它不是检查乘积，是逻辑算符。

The numbers for toric_L3. The total number of candidates is Σ_w=1^d−1 C(n,w)·3^w: choose w qubits (C(n, w) ways), put X, Y or Z on each (3^w ways), sum w from 1 to d − 1. The contract caps it at 65,536 (= 2¹⁶). toric_L3: n = 18, d = 3, candidates = 18·3 + C(18,2)·9 = 54 + 153·9 = 54 + 1377 = 1,431, well under the ceiling; and its distance claim is a verified exact value (exact: 3), so it passes both gates and receives the small-exact-distance-enumeration (small exact-distance enumeration certificate). The bench below lays the candidate stream out one by one. Why do all 1,431 land in the “anticommutes” class and none in “product of checks”? A product of checks can be I: every qubit is touched by exactly two X checks, so multiplying all nine X checks puts two X's on each qubit and everything cancels (likewise for the nine Z checks). But any product that is not I touches at least 4 qubits: multiplying out all 511 nonempty sets of the 9 X checks, every set except “all nine” (which gives I) touches at least 4 qubits, and the same holds for Z checks (enumerated by this guide's notes script); in a mixed X-and-Z product, the X part or the Z part is not I, so it touches at least as many. Hence no candidate of weight 1 or 2 is a product of checks. The witness is X₀X₁X₂ on one whole column of the left layer, going once round the torus: it commutes with all 9 Z checks; appending it to H_X as a tenth row raises the rank from 8 to 9, so it is not a sum of X checks; and since it contains only X's, a product involving Z checks can equal it only if those Z checks multiply to I by themselves, which leaves a product of X checks again. So it is not a product of checks: it is a logical operator.

人话：Lean 逐个看完了 1431 个重量 1、2 的候选，确认每个都会触发警报（或本身是检查乘积），再核对一个重量 3 的见证。

Plainly: Lean went through all 1,431 candidates of weight 1 and 2 one by one, confirmed that each trips an alarm (or is a product of checks), and then checked one weight-3 witness.

算术。gross 的 n = 144、d = 12，候选数 Σ_w=1¹¹ C(144,w)·3^w ≈ 1.70 × 10²¹（本篇按契约公式算出，QEC-Bank 页面上没有这个数）。上限 65 536 ≈ 6.6 × 10⁴，超了约 2.6 × 10¹⁶ 倍。即使只数纯 X 型候选（去掉 3^w），Σ C(144,w) 也约有 1.0 × 10¹⁶ 个。换个感觉：就算每秒分类 10⁹ 个候选，1.7 × 10²¹ 个也要约 5.4 万年。这不是「再等硬件快一点」的差距；搜索本身是有限的，只是大得离谱，在这版策略下够不着。契约说：「Crossing it means unsupported, not false」——超限叫「不支持」，不叫「错」。

Arithmetic. Gross has n = 144, d = 12, so the candidate count Σ_w=1¹¹ C(144,w)·3^w ≈ 1.70 × 10²¹ (evaluated here from the contract's formula; no QEC-Bank page lists this number). The ceiling 65,536 ≈ 6.6 × 10⁴ is exceeded by a factor of about 2.6 × 10¹⁶. Even counting only pure-X candidates (dropping the 3^w), Σ C(144,w) is about 1.0 × 10¹⁶. For a feel: even classifying 10⁹ candidates per second, 1.7 × 10²¹ of them would take about 54,000 years. This is not a gap that faster hardware closes; the search is finite, just absurdly large, and out of this policy's reach. The contract says: “Crossing it means unsupported, not false”.

策略。就算算得动，这类证书也只为 verified 的精确码距声明生成（策略 = QEC-Bank 规定「什么情况下生成哪类证书」的规则）：QEC-Bank 仓库里「Formal Unification v1」（形式化统一）的结果文件写道，小规模精确类「is generated only for verified exact-distance claims whose complete lower-weight Pauli enumeration fits the frozen 65,536-candidate policy」。gross 的 d 是 bounded：下界是 bravyi2024bicycle 的引文，上界是种子搜索的见证。两道门 gross 都没过。于是它只有 structural-validity；它的 d 保留原有证据词 bounded，一字未改——这就是形式化页总纲里「claims outside Lean Complete v1 keep their existing evidence origin」落到 gross 身上的样子。

Policy. Even with the compute, this class is generated only for verified exact-distance claims (the policy = the QEC-Bank rules for “which certificate class is generated when”): the result file of “Formal Unification v1” in the QEC-Bank repository states that the small-exact class “is generated only for verified exact-distance claims whose complete lower-weight Pauli enumeration fits the frozen 65,536-candidate policy”. Gross's d is bounded: the lower bound is the bravyi2024bicycle citation, the upper bound a seeded-search witness. Gross fails both gates. So it holds only structural-validity, and its d keeps its original evidence word bounded, unchanged: this is what the headline “claims outside Lean Complete v1 keep their existing evidence origin” looks like when applied to gross.

参数页上 gross 的 upper: {value: 12, method: rand-lowweight-v1, seed: 5, iters: 2000} 很容易被读成「一份证书」。要分清三层。它是：一个可重跑的存在性见证。rand-lowweight-v1 是 QEC-Bank 的一种随机低重量搜索：在「与所有 Z 检查对易的 X 串」里随机取组合，去掉检查乘积，再用检查去削减重量（参数导读 3.3 节）。「随机」用的是 NumPy（Python 的数值计算库）的随机数发生器，种子是它的起始值：同一个种子每次产生同一串「随机数」，所以整个搜索可以一模一样地重跑。验证器（条目的例行检查程序）每次都用种子 5 重跑 2000 次迭代，必须再次得到重量 12 的逻辑算符，否则 make verify-entry 失败；它证明 d ≤ 12。它不是：一份 Lean 证书。契约里确有 distance-upper-bound@1 这一类（载荷恰为 {upper: u}，「proves only d <= u」），但 card.yaml 为 gross 登记的证书只有一份，就是 structural-validity；那个重量 12 的见证住在 instances.yaml（条目里逐条记录实例声明的数据文件）和 Python 验证器里，没有被封装成 Lean 检查过的证书。它更不是：下界。它对「不存在重量 11 的逻辑算符」一个字也没说；那一半是引文。所以即便将来把它打包成 distance-upper-bound@1 并通过 Lean，gross 的 d 也仍是 bounded——契约：成功的证书只把命题记入 discharges，「it does not rewrite the source origin」。

The gross line upper: {value: 12, method: rand-lowweight-v1, seed: 5, iters: 2000} on the parameters page is easily misread as “a certificate”. Three layers must be kept apart. It is: a rerunnable existence witness. rand-lowweight-v1 is a QEC-Bank random low-weight search: it takes random combinations among the “X strings that commute with every Z check”, discards products of checks, and uses checks to trim the weight (parameters guide, section 3.3). The randomness comes from the random-number generator of NumPy (Python's numerical library), and the seed is its starting value: the same seed produces the same stream of “random” numbers every time, so the whole search can be rerun identically. On every run the verifier (the entry's routine checking program) reruns 2,000 iterations with seed 5 and must again obtain a weight-12 logical, or make verify-entry fails; it proves d ≤ 12. It is not: a Lean certificate. The contract does have a class distance-upper-bound@1 (payload exactly {upper: u}, which “proves only d <= u”), but card.yaml registers a single certificate for gross, the structural-validity one; the weight-12 witness lives in instances.yaml (the entry's data file recording each instance's claims) and the Python verifier and has not been packaged into a Lean-checked certificate. It is even less: a lower bound. It says nothing about “no weight-11 logical exists”; that half is the citation. So even if it were one day packaged as distance-upper-bound@1 and passed Lean, gross's d would remain bounded: per the contract, a successful certificate only records the claim in its discharges, “it does not rewrite the source origin”.

条目文档 codes/bivariate_bicycle/pedagogy/derivations.md 的「Reproduction contract」（复现约定）规定了下面三行命令。你需要一份 QEC-Bank 仓库（本教程不附带），在仓库最顶层的目录里运行：第一行打开仓库自带的 Python 环境（.venv，装好了所需的库），第二行运行复现脚本，第三行用 make（按仓库预先写好的规则执行一组命令的工具）运行条目验证。

The “Reproduction contract” in the entry document codes/bivariate_bicycle/pedagogy/derivations.md prescribes the three command lines below. You need a copy of the QEC-Bank repository (not shipped with this tutorial) and run them from its top-level directory: the first line activates the repository's own Python environment (.venv, with the required libraries installed), the second runs the reproduction script, the third uses make (a tool that runs a set of commands according to rules written in the repository) to run the entry verification.

第一条脚本 reproduce.py 先调用 verify_entry（任何失败立即中止），再用一份独立写的循环移位重建 gross 的两个多项式，并逐条 assert：

The first script, reproduce.py, first calls verify_entry (any failure aborts at once), then rebuilds gross's two polynomials from an independently written cyclic shift and asserts, item by item:

第二条命令 make verify-entry 是条目级门禁：「The ordinary verifier independently checks both instances.yaml records」，并执行第 2 章的重放。证书那一层由仓库级门禁 python tools/build_formal_unification.py verify 覆盖：这条默认验证不调用 Lean 也不联网，只用 Python 独立重算每份证书，并与仓库里存档的证书字节逐位比对。真正调用 Lean、产出 Lean 证据的 replay 命令只在「封存运行时」上运行——一台固定版本的运行环境，目前只对一个精确平台（arm64-apple-darwin25.5.0，Lean v4.30.0-rc2）二进制兼容——并受 QEC-Bank 称为 Board contract 的规则约束（本系列没有展开这份规则；见表面码形式化导读 4.2 节）。所以在你自己的机器上：能重跑 reproduce.py、条目验证与 Python 层的证书核对；不能重新产出 Lean 证据。

The second command, make verify-entry, is the entry-level gate: “The ordinary verifier independently checks both instances.yaml records”, and it performs the replay of Chapter 2. The certificate layer is covered by the repository gate python tools/build_formal_unification.py verify: this default verification invokes neither Lean nor the network; it recomputes every certificate independently in Python and compares it bit by bit with the certificate bytes stored in the repository. The replay command, which actually invokes Lean and produces Lean evidence, runs only on the “sealed runtime”, a fixed-version runtime environment that is currently binary-compatible with one exact platform (arm64-apple-darwin25.5.0, Lean v4.30.0-rc2), and under rules the QEC-Bank calls a Board contract (this series does not spell those rules out; see section 4.2 of the surface-code formal guide). So on your own machine you can rerun reproduce.py, the entry verification and the Python-layer certificate checks; you cannot regenerate the Lean evidence.

derivations.md 的「Provenance split」把 BB 条目的结论分成三层，原文逐字转录如下（中间一列保留英文原文，右列用中文说明它的意思与证书覆盖情况）。

The “Provenance split” in derivations.md sorts the BB entry's conclusions into three layers, transcribed verbatim below, with the meaning and the certificate coverage in the right column.

第三层值得逐项点名，因为它们正是 BB 码最常被引用的数字。

• 深度 7 的症状电路与电路码距（把测量电路里任何位置的故障都算进去的码距，不只数数据比特上的错误；BB 教程 6.2 节）：证书只看静态矩阵，gross-parameter-ledger.md 明说「a distance-12 fault circuit」不能从静态账本推出。
• 0.8% 这个数：Bravyi 等人 2024 年的论文（arXiv:2308.07915）v1、v2 摘要里的数字，说的是「一族 LDPC 码」（a family of LDPC codes），不是 gross 一个码。它也不是「几种尺寸的曲线交于一点」那种阈值。论文对每个码分别解一个打平方程 p_L(p) = kp，解出这个码自己的「伪阈值」p₀：p 是每个电路位置的出错概率，p_L 是整块码每轮纠错失败（k 个逻辑比特里任何一个出错）的概率，kp 近似 k 个不编码的裸比特里至少一个出错的概率；p_L 只在 p ≥ 10⁻³ 处模拟，更小的 p 靠拟合公式外推。v2 的表 1 里五个码的 p₀ 是 0.0048 到 0.0069（gross 为 0.0065），正文说 144 与 288 比特两个码「close to 0.007」；0.8% 是这类每码伪阈值的一个整数化说法。噪声是「标准电路级噪声模型」（每个门、空闲、制备和读出都可能出错），症状由深度 7 的电路提取，译码器是 BP-OSD（置信传播加有序统计后处理的一种译码算法）；完整的五个限定项见 BB 教程 6.4 节。card.yaml 的译码器记录原话是「It is not a decoder-independent threshold of every BB construction: changing the family, CNOT order, detector model, noise normalization, or postprocessing defines a different threshold experiment」——它属于那一整套「家族 + 电路 + 探测器 + 归一化 + 译码器」的实验，不属于矩阵。
• BP-OSD 的性能：同理。
• 逻辑门（横向 CNOT、折叠横向门、自同构门、手术，6.5 节）：QEC-Bank 全部标 claimed；reproduce.py 证明了平移是自同构（重新给比特编号后检查的集合不变），intuition.md 紧接着说这个论证「does not identify its action on the twelve logical qubits」。所以这里的检查并不识别、也不认证任何一个具体的逻辑门。平移的逻辑作用是另外算出来的：Bravyi 等人（arXiv:2308.07915 v2，9.2 节「Logical Gates based on Automorphisms」）证明每个平移都是一个逻辑 CNOT 电路（差一个逻辑 Pauli 修正）；他们还写道除恒等平移外没有哪个平移作用成逻辑恒等，但对 gross 这一句不成立：x⁶（沿长为 12 的方向平移半圈）作用成逻辑恒等，其余 70 个非恒等平移有非平凡的逻辑作用（检验方法见直觉教程 6.5 节）。这个结论在文献里，不在 QEC-Bank 的证书里。
• 任意子解释（chen2025anyon）：把 BB 码读成一种拓扑物质的解释，放在表示阶梯最远离机器执行的一级 R5，标为 curated（从论文整理而来，不是构造器算出的）。
• 昆仑实验（Wang 等 2025，arXiv:2505.09684）：在 32 个长程耦合超导比特的「昆仑」处理器上运行 [[18,4,4]] BB 码（18 个数据比特加 14 个检查比特），报告每个逻辑比特每轮纠错的逻辑错误率 (8.91 ± 0.17)%。这个数带着几个限定：① 只统计没有检测到泄漏（比特跑出 0、1 两个能级）的实验次数，每个轮数 4 万次以上；② 纠错在事后的数据处理里完成，译码器是推广到电路级噪声模型的 BP-OSD；③ 先把逻辑错误概率对轮数拟合出整块每轮的失败率 p_L，再按 1 − (1 − p_L)^1/4 折算到每个逻辑比特；逻辑 Z 基与 X 基两组记忆实验各拟合一次，得 (9.15 ± 0.27)% 与 (8.67 ± 0.21)%，8.91% 是两者的平均；④ ± 0.17% 是一个标准差，包含统计与拟合的不确定度（BB 教程 6.6 节）。硬件结果，属于用例与实现侧面。
• 渐近坏（postema2025existence，即 Postema 与 Kokkelmans 的 arXiv:2502.17052，v3 定理 2.19）：让一串码的 n 越来越大，如果码率 k/n 或相对码距 d/n 趋于 0，这串码就叫「渐近坏」（两者都保持在某个正数之上才叫「渐近好」）。定理说：A、B 都是三项式（于是每条检查重量固定为 6）的任何一串 BB 码，n → ∞ 时都是渐近坏的；它不要求两个多项式固定，环面尺寸 l、m 和各项的指数都可以一路变化；证明得到的是 d/n → 0。这是文献定理，不是检查矩阵的证书能核对的东西；见参数导读 5.4 节。

检查程序封存时（QEC-Bank 的任务 T195）的结果文件对这一切早有总括：检查器不接受「decoder, threshold, hardware model」，也不接受「family-distance theorem」——所以连 bb72、bb288 那些 claimed 的 d，以及任何「对所有 l、m 成立」的论断，都在 Lean 之外。

The third layer deserves naming item by item, because these are precisely the most-quoted BB numbers.

• The depth-7 syndrome circuit and circuit distance (the distance counting faults anywhere in the measurement circuit, not only errors on data qubits; BB guide section 6.2): certificates see only the static matrix, and gross-parameter-ledger.md states that “a distance-12 fault circuit” does not follow from the static ledger.
• The 0.8% figure: the number in the v1 and v2 abstracts of Bravyi et al. 2024 (arXiv:2308.07915), stated for “a family of LDPC codes”, not for the gross code alone. Nor is it a threshold where curves for several sizes cross. The paper solves a break-even equation p_L(p) = kp separately for each code, giving that code's own “pseudo-threshold” p₀: p is the fault probability per circuit location, p_L the probability that the whole block fails in one round (any of its k logical qubits goes wrong), and kp approximates the probability that at least one of k bare, unencoded qubits fails; p_L is simulated only for p ≥ 10⁻³ and extrapolated below with a fitting formula. In v2's Table 1 the five codes have p₀ from 0.0048 to 0.0069 (0.0065 for gross), and the text says the 144- and 288-qubit codes are “close to 0.007”; 0.8% is a round figure for such per-code pseudo-thresholds. The noise is the “standard circuit-based noise model” (every gate, idle step, preparation and readout may fail), syndromes are extracted by a depth-7 circuit, and the decoder is BP-OSD (belief propagation followed by ordered-statistics post-processing, one decoding algorithm); the full five qualifiers are in BB guide section 6.4. The decoder record in card.yaml says “It is not a decoder-independent threshold of every BB construction: changing the family, CNOT order, detector model, noise normalization, or postprocessing defines a different threshold experiment”; it belongs to that whole family-plus-circuit-plus-detector-plus-normalisation-plus-decoder experiment, not to the matrix.
• BP-OSD performance: likewise.
• Logical gates (transversal CNOT, fold-transversal gates, automorphism gates, surgery, section 6.5): all claimed in the QEC-Bank; reproduce.py proves translations are automorphisms (relabelling the qubits leaves the set of checks unchanged), and intuition.md adds at once that this argument “does not identify its action on the twelve logical qubits”. So the check here does not identify or certify any particular logical gate. The logical action of a translation is computed elsewhere: Bravyi et al. (arXiv:2308.07915 v2, section 9.2 “Logical Gates based on Automorphisms”) show that every translation is a logical CNOT circuit, up to a logical Pauli correction; they also write that no translation other than the identity acts as the logical identity, but for gross that does not hold: x⁶ (a half-turn along the direction of length 12) acts as the logical identity, while the other 70 nonidentity translations have a nontrivial logical action (the check is described in §6.5 of the intuition guide). That result lives in the literature, not in the QEC-Bank certificates.
• The anyon interpretation (chen2025anyon): reading the BB code as a kind of topological matter, placed on R5, the rung of the representation ladder farthest from machine execution, and marked curated (collected from a paper, not computed by the constructor).
• The Kunlun experiment (Wang et al. 2025, arXiv:2505.09684): a [[18,4,4]] BB code (18 data qubits plus 14 check qubits) run on the “Kunlun” processor of 32 long-range-coupled superconducting qubits, reporting a logical error rate of (8.91 ± 0.17)% per logical qubit per error-correction cycle. The number carries several qualifiers: (1) only runs in which no leakage (a qubit leaving its two levels 0 and 1) was detected are counted, over 40,000 per number of rounds; (2) correction is done afterwards in data processing, with a BP-OSD decoder extended to the circuit-level noise model; (3) the logical error probability is fitted against the number of rounds to get the whole block's failure rate per round p_L, which is converted to a per-logical-qubit rate by 1 − (1 − p_L)^1/4; the logical Z-basis and X-basis memory experiments are fitted separately, giving (9.15 ± 0.27)% and (8.67 ± 0.21)%, and 8.91% is their average; (4) ± 0.17% is one standard deviation, covering statistical and fit uncertainty (BB guide section 6.6). A hardware result, belonging to the Use cases & realizations facet.
• Asymptotic badness (postema2025existence, i.e. Postema and Kokkelmans, arXiv:2502.17052, v3 Theorem 2.19): a sequence of codes with n growing is called “asymptotically bad” if its rate k/n or its relative distance d/n tends to 0 (“asymptotically good” if both stay above some positive number). The theorem says that any sequence of BB codes with A and B both trinomials (so every check has the fixed weight 6) is asymptotically bad as n → ∞; it does not require the two polynomials to stay fixed: the torus sizes l, m and the exponents of the terms may all change along the way; the proof gives d/n → 0. This is a literature theorem, not something a check-matrix certificate can check; see section 5.4 of the parameters guide.

The result file written when the checker was sealed (QEC-Bank task T195) covers all of this in advance: the checker accepts no “decoder, threshold, hardware model” and no “family-distance theorem”, so even the claimed d of bb72 and bb288, and any statement “for all l, m”, lie outside Lean.

回放一遍：BB 条目的两个实例各有一个语义哈希（gross 74f45e7b…，toric_L3 b469c20c…），分支都是 css-chain。它们的矩阵由 construction 块重放：bivariate_polynomial@1 跑两次得 A、B，bivariate_bicycle@1 拼成 [A | B] 与 [Bᵀ | Aᵀ]，exact-checkmatrix-v1 要求与构造器输出连行序、比特序都相同。两个实例都持有 structural-validity（n、k、css）；toric_L3 另持 small-exact-distance-enumeration（1431 个候选，在 65 536 之内）；gross 没有——候选数约 1.7 × 10²¹，且其 d 本就是 bounded——证据词不变。seed 5 的见证是可重跑的上界，不是 Lean 证书，更不是下界。两条命令在你的机器上重跑 Python 层的一切；深度 7、0.8%、逻辑门、昆仑、渐近坏在这一版证书体系之外。

Replay: the BB entry's two instances each have a semantic hash (gross 74f45e7b…, toric_L3 b469c20c…), both on the css-chain branch. Their matrices are replayed from the construction block: bivariate_polynomial@1 runs twice for A and B, bivariate_bicycle@1 assembles [A | B] and [Bᵀ | Aᵀ], and exact-checkmatrix-v1 demands equality with the constructor's output down to row and qubit order. Both instances hold structural-validity (n, k, css); toric_L3 also holds small-exact-distance-enumeration (1,431 candidates, under 65,536); gross does not, with about 1.7 × 10²¹ candidates and a d that was bounded to begin with, and its evidence word is unchanged. The seed-5 witness is a rerunnable upper bound, not a Lean certificate, still less a lower bound. Two commands rerun everything at the Python layer on your machine; depth 7, 0.8%, logical gates, Kunlun and asymptotic badness stay outside this version of the certificate system.