当「我证明了」
变成「机器核对过」 When “I proved it”
becomes “a machine checked it”

参数页的码距定理是好证明：短、对任何 L 成立、有文献支撑。但它依赖读者理解「不相交代表」这个想法。机器不理解想法，只会算。QEC-Bank 的证书certificate：绑定在一个有限对象上的数据包，附带一个可独立重算的检查器。检查器从对象本身重算每个字段并要求逐位相等；不接受任何「据称」的值。因此另起一套规则：一份证书是一包数据（例如「这个矩阵的化简结果是这些行、主元在这些列」），配一个通用检查器；检查器从对象本身重新算一遍，要求与数据完全一致。QEC-Bank 的契约文件（docs/design-references/2026-08-21-atlas-formal-ir-v1-contract.md）用一句话立下标准：「Supplying a rank integer alone is not a certificate」——只写一个「秩 = 6」不算证书，必须给出能被重算的化简矩阵。

The distance theorem in the parameters guide is a good proof: short, valid for every L, backed by the literature. But it relies on the reader grasping the idea of “disjoint representatives”. A machine grasps no ideas; it only computes. So the QEC-Bank certificateA data package bound to one finite object, together with an independently re-runnable checker. The checker recomputes every field from the object itself and demands bit-for-bit equality; no “stated” value is accepted. plays by different rules: a certificate is a package of data (for instance “the reduced form of this matrix has these rows, with pivots in these columns”) plus a generic checker; the checker recomputes everything from the object itself and requires exact agreement. The QEC-Bank contract (docs/design-references/2026-08-21-atlas-formal-ir-v1-contract.md) sets the standard in one sentence: “Supplying a rank integer alone is not a certificate”. Writing “rank = 6” is not a certificate; you must hand over a reduced matrix that can be recomputed.

另一条设计原则同样直白：证书「is generated from data; there are no per-code theorem files」。没有一份叫「表面码定理」的文件。同一台检查器对表面码、环面码、任何 CSS 码都做一样的事——正因为它对码一无所知，它的通过才有说服力。

A second design principle is equally blunt: a certificate “is generated from data; there are no per-code theorem files”. There is no file called “the surface-code theorem”. The same checker does the same thing for the surface code, the toric code, any CSS code, and precisely because it knows nothing about codes, its passing verdict carries weight.

QEC-Bank 的检查器用Lean一种交互式定理证明器兼编程语言。用 Lean 写的检查器，其正确性本身可以被 Lean 的内核审计（例如列出它依赖的全部公理）。实现，取名 qec-atlas-lean-complete-v1（表面码 card.yaml 中 lean.checker 一栏的原文）。它在 2026-08-21 的 QEC-Bank 任务 T195（QEC-Bank 用 T 加编号管理每一项工程任务）中被「封存」（sealed），意思是三件事：源代码逐字节冻结，以后改一个字节就不再是这台检查器；在一个断网的隔离环境里，从零构建和重放已有证书的全部测试都通过；并用 Lean 的内核列出它依赖的公理，结果只有 Lean 标准库自带的三条（propext、Classical.choice、Quot.sound，数学家日常默认的逻辑规则），源码里也没有 sorry（Lean 里「这一步先跳过、当作已证明」的占位符）。换句话说，检查器没有偷偷假设任何额外的东西。

The QEC-Bank checker is written in LeanAn interactive theorem prover and programming language. A checker written in Lean can itself be audited by Lean's kernel, for example by listing every axiom it depends on. and is named qec-atlas-lean-complete-v1 (the literal lean.checker field of the surface-code card.yaml). It was “sealed” in QEC-Bank task T195 (the QEC-Bank numbers every engineering task T plus a number) on 2026-08-21, which means three things: its source bytes are frozen, so changing one byte makes it a different checker; inside a network-denying sandbox, every test of building from scratch and of replaying existing certificates passed; and Lean's kernel listed the axioms it depends on, which turned out to be only the three shipped with Lean's standard library (propext, Classical.choice, Quot.sound, the logical rules mathematicians assume every day), with no sorry (Lean's placeholder for “skip this step and treat it as proved”) in the source. In other words, the checker assumes nothing extra behind your back.

同样重要的是 T195 结果文件写明它不接受什么：「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 成立的定理，不在机器核对的范围内；机器只核对一个个有限实例。这也解释了 QEC-Bank 形式化页上那句总纲：「Eligible small exact-distance certificates are additive; claims outside Lean Complete v1 keep their existing evidence origin」——证书是加上去的一层，加不上的声明保留原有的证据词（verified / bounded / claimed）。

Equally important, the T195 result states what it does not accept: “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 other words, the all-L theorem of the parameters guide is outside what the machine checks; the machine checks finite instances one at a time. This also explains the headline sentence of the QEC-Bank formal-verification page: “Eligible small exact-distance certificates are additive; claims outside Lean Complete v1 keep their existing evidence origin”. A certificate is a layer added on top; claims that cannot receive one keep their original evidence word (verified / bounded / claimed).

下面就是机器实际拿到的第一个对象：L3，13 个数据比特（n = 13）、6 条 X 检查、6 条 Z 检查，存 1 个逻辑比特（k = 1；n、k 的记账见 Toric Code 直觉教程「记账」一节，码距 d 的定义见同教程「它的致命弱点」一节）。本篇接下来的一切——身份、证书、复现——都是对这一块（以及 L4、L5 两块）说的，不是对「表面码」这个族名说的。

Below is the first object the machine actually receives: L3, with 13 data qubits (n = 13), 6 X-checks and 6 Z-checks, storing one logical qubit (k = 1; the n, k bookkeeping is in the toric guide's “ledger” section, and distance d is defined in its “fatal flaw” section). Everything that follows in this guide, identity, certificates, reproduction, is said about this patch (and its L4 and L5 siblings), never about the family name “surface code”.

Formal IRFormal intermediate representation：QEC-Bank 为每个已发布实例生成的、无散文的 JSON 文档（schema 为 qec-atlas-formal-ir-v1），把有限码对象、构造轨迹、声明、见证、证书和附件分放在固定字段里。是 QEC-Bank 为每个实例生成的一份 JSON 文档。JSON 是一种纯文本数据格式：花括号 {…} 里是一组字段，每个字段写成 "名字": 值，值可以是数、字符串、方括号 […] 里的列表，或者又一个 {…}。把内存里的数据写成这样一串文字、最终存成一串字节，叫序列化。这份文档顶层恰好十个字段：schema, profile, semantic, semantic_hash, claims, traces, witnesses, certificates, attachments, provenance。契约刻意把四件常被混在一起的东西分开：① 有限数学对象本身；② 生成它的构造轨迹；③ 关于它的命题、见证与证书；④ 电路、基准、引文等非形式化附件。只有第 ① 项进入哈希。原文给了理由：「a new proof or citation must not change which code object the hash names」——多一篇论文引用、多一份证书，对象还是那个对象。

The Formal IRFormal intermediate representation: the prose-free JSON document (schema qec-atlas-formal-ir-v1) the QEC-Bank generates for every shipped instance, placing the finite code object, construction traces, claims, witnesses, certificates and attachments in fixed fields. is a JSON document the QEC-Bank generates per instance. JSON is a plain-text data format: curly braces {…} hold a set of fields, each written "name": value, where a value can be a number, a string, a list in square brackets […], or another {…}. Writing data held in memory out as such text, and finally as a string of bytes, is called serialisation. This document has exactly ten top-level fields: schema, profile, semantic, semantic_hash, claims, traces, witnesses, certificates, attachments, provenance. The contract deliberately separates four things that are often mixed: (1) the finite mathematical object itself; (2) a construction trace that produces it; (3) propositions, witnesses and certificates about it; (4) non-formal attachments such as circuits, benchmarks and citations. Only item (1) feeds the hash. The reason is stated: “a new proof or citation must not change which code object the hash names”. Add a paper, add a certificate, and the object remains the same object.

语义哈希semantic_hash：对 Formal IR 中 semantic 对象的规范字节做 SHA-256 得到的 64 位十六进制串；它就是该有限码对象在 QEC-Bank 中的身份。的配方在契约第 10 节：先把 semantic 对象写成规范字节canonical bytes：按 RFC 8785 JSON 规范化方案（键排序、无空白、UTF-8、无 BOM、无尾换行）得到的唯一字节串。同一对象无论谁来序列化，字节都相同。（RFC 8785，键排序、无空白），再在前面接上域前缀 qec-atlas-formal-ir-v1 和一个零字节（前缀给这串字节贴上「这是 Formal IR 对象」的标签：别种数据即使恰好写成同样的字节，加上各自不同的前缀后，送进 SHA-256 的输入也不同。前缀只负责区分输入的类别。两份不同的输入会不会恰好得到同一个哈希，要靠 SHA-256 本身的抗碰撞性：按 NIST 的定义，在可行的计算量内找不到这样一对输入。这是计算上的保证，不是数学上的「不可能」），对整体做 SHA-256一种密码学摘要函数：任意长度输入 → 固定 256 位（64 位十六进制）输出；改动输入的任一比特，输出面目全非；在可行的计算量内，既不能从输出反推输入，也找不到两份输出相同的不同输入。。规范化是关键：同一个矩阵不管谁来序列化，字节都一样，哈希才一样。契约还要求 Python 与 Lean 各自独立算出相同的哈希，并且「A supplied hash is never trusted」——文档里写着的哈希只是给人看的，检查器永远自己重算。

The recipe for the semantic hashsemantic_hash: the 64-hex-digit SHA-256 of the canonical bytes of the Formal IR's semantic object; it is the identity of that finite code object in the QEC-Bank. is contract section 10: write the semantic object as canonical bytesThe unique byte string produced by the RFC 8785 JSON Canonicalization Scheme (sorted keys, no whitespace, UTF-8, no BOM, no trailing newline). Whoever serialises the same object gets the same bytes. (RFC 8785, sorted keys, no whitespace), prepend the domain prefix qec-atlas-formal-ir-v1 and one zero byte (the prefix labels the bytes “this is a Formal IR object”: even if some other kind of data happens to serialise to the same bytes, its own different prefix makes the input to SHA-256 different. The prefix only separates input domains. Whether two different inputs could still give the same hash rests on SHA-256's collision resistance: in NIST's definition, finding such a pair is computationally infeasible. That is a computational guarantee, not a mathematical impossibility), and take the SHA-256A cryptographic digest: input of any length → a fixed 256-bit (64 hex digit) output; flipping one input bit scrambles the output; with feasible computation one can neither recover an input from its output nor find two different inputs with the same output. of the whole. Canonicalisation is the crux: the same matrix serialised by anyone yields the same bytes, hence the same hash. The contract further requires Python and Lean to compute the same hash independently, and states “A supplied hash is never trusted”: the hash written in a document is for humans; the checker always recomputes its own.

一个能核对的例子。下面是一个玩具 semantic 对象（两个字段是为演示编的，不是 QEC-Bank 的真实字段；真实的 L3 对象见下一段）。两个人把同一个对象写成了两段不同的文字：

A worked example you can check. Below is a toy semantic object (its two fields are made up for the demonstration and are not the QEC-Bank's real fields; the real L3 object follows in the next paragraph). Two people serialised the same object into two different texts:

规范化做三件事：字段按名字排序（n 排在 rows 前面），删掉所有空格和换行，再按 UTF-8 把每个字符变成字节。A 和 B 于是得到同一串 24 个字节。接着在前面接上 22 字节的前缀 qec-atlas-formal-ir-v1 和 1 个零字节，一共 47 个字节，这就是送进 SHA-256 的全部输入（十六进制，每两位一个字节）：

Canonicalisation does three things: it sorts the fields by name (n before rows), deletes every space and line break, and turns each character into bytes by UTF-8. A and B therefore give the same 24 bytes. Prepending the 22-byte prefix qec-atlas-formal-ir-v1 and one zero byte gives 47 bytes, the entire input to SHA-256 (in hexadecimal, two digits per byte):

真实的 L3 对象，以及「改哪里会换身份」。L3 的 semantic 有三块：identity（所属条目 surface、实例标签 L3、参数 L = 3），native（原生分支 css-chain、n = 13、H_X 与 H_Z 各 6 行 13 列），lowering（同样的 12 条检查改写成统一的「先 X 位、后 Z 位」26 列格式）。用上面的配方对它重算，得到 8442e560b9de5fb4…，与卡片上的值逐位相同（本页用 QEC-Bank 仓库里的 Formal IR 文件重算过）。再做三次改动对照：

The real L3 object, and which edits change the identity. L3's semantic has three blocks: identity (owning entry surface, instance label L3, parameter L = 3), native (native branch css-chain, n = 13, H_X and H_Z with 6 rows and 13 columns each), and lowering (the same 12 checks rewritten in a uniform “X bits, then Z bits” 26-column format). Recomputing it with the recipe above gives 8442e560b9de5fb4…, identical bit for bit to the card's value (this page recomputed it from the Formal IR file in the QEC-Bank repository). Now compare three edits:

加引文不改变哈希，因为 attachments 根本不在哈希的输入里，这正是 2.1 节「只有第 ① 项进入哈希」的意思。改一个矩阵比特，就成了另一个对象。标签也在 semantic 的 identity 块里，所以同一个矩阵换个标签也会换哈希：哈希锁定的是「这个带标签的实例，连同它的矩阵」。

Adding a citation leaves the hash alone because attachments are not part of the hash input at all, which is what “only item (1) feeds the hash” in §2.1 means. Flipping one matrix bit makes a different object. The label also sits in the identity block of semantic, so the same matrix under another label gets another hash: the hash pins down “this labelled instance together with its matrix”.

QEC-Bank 形式化页登记了三行。「native branch」一栏写的都是 css-chain：Formal IR 有四条分支branch：Formal IR 描述有限对象的四种原生方式之一：static stabilizer（静态稳定子）、css-chain（CSS 链复形）、subsystem/gauge（子系统/规范）、measurement schedule（测量时序）。表面码走 css-chain。——静态稳定子、CSS 链复形、子系统/规范、测量时序——表面码作为 CSS 码走 css-chain，对象由 H_X、H_Z 两块矩阵给出。哈希前缀取自页面；完整 64 位值在 card.yaml 的 formalization.instances 里。

The QEC-Bank formal-verification page registers three rows. The “native branch” column reads css-chain throughout: the Formal IR has four branchesOne of the four native ways the Formal IR describes a finite object: static stabilizer, css-chain (CSS chain complex), subsystem/gauge, measurement schedule. The surface code uses css-chain., static stabilizer, CSS chain, subsystem/gauge, measurement schedule, and the surface code, being CSS, uses css-chain, the object given by the two matrices H_X, H_Z. The hash prefixes are as shown on the page; the full 64-digit values sit in formalization.instances of card.yaml.

每份证书自己也有一个由内容决定的名字，格式固定为 certificate:<对象哈希>:<类别>:<证书内容哈希>@1。例如 L3 的结构证书在 card.yaml 里写作：

Each certificate likewise carries a content-determined name in the fixed format certificate:<object hash>:<kind>:<payload hash>@1. For instance, the L3 structural certificate appears in card.yaml as:

契约第 5 节规定「Every emitted instance must carry a structural-validity@1 certificate」。它的检查器要做的事，正是参数页 2.2 节那道算术的机器版：对稳定子矩阵做规范 RREFreduced row echelon form，行最简形：对 0/1 矩阵做模 2 的高斯消元，从左到右选主元，得到的唯一形态。证书提供期望的 RREF 与主元列，检查器重算并要求完全相等（canonical-rref-v1）。（模 2 高斯消元），从矩阵宽度读出 n，由秩公式得到 k，再验证「表示层面的 CSS 判据」（X 行与 Z 行两两正交，即 H_XH_Z^T = 0）。证书的载荷字段是固定的：branch, stabilizer: {rref, pivots}, gauge_span, computed: {n, k, css, dynamic_k}, schedule。检查器「recomputes every field from semantic; no field is accepted as an assumption」。

Contract section 5 rules that “Every emitted instance must carry a structural-validity@1 certificate”. What its checker does is the machine edition of the arithmetic in section 2.2 of the parameters guide: it puts the stabilizer matrix into canonical RREFReduced row echelon form: Gaussian elimination mod 2 on a binary matrix with pivots chosen left to right, yielding a unique shape. The certificate supplies the expected RREF and pivot columns; the checker recomputes and demands exact equality (canonical-rref-v1). (Gaussian elimination mod 2), reads n from the matrix width, gets k from the rank formula, and verifies the presentation-level CSS predicate (every X row orthogonal to every Z row, i.e. H_XH_Z^T = 0). The payload fields are fixed: branch, stabilizer: {rref, pivots}, gauge_span, computed: {n, k, css, dynamic_k}, schedule. The checker “recomputes every field from semantic; no field is accepted as an assumption”.

它解除（discharge）的命题是 validity, n, k, css。契约同样明确它永远不解除什么：「It never discharges distance, decoder, circuit, or family claims.」所以三个实例的 n = 13 / 25 / 41、k = 1、css = true 都有了 Lean 核对；码距要靠下一类。

The propositions it discharges are validity, n, k, css. The contract is equally explicit about what it never discharges: “It never discharges distance, decoder, circuit, or family claims.” So n = 13 / 25 / 41, k = 1 and css = true for all three instances are Lean-checked; distance needs the next class.

码距的证书要证两件事。上界容易：给出一个重量恰为 d 的逻辑见证static-logical@1 witness：一个 Pauli 行向量，与所有稳定子对易且不在稳定子的行空间内；载荷恰为 {pauli, weight}，检查器重算其重量。——一个与所有检查对易、却不是检查乘积的 Pauli 算符，检查器重算它的重量。直觉教程里的横跨串就是这样的见证。下面的实验台让你亲手做一个示意性的逻辑见证：在固定的 L = 5 贴片（n = 41 个比特）上画一条串，实验台同时检查 X、Z 两部分是否都不触发警报、又不是检查的乘积，然后显示它的重量 u 和由此得到的 d ≤ u（d = 码距，u = 见证的重量）。它不是 QEC-Bank 的证书：没有绑定对象的语义哈希，也没有证书规定的载荷格式和内容哈希，只演示见证本身的逻辑。

A distance certificate must prove two things. The upper bound is easy: exhibit a logical witnessA static-logical@1 witness: a Pauli row vector that commutes with every stabilizer and lies outside the stabilizer row space; its payload is exactly {pauli, weight}, and the checker recomputes the weight. of weight exactly d, a Pauli that commutes with every check yet is not a product of checks, whose weight the checker recomputes. The spanning strings of the intuition guide are exactly such witnesses. The bench below lets you build an illustrative logical witness by hand: draw a string on the fixed L = 5 patch (n = 41 qubits); the bench checks that neither its X part nor its Z part trips an alarm and that it is not a product of checks, then shows its weight u and the resulting d ≤ u (d = distance, u = the witness's weight). It is not a QEC-Bank certificate: it is not bound to the object's semantic hash and has neither the certificate's payload format nor its content hash; it only demonstrates the logic of a witness.

下界才是贵的那一半。契约第 7 节要求：对每一个重量小于 d 的非恒等 Pauli 算符（X、Y、Z 三种取值都算），按固定顺序 weight-then-support-lexicographic-then-X-Y-Z-v1 排好，逐个给出一条「分类」：要么 {kind: "anticommutes", stabilizer_row}——它与第几条检查反对易（会触发警报）；要么 {kind: "in-span", coefficients}——它是哪些检查的乘积（无害）。检查器重新生成整条候选流，「classifications cannot omit, duplicate, or reorder candidates」。这就是参数页里 exact-css-enum 那句「穷举」被写成可核对数据后的样子。

The lower bound is the expensive half. Contract section 7 demands: for every non-identity Pauli of weight below d (X, Y and Z on each qubit all count), sorted in the fixed order weight-then-support-lexicographic-then-X-Y-Z-v1, one “classification” each: either {kind: "anticommutes", stabilizer_row}, naming a check it anticommutes with (so it would trip an alarm), or {kind: "in-span", coefficients}, naming the checks it is a product of (so it is harmless). The checker regenerates the entire candidate stream, and “classifications cannot omit, duplicate, or reorder candidates”. This is what the word “exhaustive” behind exact-css-enum in the parameters guide looks like once written as checkable data.

看一个小到能全部写出来的例子：L = 2 的平面码，n = 5、d = 2（它的检查矩阵见参数页 2.2 节的折叠框，比特编号 q0…q4 用构造器的编号，对应那里的 h₀₀、h₁₀、h₀₁、h₁₁、v）。重量小于 2 的候选只有重量 1 的那些：5 个比特 × 3 种 Pauli = 15 个。按规定顺序，候选流从 X_q0、Y_q0、Z_q0 开始，再到 q1……每一个都碰到某条检查、会报警，所以 15 条分类全是 anticommutes。下面逐条写出（示意：检查行编号 0、1 是两条 X 检查，2、3 是两条 Z 检查；这是按同样规则手算的，不是证书原文）。判断规则很简单：单比特的 X 与一条检查反对易，当且仅当这条检查是 Z 型且碰到这个比特；Z 反过来看 X 型检查；Y 同时含 X 和 Z，两类都看。有几条可选时，下表的分类取编号最小的一条。图 3.1 和它下面的支撑表给出全部四条检查，15 条候选全部列在其后：

Here is an example small enough to write out in full: the L = 2 planar code, n = 5, d = 2 (its check matrices are in the fold of §2.2 of the parameters page; qubits q0…q4 use the constructor's numbering and correspond to h₀₀, h₁₀, h₀₁, h₁₁, v there). The candidates of weight below 2 are just those of weight 1: 5 qubits × 3 Paulis = 15. In the prescribed order the stream starts X_q0, Y_q0, Z_q0, then q1, and so on. Each one hits some check and would raise an alarm, so all 15 classifications are anticommutes. They are written out below (an illustration: check rows 0 and 1 are the two X checks, 2 and 3 the two Z checks; computed by hand with the same rule, not copied from a certificate). The rule is simple: a single-qubit X anticommutes with a check exactly when the check is Z-type and touches that qubit; Z is the same with X-type checks; Y contains both X and Z, so both kinds count. When several rows qualify, the table below lists the lowest-numbered one. Figure 3.1 and the support table under it give all four checks; all 15 candidates follow:

15 条都不是逻辑算符，所以 d ≥ 2。再附一个重量 2 的见证：Z_q0Z_q2（上面一行的两条横边 h₀₀、h₀₁ 各放一个 Z，从左毛边走到右毛边，图 3.1 的蓝色粗线）。它与行 0 的星共享 q0、q2 两个比特，与行 1 的星共享 0 个，都是偶数，所以全部对易。它是不是 Z 检查的乘积？两条 Z 检查只能组合出四种乘积，逐个写出来比一比：

None of the 15 is a logical operator, so d ≥ 2. Add one witness of weight 2: Z_q0Z_q2 (a Z on each of the two horizontal edges h₀₀, h₀₁ of the top row, from the left rough edge to the right one; the thick blue line in Figure 3.1). It shares two qubits, q0 and q2, with the row-0 star and none with the row-1 star, both even numbers, so it commutes with every check. Is it a product of Z checks? The two Z checks can form only four products; write them all out and compare:

四种都不是 Z_q0Z_q2，所以它不是检查的乘积，是真正的逻辑算符，d ≤ 2。两半合起来 d = 2。L3 的证书做的是同一件事，只是候选有 741 个。

None of the four is Z_q0Z_q2, so it is not a product of checks: it is a genuine logical operator, and d ≤ 2. Together, d = 2. The L3 certificate does the same thing with 741 candidates.

算术。候选数是 Σ_w=1^d−1 C(n,w)·3^w重量恰为 w 的非恒等 Pauli 算符个数：从 n 个比特里选 w 个（组合数 C(n,w)，读「n 选 w」），每个选中的比特取 X、Y、Z 之一（3^w 种）。对 w 从 1 到 d−1 求和。。契约给这类证书设了一道上限：候选总数 ≤ 65 536，上限本身的来源记为 {kind: bounded, method: t189-lean-complete-v1-certificate-size-policy}。按公式代入三个实例（下表由公式算得，不是 QEC-Bank 页面上的数字）：L3 只有 741 个候选；L4 是 64 875 个，恰好挤进上限；L5 则要 8 498 193 个，超出上限一百多倍。契约说得清楚：「Crossing it means unsupported, not false」——超限叫「不支持」，不叫「错」。这和参数页 3.3 节里 L5 的穷举并不矛盾：那里的 exact-css-enum 只试纯 X 与纯 Z 算符，重量 1 到 4 各一遍，约 23 万次（2 × 112 791 = 225 582）；Lean 证书要把 X、Y、Z 的所有组合逐条写进数据，才会到 850 万条。卡住 L5 的是证书大小的策略上限，不是计算量。

Arithmetic. The candidate count is Σ_w=1^d−1 C(n,w)·3^wThe number of non-identity Paulis of weight exactly w: choose w of the n qubits (the binomial coefficient C(n,w), read “n choose w”), then pick X, Y or Z on each chosen qubit (3^w ways). Sum over w from 1 to d−1.. The contract places a ceiling on this class: total candidates ≤ 65,536, the ceiling's own origin recorded as {kind: bounded, method: t189-lean-complete-v1-certificate-size-policy}. Evaluating the formula for the three instances (the table below is computed from the formula, not copied from a QEC-Bank page): L3 has only 741 candidates; L4 has 64,875 and just squeezes under the ceiling; L5 would need 8,498,193, over a hundred times too many. The contract is clear: “Crossing it means unsupported, not false”. This does not contradict §3.3 of the parameters page, where L5 is enumerated: exact-css-enum there tries only pure-X and pure-Z operators of weights 1 to 4, about 230,000 tests (2 × 112,791 = 225,582), whereas the Lean certificate must write every combination of X, Y and Z into its data, 8.5 million entries. What stops L5 is the policy cap on certificate size, not the amount of computation.

策略。即使算力够，这类证书也只为「verified 的精确码距声明」生成：形式化统一结果文件写道，小规模精确类「is generated only for verified exact-distance claims whose complete lower-weight Pauli enumeration fits the frozen 65,536-candidate policy」。而 L5 的码距是 bounded——下界来自定理与文献，上界来自种子搜索的见证。两道门 L5 都没过，所以它只有 structural-validity 一类；它的 d 保留原有证据词 bounded，一字未改。

Policy. Even with the compute to spare, this class is generated only for verified exact-distance claims: the formal-unification result 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”. And the L5 distance is bounded, its lower bound from a theorem and the literature, its upper bound from a seeded-search witness. L5 fails both gates, so it holds only structural-validity; its d keeps its original evidence word bounded, unchanged.

QEC-Bank 的 codes/surface/pedagogy/derivations.md 把复现写成契约。在仓库根目录：

The QEC-Bank file codes/surface/pedagogy/derivations.md writes reproduction down as a contract. From the repository root:

第一条脚本 reproduce.py 导入已发布的构造器，逐条断言教学页用到的每个计算结论：L = 3、4、5（L = 家族变量）的检查矩阵与近邻几何、秩 L(L−1)、行/列逻辑代表的「逻辑、等价、不相交」三性质、L3 的症状漫步reproduce.py 中的 L3 例子：单个 X 错误 → 一对警报；靠边的错误 → 单个警报；三个比特的一行 → 零警报且是逻辑算符。、L3 与 L4 的精确码距（exact-css-enum）、L5 的种子上界见证 {value: 5, method: rand-lowweight-v1, iters: 2000, seed: 0}、含帮手的资源计数，以及 L3 光边合并矩形 n=28, k=1, checks=27, d=3（n = 物理比特数，k = 逻辑比特数，checks = 检查数，d = 码距）。「It exits nonzero on the first disagreement」——任何一条不符，脚本立即以非零退出。第二条命令是条目级门禁，独立重跑 instances.yaml 中的每条声明。

The first script, reproduce.py, imports the shipped constructor and asserts every computed statement the pedagogy pages use: check matrices and nearest-neighbour geometry for L = 3, 4, 5 (L = family variable), the ranks L(L−1), the three properties (logical, equivalent, disjoint) of the row/column representatives, the L3 syndrome walkThe L3 example in reproduce.py: one X error → a pair of alarms; an error at the edge → a single alarm; a full row of three qubits → zero alarms, and a logical., the exact distances at L3 and L4 (exact-css-enum), the L5 seeded upper witness {value: 5, method: rand-lowweight-v1, iters: 2000, seed: 0}, the ancilla-inclusive resource counts, and the L3 smooth-merge rectangle n=28, k=1, checks=27, d=3 (n = physical qubits, k = logical qubits, checks = number of checks, d = distance). “It exits nonzero on the first disagreement.” The second command is the entry-level gate; it independently reruns every claim in instances.yaml.

证书那一层由仓库级门禁 python tools/build_formal_unification.py verify 覆盖。formal/ir/README.md 说明它做什么：「Default verification never invokes Lean or the network: it regenerates the Python projection, checks every certificate independently, compares the committed bytes, and validates the sealed-runtime identity.」也就是说，日常验证是用 Python 独立重算每份证书并与提交的字节比对；真正调用 Lean 的 replay 命令是「evidence-producing」的，只能在一项明确授权的 Board 任务下（Board 是 QEC-Bank 的任务登记表，每项任务写明谁在改什么），用那台封存的运行时执行。那台运行时目前只能在一种精确的机器上运行：苹果 ARM 芯片、macOS 的 Darwin 内核 25.5.0（平台标识 arm64-apple-darwin25.5.0），Lean 版本 v4.30.0-rc2。所以你在自己的机器上能做的是：重跑 Python 投影与证书核对；不能做的是：重新产出 Lean 证据。两者 QEC-Bank 都写在明处。

The certificate layer is covered by the repository gate python tools/build_formal_unification.py verify. formal/ir/README.md explains what it does: “Default verification never invokes Lean or the network: it regenerates the Python projection, checks every certificate independently, compares the committed bytes, and validates the sealed-runtime identity.” That is, everyday verification recomputes every certificate independently in Python and compares against the committed bytes; the replay command that actually invokes Lean is “evidence-producing” and may run only under an explicitly authorised Board task (the Board is the QEC-Bank task register, where each task states who changes what), on the sealed runtime. That runtime currently runs on exactly one kind of machine: Apple ARM hardware with macOS's Darwin kernel 25.5.0 (platform string arm64-apple-darwin25.5.0), Lean version v4.30.0-rc2. So on your own machine you can rerun the Python projection and certificate checks; you cannot regenerate the Lean evidence. The QEC-Bank states both in the open.

derivations.md 的「provenance split」把表面码条目的结论分成三层。机器验证：n、k、CSS 结构、两个小实例的精确码距。定理与文献 + 可重跑见证：L5 的下界与上界，故标 bounded。纯文献声明：「Thresholds and hardware results are not properties of a bare check matrix. They remain literature claims with the complete noise model and decoder written beside each number.」阈值（译码器教程的阈值账本列了四个，每个都写明它的噪声模型与译码器）、Willow 的 Λ = 2.14 ± 0.02（码距 3、5、7 的存储实验，离线神经网络译码器，arXiv:2408.13687；Λ：码距每增 2 时逻辑错误率的压制倍数，是设备与译码器的拟合值，不是阈值 p_th 与物理错误率 p 之比 p_th/p 的直接测量）——每个数都属于不同的噪声模型与译码器，QEC-Bank 在译码器教程的阈值账本里逐条列出限定项；它们今天都在 Lean Complete v1 之外：当前的证书只看一个有限的检查矩阵，这些声明保留原有的证据来源。同理，逻辑操作（格点手术、横向门等）在 QEC-Bank 中一律是 claimed：T195 明说它不接受「decoder, threshold, hardware model」。

The “provenance split” in derivations.md sorts the surface-code entry's conclusions into three layers. Machine-verified: n, k, CSS structure, and the two small exact distances. Theorem and literature plus a re-runnable witness: the L5 lower and upper bounds, hence bounded. Literature claims only: “Thresholds and hardware results are not properties of a bare check matrix. They remain literature claims with the complete noise model and decoder written beside each number.” The thresholds (the decoders guide's threshold ledger lists four, each with its noise model and decoder) and Willow's Λ = 2.14 ± 0.02 (a distance-3, 5, 7 memory experiment decoded offline by a neural network, arXiv:2408.13687; Λ: the factor by which the logical error rate drops when the distance grows by 2, a device-and-decoder fit, not a direct measurement of the ratio p_th/p of threshold to physical error rate) each belong to a different noise model and decoder; the QEC-Bank lists the qualifiers line by line in the threshold ledger of the decoders guide. All of them are outside Lean Complete v1 today: the current certificates see only a finite check matrix, and these claims keep their existing evidence origin. Likewise every logical operation (lattice surgery, transversal gates and so on) is claimed in the QEC-Bank: T195 states outright that it accepts no “decoder, threshold, hardware model”.

回放一遍：证书是数据加一台不信任任何人的检查器，一次只核对一个有限对象；Lean Complete v1 是 QEC-Bank 封存的那台检查器，明文列出它不接受的东西。每个实例的身份是 semantic 对象规范字节的 SHA-256，证明与引用都不进入哈希。三个实例都持有 structural-validity（n、k、css）；L3、L4 另持 small-exact-distance-enumeration（741 与 64 875 个候选，均在 65 536 上限内）；L5 因超限且本就 bounded 而没有，证据词不变。两条命令能在你的机器上重跑 Python 层的一切；Lean 证据的再生产只在封存运行时上进行。阈值、硬件与逻辑操作目前在 Lean Complete v1 之外。

Replay: a certificate is data plus a checker that trusts no one, checking one finite object at a time; Lean Complete v1 is the QEC-Bank's sealed checker, with an explicit list of what it does not accept. Each instance's identity is the SHA-256 of the canonical bytes of its semantic object; proofs and citations never enter the hash. All three instances hold structural-validity (n, k, css); L3 and L4 also hold small-exact-distance-enumeration (741 and 64,875 candidates, both under the 65,536 ceiling); L5 does not, being over the ceiling and bounded to begin with, and its evidence word is unchanged. Two commands rerun everything at the Python layer on your machine; regenerating Lean evidence happens only on the sealed runtime. Thresholds, hardware and logical operations are outside Lean Complete v1 today.