Definition 5.7The restricted measurement interface: root and one-heap queries to one fixed structured head, bounded readout

Checked definition or construction Lean contains the definition or construction, with checked properties.

1 Paper text

Definition 5.7 (Restricted rollout measurements and readout) Fix a root position $P$ . An admissible query starts at $P$ or a position obtained by changing one heap of $P$ ; the changed index and old/new values are known to the readout. A legal one-move successor is an admissible query. Arbitrary transformations of the whole root are excluded. For the single-channel lower bound, one fixes a policy $\pi_j$ from Proposition 5.9, independently of $P$ . Writing $\beta=\mathrm{RO}_{\pi_j}(P)$ , the agent’s final move must have the form $F_N(P,\beta)$ , where $F_N$ is a polynomial-size, constant-depth Boolean circuit family. Any value head, query corrections or other processing must be included in this readout bound. The number of queries alone does not impose that bound. A multi-channel construction may query distinct members of the same structured policy family and apply a polynomial-size, constant-depth readout to $P$ and their outcome bits. A policy head means a rollout policy, not simply a parallel output neuron. We count simulated game moves separately from the circuit work per move.

Generated from paper_jmlr.tex, lines 639–644.

2 Explain this

This definition fixes exactly what the single-channel lower bound allows.

Queries. Start a rollout at the root board $P$ , or at a board obtained by changing one heap of $P$ (for example a candidate successor). Rollouts from arbitrary transformed boards are not allowed.
One channel. The policy is one fixed member $\pi_j$ of the structured family, chosen independently of $P$ .
Bounded readout. The final move must be computed by a polynomial-size, constant-depth circuit from $P$ and the observed bit $\beta$ . Any value head, correction of queries or other processing counts towards that readout.

The multi-channel construction may query several members of the family and then apply such a readout. A "policy head" means a rollout policy, not a parallel output neuron.

3 How this is formalised

The interface appears in Lean through its consequences rather than as a single definition.

One-heap queries: Prob.single_policy_affine and Misc.single_policy_correction show that a rollout from a board with one heap changed from $h$ to $h'$ returns the root outcome XOR a correction bit computable from $h\oplus h'$ , so such queries add no new unknown bit.
Why arbitrary starts are excluded: Misc.bitBoard_query (next record).
The readout bound: BinReadout.BBound specifies binary readout formulas of depth at most $d$ and size at most $s$ ; the conditional theorem quantifies over all such readouts. The correlation premise for their indicators is Prob.CorrHyp.

Coverage record
Paper anchor	`def:agent-types` (manuscript label)
Displayed as	Definition 5.7
Claim	The restricted measurement interface: root and one-heap queries to one fixed structured head, bounded readout
Coverage category	Checked definition or construction
Statement source	paper_jmlr.tex lines 639–644; SHA-256 of the normalised block source `8064cbf4f0ed779a…`
Lean declarations	`NimAudit.Prob.single_policy_affine` (NimProbability, lines 925–931, file `1d5d7977a43e…`) `NimAudit.Misc.single_policy_correction` (Misc, lines 718–720, file `07766c03566d…`) `NimAudit.Misc.bitBoard_query` (Misc, lines 843–847, file `07766c03566d…`) `NimAudit.BinReadout.BBound` (BinaryReadout, lines 131–144, file `17ef1a62ba9e…`)
Prose-to-formal notes	In the conditional bound the readout is any family of bounded-depth, polynomial-size binary circuits receiving the board and the observed bit. Query corrections must be computed inside that readout.
Audited correspondence rows	`def:agent-types`
Explanations	`explain/def:agent-types`, `formal/def:agent-types`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Prob.single_policy_affine`

Module NimProbability (lean/phase2/NimProbability.lean, lines 925–931) · file SHA-256 1d5d7977a43e854d… Axioms reported by the fresh build: propext, Quot.sound

SINGLE-POLICY INFORMATION BOUND (paper Prop. single-policy-bound): if P' differs from P in one heap h -> h', then RO_{pi_j}(P') = RO_{pi_j}(P) XOR <w_j, h XOR h'>, a correction bit computable from the known heap values.

Statement as elaborated and printed by Lean 4.26.0

∀ {B j : ℕ},
  j < B →
    ∀ (pre post : List ℕ) (h h' : ℕ),
      NimAudit.Game.rolloutWinner j (pre ++ h' :: post) =
        (NimAudit.Game.rolloutWinner j (pre ++ h :: post) ^^
          NimAudit.Prob.dotB B (NimAudit.Prob.headVec j) (h ^^^ h'))

Exact source text, lines 925–931

925/-- SINGLE-POLICY INFORMATION BOUND (paper Prop. single-policy-bound): if P' differs926    from P in one heap h -> h', then RO_{pi_j}(P') = RO_{pi_j}(P) XOR <w_j, h XOR h'>,927    a correction bit computable from the known heap values. -/928theorem single_policy_affine {B j : Nat} (hj : j < B) (pre post : List Nat) (h h' : Nat) :929    rolloutWinner j (pre ++ h' :: post) =930      xor (rolloutWinner j (pre ++ h :: post)) (dotB B (headVec j) (h ^^^ h')) := by931  rw [rollout_outcome_linear hj, rollout_outcome_linear hj, nimSum_move, dotB_xor_right]

Project declarations in the statement: Game.rolloutWinner, Prob.dotB, Prob.headVec

Project declarations used by the proof or definition body

Game.nimSum_move, Game.rolloutWinner, Prob.dotB, Prob.dotB_xor_right, Prob.headVec, Prob.rollout_outcome_linear, nimSum

theorem `Misc.single_policy_correction`

Module Misc (lean/phase6/Misc.lean, lines 718–720) · file SHA-256 07766c03566dbfca… Axioms reported by the fresh build: propext, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

∀ (j : ℕ) (pre post : List ℕ) (h h' : ℕ),
  NimAudit.Game.rolloutWinner j (pre ++ h' :: post) =
    (NimAudit.Game.rolloutWinner j (pre ++ h :: post) ^^ NimAudit.channel j (h ^^^ h'))

Exact source text, lines 718–720

718theorem single_policy_correction (j : Nat) (pre post : List Nat) (h h' : Nat) :719    rolloutWinner j (pre ++ h' :: post) = xor (rolloutWinner j (pre ++ h :: post)) (channel j (h ^^^ h')) := by720  rw [rolloutWinner_channel, rolloutWinner_channel, one_heap_update pre post h h', Nat.xor_assoc, channel_xor]

Project declarations in the statement: Game.rolloutWinner, channel

Project declarations used by the proof or definition body

Game.rolloutWinner, Game.rolloutWinner_channel, channel, channel_xor, nimSum, one_heap_update

theorem `Misc.bitBoard_query`

Module Misc (lean/phase6/Misc.lean, lines 843–847) · file SHA-256 07766c03566dbfca… Axioms reported by the fresh build: propext, Quot.sound

WHY ARBITRARY START POSITIONS ARE EXCLUDED (Definition def:agent-types): a single rollout of π₀ on the board whose heaps are the k-th bits of P returns σ_k(P).

Statement as elaborated and printed by Lean 4.26.0

∀ (k : ℕ) (P : List ℕ),
  NimAudit.Game.rolloutWinner 0 (List.map (fun h => if h.testBit k = true then 1 else 0) P) =
    (NimAudit.nimSum P).testBit k

Exact source text, lines 843–847

843/-- WHY ARBITRARY START POSITIONS ARE EXCLUDED (Definition def:agent-types): a single844    rollout of π₀ on the board whose heaps are the k-th bits of P returns σ_k(P). -/845theorem bitBoard_query (k : Nat) (P : List Nat) :846    rolloutWinner 0 (P.map (fun h => if h.testBit k then 1 else 0)) = (nimSum P).testBit k := by847  rw [rolloutWinner_channel]; simp only [channel, if_true]; exact nimSum_bitBoard k P

Project declarations in the statement: Game.rolloutWinner, nimSum

Project declarations used by the proof or definition body

Game.rolloutWinner, Game.rolloutWinner_channel, Misc.nimSum_bitBoard, channel, nimSum

inductive `BinReadout.BBound`

Module BinaryReadout (lean/phase4/BinaryReadout.lean, lines 131–144) · file SHA-256 17ef1a62ba9edafb…

Resource bounds for binary readout formulas.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → ℕ → ℕ → ℕ → ℕ → ℕ → Prop

Exact source text, lines 131–144

131/-- Resource bounds for binary readout formulas. -/132structure BBound (R : BCirc) (N B r d s : Nat) : Prop where133  idx_len : R.idx.length = r134  val_len : R.val.length = B135  width : N ≤ 2 ^ r136  depth_valid : depth R.valid ≤ d137  depth_idx : ∀ c ∈ R.idx, depth c ≤ d138  depth_val : ∀ c ∈ R.val, depth c ≤ d139  size_valid : size R.valid ≤ s140  size_idx : ∀ c ∈ R.idx, size c ≤ s141  size_val : ∀ c ∈ R.val, size c ≤ s142  max_valid : maxInput R.valid ≤ B * N143  max_idx : ∀ c ∈ R.idx, maxInput c ≤ B * N144  max_val : ∀ c ∈ R.val, maxInput c ≤ B * N

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid

Definitions these statements use

def `Prob.CorrHyp`

Module NimProbability (lean/phase2/NimProbability.lean, lines 541–546) · file SHA-256 1d5d7977a43e854d…

THE IMPORTED PARITY-CORRELATION PREMISE, as a predicate used only as a theorem hypothesis: |E[H_{b,a} chi_u]| ≤ η for every b, every a < q and every nonzero u < q. (Not an axiom; not proved here.)

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Prob.Readout → ℚ → Prop

Exact source text, lines 541–546

541/-- THE IMPORTED PARITY-CORRELATION PREMISE, as a predicate used only as a theorem542    hypothesis: |E[H_{b,a} chi_u]| ≤ η for every b, every a < q and every nonzero543    u < q.  (Not an axiom; not proved here.) -/544def CorrHyp (B N : Nat) (F : Readout) (η : Rat) : Prop :=545  ∀ (b : Bool) (a u : Nat), a < 2 ^ B → 0 < u → u < 2 ^ B →546    -η ≤ corr B N F b a u ∧ corr B N F b a u ≤ η

Project declarations in the statement: Prob.Readout

Project declarations used by the proof or definition body

Prob.Readout, Prob.corr

def `Game.rolloutWinner`

Module NimGame (lean/phase2/NimGame.lean, lines 142–152) · file SHA-256 23df6bb87ecfd344…

Rollout outcome RO_{pi_j}(P) as a game: both players follow pi_j; the result is `true` iff the player to move at P (the first player) wins under normal play. At a terminal start it is `false`.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Bool

Exact source text, lines 142–152

142/-- Rollout outcome RO_{pi_j}(P) as a game: both players follow pi_j; the result is143    `true` iff the player to move at P (the first player) wins under normal play.144    At a terminal start it is `false`. -/145def rolloutWinner (j : Nat) (p : List Nat) : Bool :=146  match h : policyStep j p with147  | none => false148  | some q => !rolloutWinner j q149termination_by rolloutCount j p150decreasing_by151  have := policyMove_count (policyStep_some h)152  omega

Project declarations in the statement: none

Project declarations used by the proof or definition body

Rollout.policyMove_count, Rollout.policyStep, Rollout.policyStep_some, rolloutCount

def `Prob.dotB`

Module NimProbability (lean/phase2/NimProbability.lean, lines 259–262) · file SHA-256 1d5d7977a43e854d…

The F_2 inner product of the first B bits of u and v.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → Bool

Exact source text, lines 259–262

259/-- The F_2 inner product of the first B bits of u and v. -/260def dotB : Nat → Nat → Nat → Bool261  | 0, _, _ => false262  | B + 1, u, v => xor (dotB B u v) (u.testBit B && v.testBit B)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Prob.headVec`

Module NimProbability (lean/phase2/NimProbability.lean, lines 875–876) · file SHA-256 1d5d7977a43e854d…

The vector w_j with RO_{pi_j}(P) = <w_j, sigma(P)>: w_0 = 1, w_j = 2^j XOR 1.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ

Exact source text, lines 875–876

875/-- The vector w_j with RO_{pi_j}(P) = <w_j, sigma(P)>: w_0 = 1, w_j = 2^j XOR 1. -/876def headVec (j : Nat) : Nat := if j = 0 then 1 else 2 ^ j ^^^ 1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `channel`

Module NimCore (lean/NimCore.lean, lines 77–78) · file SHA-256 b07db6c505210d5a…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → Bool

Exact source text, lines 77–78

77def channel (j sigma : Nat) : Bool :=78  if j = 0 then sigma.testBit 0 else xor (sigma.testBit j) (sigma.testBit 0)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `nimSum`

Module NimCore (lean/NimCore.lean, lines 7–9) · file SHA-256 b07db6c505210d5a…

Statement as elaborated and printed by Lean 4.26.0

List ℕ → ℕ

Exact source text, lines 7–9

7def nimSum : List Nat → Nat8  | [] => 09  | h :: t => h ^^^ nimSum t

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `BinReadout.BCirc`

Module BinaryReadout (lean/phase4/BinaryReadout.lean, lines 24–28) · file SHA-256 17ef1a62ba9edafb…

Binary readout formulas for one observed bit.

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 24–28

24/-- Binary readout formulas for one observed bit. -/25structure BCirc where26  valid : Circ27  idx : List Circ28  val : List Circ

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Circ

Full modules

Module	File	Lines	Imports
BinaryReadout	`lean/phase4/BinaryReadout.lean`	333	FiniteNet, NimCorrBridge
Misc	`lean/phase6/Misc.lean`	912	Bypass
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
NimProbability	`lean/phase2/NimProbability.lean`	1074	NimGame

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

Definition 5.7The restricted measurement interface: root and one-heap queries to one fixed structured head, bounded readout

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Prob.single_policy_affine

theorem Misc.single_policy_correction

theorem Misc.bitBoard_query

inductive BinReadout.BBound

Definitions these statements use

def Prob.CorrHyp

def Game.rolloutWinner

def Prob.dotB

def Prob.headVec

def channel

def nimSum

inductive BinReadout.BCirc

Full modules

theorem `Prob.single_policy_affine`

theorem `Misc.single_policy_correction`

theorem `Misc.bitBoard_query`

inductive `BinReadout.BBound`

def `Prob.CorrHyp`

def `Game.rolloutWinner`

def `Prob.dotB`

def `Prob.headVec`

def `channel`

def `nimSum`

inductive `BinReadout.BCirc`