Section C, “Where the layer counts come from”Origin and limitations of the 20-to-42 layer bound
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
Where the layer counts come from. For the two-frame selector, the compositional Boolean-depth bound is : at most four levels extract the frame difference, four handle candidate tests and replacement bits, nine are allowed by the general selection construction (including fallback and output handling), and three encode the selected heap’s binary index. These are bounds on composed subcircuits, not necessarily the exact number of levels on a shortest implementation. The compiler then gives at most threshold layers. Similarly, Boolean depths , , and give the other entries in the table.
Generated from paper_jmlr.tex, lines 1546–1548.
2 Explain this
The number 42 comes from conservative accounting, not a training experiment or a lower bound. Difference extraction adds at most 4 Boolean levels; the candidate construction has bound 4; the generic selector allows 9 more; binary index encoding allows 3 more. The total bound 20 is converted to threshold layers. The generic compiler pads dependencies and reserves the two-layer cost of AND at every Boolean level. A specialised network may be smaller, but a sharper claim requires a new construction and proof.
From Boolean formulas to threshold layers
Exact trace and teaching example The checked compiler’s exact output is shown beside a hand-made teaching circuit; each part is labelled.
Every gate in these networks has weights and thresholds in . An OR gate fires when at least one of its literals is 1. NOT is a negated literal. An AND needs two layers: an OR of the negated inputs (that is, NOT AND), then a negated copy. Choose a formula and set the inputs. The hand-made circuit on the left uses the fewest layers possible in this gate model. The grid on the right is exactly what the checked compiler of Figure 8 builds for the same formula, with the value of every wire at every layer. The two answer the same truth table, but only the compiler comes with a general proof.
Formula: XOR(a, b) (Lean term: xor2 (input 0) (input 1) = or [and [a, not b], and [not a, b]]). Boolean depth d = 3, formula size 9.
Input: a = 1 b = 0
Teaching example A hand-made circuit
2 threshold layers, the fewest possible in this gate model. Every gate is an OR of literals with weights 1 and threshold 1, so an AND needs two layers (De Morgan).
| Layer | Gates |
|---|---|
| 1 | u = OR(¬a, b) → 0 v = OR(a, ¬b) → 1 |
| 2 | OR(¬u, ¬v) = XOR(a, b) → 1 |
Output: 1
Exact construction trace What the checked compiler builds
The network ThresholdNet.compileF produces for this formula, as Lean computes it: 8 layers (the bound is 2d + 2 = 8); each of the 7 computing layers has one wire per program gate (S = 9); 64 gates in total (the bound is (2d + 1)S + K = 64). Each cell shows what that wire does at that layer and its value on the input above. “·” is an idle wire (constant 0 until its inputs are ready); “copy” is an identity buffer. Layer 1 reads the inputs into the construction and the last layer arranges the outputs: these are the two extra layers in 2d + 2, and the factor 2 lets every Boolean level cost as much as an AND.
| Program gate | 1 | 2 | 3 | 4 | 5 | 6 | 7 | out |
|---|---|---|---|---|---|---|---|---|
| g0 = input a | in 1 | copy 1 | copy 1 | copy 1 | copy 1 | copy 1 | copy 1 | |
| g1 = input b | in 0 | copy 0 | copy 0 | copy 0 | copy 0 | copy 0 | copy 0 | |
| g2 = NOT g1 | · 0 | NOT 1 | copy 1 | copy 1 | copy 1 | copy 1 | copy 1 | |
| g3 = AND(g0, g2) | · 0 | · 0 | AND₁ 0 | AND₂ 1 | copy 1 | copy 1 | copy 1 | |
| g4 = input a | in 1 | copy 1 | copy 1 | copy 1 | copy 1 | copy 1 | copy 1 | |
| g5 = NOT g4 | · 0 | NOT 0 | copy 0 | copy 0 | copy 0 | copy 0 | copy 0 | |
| g6 = input b | in 0 | copy 0 | copy 0 | copy 0 | copy 0 | copy 0 | copy 0 | |
| g7 = AND(g5, g6) | · 0 | · 0 | AND₁ 1 | AND₂ 0 | copy 0 | copy 0 | copy 0 | |
| g8 = OR(g3, g7) | · 0 | · 0 | · 0 | · 0 | OR 1 | copy 1 | copy 1 | out 1 |
Output: 1
Truth table
| a b | formula | teaching circuit | compiled network | |
|---|---|---|---|---|
| 0 0 | 0 | 0 | 0 | agree |
| 0 1 | 1 | 1 | 1 | agree |
| 1 0 | 1 | 1 | 1 | agree |
| 1 1 | 0 | 0 | 0 | agree |
The two-frame selector’s depth bound is a sum of bounds for composed subcircuits:
- 4 · frame difference
- 4 · candidate tests and replacement bits
- 9 · selection, fallback and output
- 3 · binary index
Boolean depth ≤ 20 → the compiler’s rule 2d + 2 → at most 42 threshold layers.
For comparison, the actual formulas for small boards, measured by Lean (the compiler uses their real depth D, not the bound):
| Board size | depth D | layers 2D + 2 | width S (formula nodes) | gates (2D + 1)S + K |
|---|---|---|---|---|
| B = 2, N = 2 | 15 | 32 | 2,009 | 62,284 |
| B = 3, N = 3 | 15 | 32 | 13,228 | 410,074 |
| B = 3, N = 4 | 15 | 32 | 34,192 | 1,059,959 |
| B = 4, N = 4 | 15 | 32 | 63,145 | 1,957,503 |
The width counts every node of every output formula, duplicates included, so it is far from economical. These numbers describe the uniform construction, not an optimised network and not a trained one.
How this relates to the Lean proof. The grid is the output of ThresholdNet.compileF as Lean
evaluates it on these formulas; the browser only evaluates the exported gates. ThresholdNet.compileF_spec
proves, for any list of formulas of depth at most , that the network has at most layers and computes every
formula exactly. The selector bounds in the table of Appendix C come from this rule:
Family.rest_ac0 (Boolean depth at most 20) and Family.rest_net (at most 42
layers with weights and thresholds 0 or 1).
What this does not show. The 42-layer figure is an upper bound for one explicit, deliberately uniform construction. It is not a lower bound, not a layer count measured in an experiment, and not a statement about which networks training finds. A more economical network may use fewer layers: for the small boards in the table, the selector formulas Lean builds have depth 15, so even the uniform compiler produces 32 layers, below the bound of 42. Proving a sharper general bound would need a separate construction and proof.
A truth-table expansion can reduce Boolean depth to two AND–OR levels with negated inputs, but may require exponentially many gates. The polynomial-size condition is therefore essential when comparing these depth bounds.
3 How this is formalised
The compositional bounds are LocalRestore.restC_bound (depth ),
PriorityEncoder.restBin_bound (depth ), and
ThresholdInst.restNet_res (at most layers).
The general conversion is ThresholdNet.compileF_spec.
These existing theorems bound this construction; they do not prove depth optimality or learnability.
| Paper anchor | par:depth-accounting (manuscript label) |
|---|---|
| Displayed as | Section C, “Where the layer counts come from” |
| Claim | Origin and limitations of the 20-to-42 layer bound |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 1546–1548; SHA-256 of the normalised block source 0c5047726ffa41ef… |
| Depends on | Appendix C, table, Appendix C, “Realisation with fixed-scale threshold gates” |
| Explanations | explain/par:depth-accounting, formal/par:depth-accounting |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.
Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).