Appendix C, tableCertified depth and layer bounds for one evaluation of each component

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

Component	Boolean depth	Threshold layers
Two-frame binary move selector	$\le20$	$\le42$
Multi-head binary readout, given outcomes	$\le19$	$\le40$
One structured policy’s binary move output	$\le17$	$\le36$
One recurrent state update and output	$\le8$	$\le18$
One shootout controller tick	$\le34$	$\le70$

Generated from paper_jmlr.tex, lines 1531–1543.

2 Explain this

The table gives certified, unoptimised bounds for one evaluation of each component, as Boolean depth and as threshold layers: two-frame move selector ≤20 / ≤42; multi-head readout given outcomes ≤19 / ≤40; one policy step ≤17 / ≤36; one recurrent update ≤8 / ≤18; one shootout controller tick ≤34 / ≤70. Together with polynomial size bounds, they certify the components' AC⁰ resources.

Caveat: these are per evaluation. A rollout or a row scan repeats evaluations, and that time is part of the algorithm.

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 $\{0,1\}$ . 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:

4493

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 $d$ , that the network has at most $2d+2$ 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.

Depicted in Lean: ThresholdNet.orGate_eval, ThresholdNet.constGate_eval, ThresholdNet.layerAt, ThresholdNet.compileF, ThresholdNet.compileF_spec, ThresholdNet.compileF_fixed_grid, Family.rest_ac0, Family.rest_net. Explains the paper’s Figure 8.

The grid is the network Lean itself computes for each formula; your browser only evaluates its gates (agreement with Lean's evaluation was checked for all 4 formulas and every input at build time). The hand-made circuit is a teaching example, not part of the checked construction.

3 How this is formalised

Each row is a family certificate for the actual objects used elsewhere:

Component	Formula family (depth)	Network family (layers)
Two-frame selector	`Family.rest_ac0` (20)	`Family.rest_net` (42)
Multi-head readout	`Family.mh_ac0` (19)	`Family.mh_net` (40)
One policy step	`Family.pol_ac0` (17)	`Family.pol_net` (36)
Recurrent update	`Family.ctrl_ac0` (8)	`Family.ctrl_net` (18)
Shootout tick	`Shootout.sh_ac0` (34)	`Shootout.sh_net` (70)

The certificates assert existence of formulas of the stated depth with total size polynomial in the actual input length of the component, uniformly over the admissible $(B,N)$ ; the network certificates use $W=1$ .

Coverage record
Paper anchor	`par-realisation-with-fixed-scale-threshold-gates-table1` (website anchor; the manuscript has no label here)
Displayed as	Appendix C, table
Claim	Certified depth and layer bounds for one evaluation of each component
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1531–1543; SHA-256 of the normalised block source `8bc8f4451c54e341…`
Lean declarations	`NimAudit.Family.rest_ac0` (Family, lines 312–316, file `7a647f0a667d…`) `NimAudit.Family.rest_net` (Family, lines 320–326, file `7a647f0a667d…`) `NimAudit.Family.mh_ac0` (Family, lines 418–420, file `7a647f0a667d…`) `NimAudit.Family.mh_net` (Family, lines 424–428, file `7a647f0a667d…`) `NimAudit.Family.pol_ac0` (Family, lines 371–374, file `7a647f0a667d…`) `NimAudit.Family.pol_net` (Family, lines 378–382, file `7a647f0a667d…`) `NimAudit.Family.ctrl_ac0` (Family, lines 475–479, file `7a647f0a667d…`) `NimAudit.Family.ctrl_net` (Family, lines 483–502, file `7a647f0a667d…`) `NimAudit.Shootout.sh_ac0` (Shootout, lines 1196–1201, file `1abd814426d3…`) `NimAudit.Shootout.sh_net` (Shootout, lines 1203–1222, file `1abd814426d3…`)
Prose-to-formal notes	Each bound is for one evaluation of the component (one move selection, one policy step, one controller update or tick). The time needed to repeat evaluations is part of the algorithm, not of these bounds.
Audited correspondence rows	`app:impl`
Explanations	`explain/c-depth-table`, `formal/c-depth-table`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Family.rest_ac0`

Module Family (lean/phase6/Family.lean, lines 312–316) · file SHA-256 7a647f0a667d5ede… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

TWO-FRAME FORMULA FAMILY CERTIFICATE (depth ≤ 20, total size polynomial in 2BN, reading only the two frames).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.AC0Fam NimAudit.Family.restAdm NimAudit.Family.restLen
  (fun i => NimAudit.ThresholdInst.bForms (NimAudit.Family.restS i)) 20

Exact source text, lines 312–316

312/-- TWO-FRAME FORMULA FAMILY CERTIFICATE (depth ≤ 20, total size polynomial in 2BN,313    reading only the two frames). -/314theorem rest_ac0 : AC0Fam restAdm restLen (fun i => bForms (restS i)) 20 :=315  bin_cert restLen_pos (fun i _ => rest_bound i) (fun _ _ => Nat.le_refl _)316    (fun i _ => Nat.le_refl _) rest_sizePoly

Project declarations in the statement: Family.AC0Fam, Family.restAdm, Family.restLen, Family.restS, ThresholdInst.bForms

Project declarations used by the proof or definition body

Family.bin_cert, Family.restAdm, Family.restLen, Family.restLen_pos, Family.restS, Family.restSz, Family.rest_bound, Family.rest_sizePoly, WholeGame.rIdx

theorem `Family.rest_net`

Module Family (lean/phase6/Family.lean, lines 320–326) · file SHA-256 7a647f0a667d5ede… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

TWO-FRAME NETWORK FAMILY CERTIFICATE (W = 1, ≤ 42 layers, polynomial widths/gates).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.NetFam NimAudit.Family.restAdm NimAudit.Family.restLen NimAudit.Family.restN 1 42

Exact source text, lines 320–326

320/-- TWO-FRAME NETWORK FAMILY CERTIFICATE (W = 1, ≤ 42 layers, polynomial widths/gates). -/321theorem rest_net : NetFam restAdm restLen restN 1 42 :=322  binNet_cert (S := restS) restLen_pos (fun i _ => rest_bound i) (fun _ _ => by omega)323    (fun i _ => Nat.le_refl _)324    (polyE restLen_pos leafBN rest_leaves ((1 + vr + vB) * restSzE + 2 * (vB * vN)) _ (fun _ => rfl))325    (polyE restLen_pos leafBN rest_leaves ((2 * 20 + 1) * ((1 + vr + vB) * restSzE) + (1 + vr + vB)) _326      (fun _ => rfl))

Project declarations in the statement: Family.NetFam, Family.restAdm, Family.restLen, Family.restN

Project declarations used by the proof or definition body

Family.PE, Family.binNet_cert, Family.instAddPE, Family.instMulPE, Family.instOfNatPE, Family.leafBN, Family.polyE, Family.restAdm, Family.restLen, Family.restLen_pos, Family.restS, Family.restSz, Family.restSzE, Family.rest_bound, Family.rest_leaves, Family.vB, Family.vN, Family.vr, WholeGame.rIdx

theorem `Family.mh_ac0`

Module Family (lean/phase6/Family.lean, lines 418–420) · file SHA-256 7a647f0a667d5ede… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

OUTCOME-CONDITIONED READOUT: formula family certificate (depth ≤ 19, input B·N + B).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.AC0Fam NimAudit.Family.mhAdm NimAudit.Family.mhLen
  (fun i => NimAudit.ThresholdInst.bForms (NimAudit.Family.mhS i)) 19

Exact source text, lines 418–420

418/-- OUTCOME-CONDITIONED READOUT: formula family certificate (depth ≤ 19, input B·N + B). -/419theorem mh_ac0 : AC0Fam mhAdm mhLen (fun i => bForms (mhS i)) 19 :=420  bin_cert mhLen_pos (fun i _ => mh_bound i) (fun _ _ => Nat.le_refl _) (fun _ _ => Nat.le_refl _) mh_sizePoly

Project declarations in the statement: Family.AC0Fam, Family.mhAdm, Family.mhLen, Family.mhS, ThresholdInst.bForms

Project declarations used by the proof or definition body

Family.bin_cert, Family.mhAdm, Family.mhLen, Family.mhLen_pos, Family.mhS, Family.mhSz, Family.mh_bound, Family.mh_sizePoly, WholeGame.rIdx

theorem `Family.mh_net`

Module Family (lean/phase6/Family.lean, lines 424–428) · file SHA-256 7a647f0a667d5ede… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.NetFam NimAudit.Family.mhAdm NimAudit.Family.mhLen NimAudit.Family.mhN 1 40

Exact source text, lines 424–428

424theorem mh_net : NetFam mhAdm mhLen mhN 1 40 :=425  binNet_cert (S := mhS) mhLen_pos (fun i _ => mh_bound i) (fun _ _ => by omega) (fun _ _ => Nat.le_refl _)426    (polyE mhLen_pos leafBN mh_leaves ((1 + vr + vB) * mhSzE + (vB * vN + vB)) _ (fun _ => rfl))427    (polyE mhLen_pos leafBN mh_leaves ((2 * 19 + 1) * ((1 + vr + vB) * mhSzE) + (1 + vr + vB)) _428      (fun _ => rfl))

Project declarations in the statement: Family.NetFam, Family.mhAdm, Family.mhLen, Family.mhN

Project declarations used by the proof or definition body

Family.PE, Family.binNet_cert, Family.instAddPE, Family.instMulPE, Family.instOfNatPE, Family.leafBN, Family.mhAdm, Family.mhLen, Family.mhLen_pos, Family.mhS, Family.mhSz, Family.mhSzE, Family.mh_bound, Family.mh_leaves, Family.polyE, Family.vB, Family.vN, Family.vr, WholeGame.rIdx

theorem `Family.pol_ac0`

Module Family (lean/phase6/Family.lean, lines 371–374) · file SHA-256 7a647f0a667d5ede… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

ONE STRUCTURED POLICY STEP: formula family certificate (depth ≤ 17, input B·N).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.AC0Fam NimAudit.Family.polAdm NimAudit.Family.polLen
  (fun i => NimAudit.ThresholdInst.bForms (NimAudit.Family.polS i)) 17

Exact source text, lines 371–374

371/-- ONE STRUCTURED POLICY STEP: formula family certificate (depth ≤ 17, input B·N). -/372theorem pol_ac0 : AC0Fam polAdm polLen (fun i => bForms (polS i)) 17 :=373  bin_cert polLen_pos (fun i _ => pol_bound i) (fun _ _ => Nat.le_refl _) (fun _ _ => Nat.le_refl _)374    pol_sizePoly

Project declarations in the statement: Family.AC0Fam, Family.polAdm, Family.polLen, Family.polS, ThresholdInst.bForms

Project declarations used by the proof or definition body

Family.bin_cert, Family.polAdm, Family.polLen, Family.polLen_pos, Family.polS, Family.polSz, Family.pol_bound, Family.pol_sizePoly, WholeGame.rIdx

theorem `Family.pol_net`

Module Family (lean/phase6/Family.lean, lines 378–382) · file SHA-256 7a647f0a667d5ede… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.NetFam NimAudit.Family.polAdm NimAudit.Family.polLen NimAudit.Family.polN 1 36

Exact source text, lines 378–382

378theorem pol_net : NetFam polAdm polLen polN 1 36 :=379  binNet_cert (S := polS) polLen_pos (fun i _ => pol_bound i) (fun _ _ => by omega) (fun _ _ => Nat.le_refl _)380    (polyE polLen_pos leafBNj pol_leaves ((1 + vr + vB) * polSzE + vB * vN) _ (fun _ => rfl))381    (polyE polLen_pos leafBNj pol_leaves ((2 * 17 + 1) * ((1 + vr + vB) * polSzE) + (1 + vr + vB)) _382      (fun _ => rfl))

Project declarations in the statement: Family.NetFam, Family.polAdm, Family.polLen, Family.polN

Project declarations used by the proof or definition body

Family.PE, Family.binNet_cert, Family.instAddPE, Family.instMulPE, Family.instOfNatPE, Family.leafBNj, Family.polAdm, Family.polLen, Family.polLen_pos, Family.polS, Family.polSz, Family.polSzE, Family.pol_bound, Family.pol_leaves, Family.polyE, Family.vB, Family.vN, Family.vr, WholeGame.rIdx

theorem `Family.ctrl_ac0`

Module Family (lean/phase6/Family.lean, lines 475–479) · file SHA-256 7a647f0a667d5ede… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

RECURRENT UPDATE: formula family certificate (depth ≤ 8, input = state + token, total size polynomial in that width, hence in B + log N).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.AC0Fam NimAudit.Family.ctrlAdm NimAudit.Family.ctrlLen NimAudit.Family.ctrlF 8

Exact source text, lines 475–479

475/-- RECURRENT UPDATE: formula family certificate (depth ≤ 8, input = state + token,476    total size polynomial in that width, hence in B + log N). -/477theorem ctrl_ac0 : AC0Fam ctrlAdm ctrlLen ctrlF 8 := by478  refine ⟨ctrlLen_pos, fun i _ c hc => (ctrlForms_res _ _ c hc).1, fun i _ c hc => (ctrlForms_res _ _ c hc).2.2, ?_⟩479  exact polyIn_mono (fun i _ => ctrlForms_size _ _) (polyE ctrlLen_pos leafBr ctrl_leaves ctrlSzE _ (fun _ => rfl))

Project declarations in the statement: Family.AC0Fam, Family.ctrlAdm, Family.ctrlF, Family.ctrlLen

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, ControllerBits.cellSize, ControllerBits.stateWidth, Family.AC0Fam.mk, Family.ctrlAdm, Family.ctrlF, Family.ctrlLen, Family.ctrlLen_pos, Family.ctrlSzE, Family.ctrl_leaves, Family.leafBr, Family.polyE, Family.polyIn_mono, Family.tsize, ThresholdInst.ctrlForms_res, ThresholdInst.ctrlForms_size, ThresholdInst.inWidth, ThresholdInst.outCount, WholeGame.rIdx

theorem `Family.ctrl_net`

Module Family (lean/phase6/Family.lean, lines 483–502) · file SHA-256 7a647f0a667d5ede… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.NetFam NimAudit.Family.ctrlAdm NimAudit.Family.ctrlLen NimAudit.Family.ctrlN 1 18

Exact source text, lines 483–502

483theorem ctrl_net : NetFam ctrlAdm ctrlLen ctrlN 1 18 := by484  refine ⟨ctrlLen_pos, fun i _ => (ctrlNet_res _ _).1, fun i _ => (ctrlNet_res _ _).2.1,485    fun i _ => (ctrlNet_res _ _).2.2.1, ?_, ?_⟩486  · obtain ⟨c, k, h⟩ := polyE ctrlLen_pos leafBr ctrl_leaves (ctrlSzE + (6 + 6 * vB + 3 * vR))487      (fun i => (stateWidth i.1 (rIdx i.2) + outCount i.1 (rIdx i.2)) * (cellSize i.1 (rIdx i.2) + 16) +488        inWidth i.1 (rIdx i.2)) (fun _ => rfl)489    refine ⟨c, k, fun i hi => netBounded_mono (ctrlNet_res _ _).2.2.2.1 ?_⟩490    have h5 := (ctrlNet_res i.1 (rIdx i.2)).2.2.2.2.2491    have h6 := h i hi492    dsimp only at h6493    unfold ctrlLen at h6 ⊢; omega494  · refine polyIn_mono (fun i _ => ?_) (polyE ctrlLen_pos leafBr ctrl_leaves495      (17 * ctrlSzE + ((4 + 5 * vB + 3 * vR) + (4 + 3 * vB + vR)))496      (fun i => 17 * ((stateWidth i.1 (rIdx i.2) + outCount i.1 (rIdx i.2)) * (cellSize i.1 (rIdx i.2) + 16)) +497        (stateWidth i.1 (rIdx i.2) + outCount i.1 (rIdx i.2))) (fun _ => rfl))498    have h1 := (ctrlNet_res i.1 (rIdx i.2)).2.2.2.2.1499    have h3 := (ctrlNet_res i.1 (rIdx i.2)).2.2.2.2.2500    have := Nat.mul_le_mul_left 17 h3501    show gateCount (ctrlNet i.1 (rIdx i.2)) ≤ _502    omega

Project declarations in the statement: Family.NetFam, Family.ctrlAdm, Family.ctrlLen, Family.ctrlN

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.size, AC0.Layer, AC0.NetBounded, AC0.NetValid, ControllerBits.cellSize, ControllerBits.stateWidth, Family.NetFam.mk, Family.PE, Family.PolyIn, Family.ctrlAdm, Family.ctrlLen, Family.ctrlLen_pos, Family.ctrlN, Family.ctrlSzE, Family.ctrl_leaves, Family.instAddPE, Family.instMulPE, Family.instOfNatPE, Family.leafBr, Family.netBounded_mono, Family.polyE, Family.polyIn_mono, Family.vB, Family.vR, FiniteNet.Wired, ThresholdInst.ctrlForms, ThresholdInst.ctrlNet, ThresholdInst.ctrlNet_res, ThresholdInst.inWidth, ThresholdInst.outCount, ThresholdNet.gateCount, WholeGame.rIdx

theorem `Shootout.sh_ac0`

Module Shootout (lean/phase7/Shootout.lean, lines 1196–1201) · file SHA-256 1abd814426d345b9… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

AC0 FAMILY CERTIFICATE of the outer controller's update (either schedule): depth ≤ 34, input width IW = 2BN + B + r + 5, total size polynomial in IW (uniformly in B and N).

Statement as elaborated and printed by Lean 4.26.0

∀ (early : Bool),
  NimAudit.Family.AC0Fam NimAudit.Family.restAdm NimAudit.Shootout.shLen
    (NimAudit.Shootout.shF early) 34

Exact source text, lines 1196–1201

1196/-- AC0 FAMILY CERTIFICATE of the outer controller's update (either schedule): depth ≤ 34,1197    input width IW = 2BN + B + r + 5, total size polynomial in IW (uniformly in B and N). -/1198theorem sh_ac0 (early : Bool) : AC0Fam restAdm shLen (shF early) 34 := by1199  refine ⟨shLen_pos, fun i _ c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).1,1200    fun i _ c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).2.2, ?_⟩1201  exact polyIn_mono (fun i _ => shF_tsize early i) (polyE shLen_pos leafS sh_leaves shSizeE _ (fun _ => rfl))

Project declarations in the statement: Family.AC0Fam, Family.restAdm, Shootout.shF, Shootout.shLen

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, Family.AC0Fam.mk, Family.polyE, Family.polyIn_mono, Family.restAdm, Family.tsize, Shootout.Fz, Shootout.IW, Shootout.SW, Shootout.cForms_res, Shootout.leafS, Shootout.shF, Shootout.shF_tsize, Shootout.shLen, Shootout.shLen_pos, Shootout.shSizeE, Shootout.sh_leaves, WholeGame.rIdx

theorem `Shootout.sh_net`

Module Shootout (lean/phase7/Shootout.lean, lines 1203–1222) · file SHA-256 1abd814426d345b9… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

NETWORK FAMILY CERTIFICATE: W = 1 (weights and thresholds in {0,1}), ≤ 70 layers, polynomial widths, fan-ins and gate count; the network's outputs are the formulas.

Statement as elaborated and printed by Lean 4.26.0

∀ (early : Bool),
  NimAudit.Family.NetFam NimAudit.Family.restAdm NimAudit.Shootout.shLen
    (NimAudit.Shootout.shN early) 1 70

Exact source text, lines 1203–1222

1203/-- NETWORK FAMILY CERTIFICATE: W = 1 (weights and thresholds in {0,1}), ≤ 70 layers,1204    polynomial widths, fan-ins and gate count; the network's outputs are the formulas. -/1205theorem sh_net (early : Bool) : NetFam restAdm shLen (shN early) 1 70 := by1206  have spec := fun i => compileF_spec (shF early i) (shLen i) 341207    (fun c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).2.2) (fun c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).1)1208  have hT := polyE shLen_pos leafS sh_leaves shSizeE1209    (fun i => SW i.1 i.2 (rIdx i.1) * Fz i.1 i.2 (rIdx i.1)) (fun _ => rfl)1210  refine ⟨shLen_pos, fun i _ => (spec i).2.2.1, fun i _ => (spec i).2.2.2.1, fun i _ => (spec i).2.2.2.2.1, ?_, ?_⟩1211  · obtain ⟨c, k, h⟩ := polyIn_add shLen_pos hT (polyIn_leaf (fun i _ => Nat.le_refl (shLen i)))1212    refine ⟨c, k, fun i hi => netBounded_mono (spec i).2.2.2.2.2.1 ?_⟩1213    have := shF_tsize early i; have := h i hi; dsimp only at *; unfold tsize at *; omega1214  · have h2 := polyIn_add shLen_pos (polyIn_mul (polyIn_const _ _ (2 * 34 + 1)) hT)1215      (polyE shLen_pos leafS sh_leaves (vB * vN + 4 + vRB + vB) (fun i => SW i.1 i.2 (rIdx i.1)) (fun _ => rfl))1216    refine polyIn_mono (fun i _ => ?_) h21217    have g := (spec i).2.2.2.2.2.21218    have := Nat.mul_le_mul_left (2 * 34 + 1) (shF_tsize early i)1219    have hl : (shF early i).length = SW i.1 i.2 (rIdx i.1) := by unfold shF; rw [cForms_length]1220    unfold tsize at this; rw [hl] at g1221    show gateCount (cNet early i.1 i.2 (rIdx i.1)) ≤ _1222    exact Nat.le_trans g (by omega)

Project declarations in the statement: Family.NetFam, Family.restAdm, Shootout.shLen, Shootout.shN

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, AC0.Layer, AC0.NetBounded, AC0.NetValid, AC0.evalNet, Family.NetFam.mk, Family.PE, Family.PolyIn, Family.instAddPE, Family.instMulPE, Family.instOfNatPE, Family.netBounded_mono, Family.polyE, Family.polyIn_add, Family.polyIn_const, Family.polyIn_leaf, Family.polyIn_mono, Family.polyIn_mul, Family.restAdm, Family.tsize, Family.vB, Family.vN, FiniteNet.Wired, Shootout.Fz, Shootout.IW, Shootout.SW, Shootout.cForms, Shootout.cForms_length, Shootout.cForms_res, Shootout.cNet, Shootout.leafS, Shootout.shF, Shootout.shF_tsize, Shootout.shLen, Shootout.shLen_pos, Shootout.shN, Shootout.shSizeE, Shootout.sh_leaves, Shootout.vRB, ThresholdNet.compileF, ThresholdNet.compileF_spec, ThresholdNet.gateCount, WholeGame.rIdx

Definitions these statements use

inductive `Family.AC0Fam`

Module Family (lean/phase6/Family.lean, lines 126–134) · file SHA-256 7a647f0a667d5ede…

AC0 FAMILY CERTIFICATE (nonuniform, multi-output). For every admissible member: the input length is positive, every output formula has depth ≤ d and reads only the first len inputs, and the total size of the outputs is ≤ c·len^k with c, k independent of the member.

Statement as elaborated and printed by Lean 4.26.0

{ι : Type} → (ι → Prop) → (ι → ℕ) → (ι → List NimAudit.AC0.Circ) → ℕ → Prop

Exact source text, lines 126–134

126/-- AC0 FAMILY CERTIFICATE (nonuniform, multi-output).  For every admissible member:127    the input length is positive, every output formula has depth ≤ d and reads only128    the first len inputs, and the total size of the outputs is ≤ c·len^k with c, k129    independent of the member. -/130structure AC0Fam {ι : Type} (adm : ι → Prop) (len : ι → Nat) (outs : ι → List Circ) (d : Nat) : Prop where131  pos : ∀ i, adm i → 1 ≤ len i132  depth_le : ∀ i, adm i → ∀ c ∈ outs i, depth c ≤ d133  reads : ∀ i, adm i → ∀ c ∈ outs i, maxInput c ≤ len i134  size_poly : PolyIn adm len (fun i => tsize (outs i))

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, Family.PolyIn, Family.tsize

def `Family.restAdm`

Module Family (lean/phase6/Family.lean, lines 282–282) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → Prop

Exact source text, lines 282–282

282def restAdm : Nat × Nat → Prop := fun i => 1 ≤ i.1 ∧ 1 ≤ i.2

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.restLen`

Module Family (lean/phase6/Family.lean, lines 283–284) · file SHA-256 7a647f0a667d5ede…

Supplied input: the two frames, 2·B·N bits.

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → ℕ

Exact source text, lines 283–284

283/-- Supplied input: the two frames, 2·B·N bits. -/284def restLen : Nat × Nat → Nat := fun i => 2 * (i.1 * i.2)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.restS`

Module Family (lean/phase6/Family.lean, lines 285–285) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → NimAudit.BinReadout.BCirc

Exact source text, lines 285–285

285def restS (i : Nat × Nat) : BCirc := restBin i.1 i.2 (rIdx i.2)

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

PriorityEncoder.restBin, WholeGame.rIdx

def `ThresholdInst.bForms`

Module ThresholdInst (lean/phase5/ThresholdInst.lean, lines 317–318) · file SHA-256 c8c66599c8e24804…

Output order: wire 0 valid, wires 1..r index bits, wires r+1..r+B value bits.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → List NimAudit.AC0.Circ

Exact source text, lines 317–318

317/-- Output order: wire 0 valid, wires 1..r index bits, wires r+1..r+B value bits. -/318def bForms (S : BCirc) : List Circ := S.valid :: (S.idx ++ S.val)

Project declarations in the statement: AC0.Circ, BinReadout.BCirc

Project declarations used by the proof or definition body

AC0.Circ, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid

inductive `Family.NetFam`

Module Family (lean/phase6/Family.lean, lines 141–149) · file SHA-256 7a647f0a667d5ede…

NETWORK FAMILY CERTIFICATE: fixed grid W, at most L layers, valid gates, first layer reading only the len inputs, polynomial widths/fan-ins and polynomial gate count.

Statement as elaborated and printed by Lean 4.26.0

{ι : Type} → (ι → Prop) → (ι → ℕ) → (ι → List NimAudit.AC0.Layer) → ℕ → ℕ → Prop

Exact source text, lines 141–149

141/-- NETWORK FAMILY CERTIFICATE: fixed grid W, at most L layers, valid gates, first layer142    reading only the len inputs, polynomial widths/fan-ins and polynomial gate count. -/143structure NetFam {ι : Type} (adm : ι → Prop) (len : ι → Nat) (net : ι → List Layer) (W L : Nat) : Prop where144  pos : ∀ i, adm i → 1 ≤ len i145  valid : ∀ i, adm i → NetValid W (net i)146  wired : ∀ i, adm i → Wired (len i) (net i)147  layers : ∀ i, adm i → (net i).length ≤ L148  bounded : ∃ c k, ∀ i, adm i → NetBounded (c * len i ^ k) (net i)149  gates : PolyIn adm len (fun i => gateCount (net i))

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Layer, AC0.NetBounded, AC0.NetValid, Family.PolyIn, FiniteNet.Wired, ThresholdNet.gateCount

def `Family.restN`

Module Family (lean/phase6/Family.lean, lines 318–318) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 318–318

318def restN (i : Nat × Nat) : List Layer := restNet i.1 i.2 (rIdx i.2)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

ThresholdInst.restNet, WholeGame.rIdx

def `Family.mhAdm`

Module Family (lean/phase6/Family.lean, lines 390–391) · file SHA-256 7a647f0a667d5ede…

Readout members (board plus B outcome wires).

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → Prop

Exact source text, lines 390–391

390/-- Readout members (board plus B outcome wires). -/391def mhAdm : Nat × Nat → Prop := restAdm

Project declarations in the statement: none

Project declarations used by the proof or definition body

Family.restAdm

def `Family.mhLen`

Module Family (lean/phase6/Family.lean, lines 392–392) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → ℕ

Exact source text, lines 392–392

392def mhLen : Nat × Nat → Nat := fun i => i.1 * i.2 + i.1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.mhS`

Module Family (lean/phase6/Family.lean, lines 393–393) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → NimAudit.BinReadout.BCirc

Exact source text, lines 393–393

393def mhS (i : Nat × Nat) : BCirc := mhBin i.1 i.2 (rIdx i.2)

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

PriorityEncoder.mhBin, WholeGame.rIdx

def `Family.mhN`

Module Family (lean/phase6/Family.lean, lines 422–422) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 422–422

422def mhN (i : Nat × Nat) : List Layer := mhNet i.1 i.2 (rIdx i.2)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

ThresholdInst.mhNet, WholeGame.rIdx

def `Family.polAdm`

Module Family (lean/phase6/Family.lean, lines 344–345) · file SHA-256 7a647f0a667d5ede…

Policy members are indexed by (B, (N, j)).

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → Prop

Exact source text, lines 344–345

344/-- Policy members are indexed by (B, (N, j)). -/345def polAdm : Nat × (Nat × Nat) → Prop := fun i => 1 ≤ i.1 ∧ 1 ≤ i.2.1 ∧ i.2.2 < i.1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.polLen`

Module Family (lean/phase6/Family.lean, lines 346–346) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → ℕ

Exact source text, lines 346–346

346def polLen : Nat × (Nat × Nat) → Nat := fun i => i.1 * i.2.1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.polS`

Module Family (lean/phase6/Family.lean, lines 347–347) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → NimAudit.BinReadout.BCirc

Exact source text, lines 347–347

347def polS (i : Nat × (Nat × Nat)) : BCirc := polBin i.1 i.2.1 i.2.2 (rIdx i.2.1)

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

PriorityEncoder.polBin, WholeGame.rIdx

def `Family.polN`

Module Family (lean/phase6/Family.lean, lines 376–376) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 376–376

376def polN (i : Nat × (Nat × Nat)) : List Layer := polNet i.1 i.2.1 i.2.2 (rIdx i.2.1)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

ThresholdInst.polNet, WholeGame.rIdx

def `Family.ctrlAdm`

Module Family (lean/phase6/Family.lean, lines 445–445) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → Prop

Exact source text, lines 445–445

445def ctrlAdm : Nat × Nat → Prop := restAdm

Project declarations in the statement: none

Project declarations used by the proof or definition body

Family.restAdm

def `Family.ctrlF`

Module Family (lean/phase6/Family.lean, lines 448–448) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Circ

Exact source text, lines 448–448

448def ctrlF (i : Nat × Nat) : List Circ := ctrlForms i.1 (rIdx i.2)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

ThresholdInst.ctrlForms, WholeGame.rIdx

def `Family.ctrlLen`

Module Family (lean/phase6/Family.lean, lines 446–447) · file SHA-256 7a647f0a667d5ede…

Per-update input: state (4 + 5B + 3r bits) plus one token (2 + B bits), r = log₂N + 1.

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → ℕ

Exact source text, lines 446–447

446/-- Per-update input: state (4 + 5B + 3r bits) plus one token (2 + B bits), r = log₂N + 1. -/447def ctrlLen : Nat × Nat → Nat := fun i => inWidth i.1 (rIdx i.2)

Project declarations in the statement: none

Project declarations used by the proof or definition body

ThresholdInst.inWidth, WholeGame.rIdx

def `Family.ctrlN`

Module Family (lean/phase6/Family.lean, lines 481–481) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 481–481

481def ctrlN (i : Nat × Nat) : List Layer := ctrlNet i.1 (rIdx i.2)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

ThresholdInst.ctrlNet, WholeGame.rIdx

def `Shootout.shF`

Module Shootout (lean/phase7/Shootout.lean, lines 1162–1162) · file SHA-256 1abd814426d345b9…

Statement as elaborated and printed by Lean 4.26.0

Bool → ℕ × ℕ → List NimAudit.AC0.Circ

Exact source text, lines 1162–1162

1162def shF (early : Bool) (i : Nat × Nat) : List Circ := cForms early i.1 i.2 (rIdx i.1)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

Shootout.cForms, WholeGame.rIdx

def `Shootout.shLen`

Module Shootout (lean/phase7/Shootout.lean, lines 1160–1161) · file SHA-256 1abd814426d345b9…

Input width of one update of the (B, N) controller (registers, reset, board).

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → ℕ

Exact source text, lines 1160–1161

1160/-- Input width of one update of the (B, N) controller (registers, reset, board). -/1161def shLen (i : Nat × Nat) : Nat := IW i.1 i.2 (rIdx i.1)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Shootout.IW, WholeGame.rIdx

def `Shootout.shN`

Module Shootout (lean/phase7/Shootout.lean, lines 1163–1163) · file SHA-256 1abd814426d345b9…

Statement as elaborated and printed by Lean 4.26.0

Bool → ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 1163–1163

1163def shN (early : Bool) (i : Nat × Nat) : List Layer := cNet early i.1 i.2 (rIdx i.1)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

Shootout.cNet, WholeGame.rIdx

Full modules

Module	File	Lines	Imports
Family	`lean/phase6/Family.lean`	574	WholeGame
Shootout	`lean/phase7/Shootout.lean`	1491	Misc, BoardStore
ThresholdInst	`lean/phase5/ThresholdInst.lean`	475	ThresholdNet, PriorityEncoder

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).

Appendix C, tableCertified depth and layer bounds for one evaluation of each component

1 Paper text

2 Explain this

From Boolean formulas to threshold layers

Teaching example A hand-made circuit

Exact construction trace What the checked compiler builds

Truth table

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Family.rest_ac0

theorem Family.rest_net

theorem Family.mh_ac0

theorem Family.mh_net

theorem Family.pol_ac0

theorem Family.pol_net

theorem Family.ctrl_ac0

theorem Family.ctrl_net

theorem Shootout.sh_ac0

theorem Shootout.sh_net

Definitions these statements use

inductive Family.AC0Fam

def Family.restAdm

def Family.restLen

def Family.restS

def ThresholdInst.bForms

inductive Family.NetFam

def Family.restN

def Family.mhAdm

def Family.mhLen

def Family.mhS

def Family.mhN

def Family.polAdm

def Family.polLen

def Family.polS

def Family.polN

def Family.ctrlAdm

def Family.ctrlF

def Family.ctrlLen

def Family.ctrlN

def Shootout.shF

def Shootout.shLen

def Shootout.shN

Full modules

theorem `Family.rest_ac0`

theorem `Family.rest_net`

theorem `Family.mh_ac0`

theorem `Family.mh_net`

theorem `Family.pol_ac0`

theorem `Family.pol_net`

theorem `Family.ctrl_ac0`

theorem `Family.ctrl_net`

theorem `Shootout.sh_ac0`

theorem `Shootout.sh_net`

inductive `Family.AC0Fam`

def `Family.restAdm`

def `Family.restLen`

def `Family.restS`

def `ThresholdInst.bForms`

inductive `Family.NetFam`

def `Family.restN`

def `Family.mhAdm`

def `Family.mhLen`

def `Family.mhS`

def `Family.mhN`

def `Family.polAdm`

def `Family.polLen`

def `Family.polS`

def `Family.polN`

def `Family.ctrlAdm`

def `Family.ctrlF`

def `Family.ctrlLen`

def `Family.ctrlN`

def `Shootout.shF`

def `Shootout.shLen`

def `Shootout.shN`