Section 6.4, “Local vs. global parity in NIM”A nim-sum bit is a degree-N character; for a known changed heap a delta bit is a two-coordinate character

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

1 Paper text

Local vs. global parity in NIM. In our encoding, the $j$ th bit of the nim-sum is the parity of the $j$ th bits across all $N$ heaps, hence a degree- $N$ character. Conditional on a specified changed heap $i$ , the sign encoding of the $j$ th delta bit is the two-coordinate character $(-1)^{x_{i,j}+x'_{i,j}}$ . When the changed index is unknown, the delta bit is specified on pairs of boards differing in at most one heap. A shallow extension to all pairs is $d_j(P,P')=\bigvee_{i=1}^{N}(x_{i,j}\oplus x'_{i,j}).$ (6.2) On the promised domain this is the required delta bit. For $N\ge2$ , its sign encoding $(-1)^{d_j}$ is not a single character, even up to sign; for $N=1$ it is exactly a degree-two character. Thus local computability does not mean that the full unknown-index map has degree two. It follows from the explicit $\AC^0$ construction in Lemma 5.4.

Generated from paper_jmlr.tex, lines 974–981.

2 Explain this

Nim-sum bits are high-degree. Bit $j$ of the nim-sum is the parity of the $j$ -th bits of all $N$ heaps: a character of degree $N$ . As $N$ grows, it is exactly the kind of function AC⁰ correlates with negligibly.

Delta bits with a known heap are low-degree. If we know that heap $i$ changed, bit $j$ of the difference is $x_{i,j}\oplus x'_{i,j}$ : a character of degree $2$ , trivially local.

3 How this is formalised

RealFourier.nimBit_spectrum_real: the sign of nim-sum bit $j$ (on the $BN$ -bit board encoding) has coefficient $1$ at one mask with exactly $N$ ones and $0$ elsewhere; its exact degree is $N$ ; its tail is $1$ below $N$ and $0$ from $N$ on. Misc.nimsum_bit_character is the Boolean form.
RealFourier.delta_spectrum_real: on the $2B$ bits of the changed heap, the sign of delta bit $j$ is the character of a two-element mask.
Fourier.nimBit_corr_of_tail: if the named Fourier.TailPremise holds at some $k<N$ , every bounded formula reading the board has squared correlation at most $\eta$ with nim-sum bit $j$ . This is a conditional application; the premise is not instantiated.

Coverage record
Paper anchor	`c-nim-bit-character` (website anchor; the manuscript has no label here)
Displayed as	Section 6.4, “Local vs. global parity in NIM”
Claim	A nim-sum bit is a degree-N character; for a known changed heap a delta bit is a two-coordinate character
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 974–981; SHA-256 of the normalised block source `5228c8bfadd11fe2…`
Lean declarations	`NimAudit.RealFourier.nimBit_spectrum_real` (RealFourier, lines 183–187, file `e0e69edd199d…`) `NimAudit.RealFourier.delta_spectrum_real` (RealFourier, lines 189–192, file `e0e69edd199d…`) `NimAudit.Misc.nimsum_bit_character` (Misc, lines 677–685, file `07766c03566d…`) `NimAudit.Fourier.nimBit_corr_of_tail` (Fourier, lines 550–564, file `afffe6072d70…`)
Prose-to-formal notes	`Fourier.nimBit_corr_of_tail` applies the named `TailPremise`; that premise is not instantiated against a published theorem (see the open item).
Audited correspondence rows	`sec:spectral-view`
Explanations	`explain/c-nim-bit-character`, `formal/c-nim-bit-character`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `RealFourier.nimBit_spectrum_real`

Module RealFourier (lean/phase8/RealFourier.lean, lines 183–187) · file SHA-256 e0e69edd199d8650… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

∀ {B N j : ℕ},
  j < B →
    (∀ T ∈ NimAudit.Bridge.bitvecs (B * N),
        NimAudit.Fourier.coef (B * N) (NimAudit.Fourier.nimBitSign B N j) T =
          if T = NimAudit.Bridge.maskU B N (2 ^ j) then 1 else 0) ∧
      NimAudit.Bridge.ones (NimAudit.Bridge.maskU B N (2 ^ j)) = N ∧
        NimAudit.Fourier.ExactDeg (B * N) (NimAudit.Fourier.nimBitSign B N j) N ∧
          ∀ (k : ℕ),
            NimAudit.Fourier.tail (B * N) (NimAudit.Fourier.nimBitSign B N j) k =
              if k < N then 1 else 0

Exact source text, lines 183–187

183theorem nimBit_spectrum_real {B N j : ℕ} (hj : j < B) :184    (∀ T ∈ bitvecs (B * N), coef (B * N) (nimBitSign (R := ℝ) B N j) T = if T = maskU B N (2 ^ j) then 1 else 0) ∧185    ones (maskU B N (2 ^ j)) = N ∧ ExactDeg (B * N) (nimBitSign (R := ℝ) B N j) N ∧186    ∀ k, tail (B * N) (nimBitSign (R := ℝ) B N j) k = if k < N then 1 else 0 :=187  nimBit_spectrum hj

Project declarations in the statement: Bridge.bitvecs, Bridge.maskU, Bridge.ones, Fourier.ExactDeg, Fourier.coef, Fourier.nimBitSign, Fourier.tail

Project declarations used by the proof or definition body

Fourier.nimBit_spectrum

theorem `RealFourier.delta_spectrum_real`

Module RealFourier (lean/phase8/RealFourier.lean, lines 189–192) · file SHA-256 e0e69edd199d8650… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

∀ {B j : ℕ},
  j < B →
    (∀ w ∈ NimAudit.Bridge.bitvecs (B * 2),
        NimAudit.Fourier.deltaSign B j w =
          NimAudit.Fourier.chi (NimAudit.Bridge.maskU B 2 (2 ^ j)) w) ∧
      NimAudit.Bridge.ones (NimAudit.Bridge.maskU B 2 (2 ^ j)) = 2 ∧
        NimAudit.Fourier.ExactDeg (B * 2) (NimAudit.Fourier.deltaSign B j) 2

Exact source text, lines 189–192

189theorem delta_spectrum_real {B j : ℕ} (hj : j < B) :190    (∀ w ∈ bitvecs (B * 2), (deltaSign B j w : ℝ) = chi (maskU B 2 (2 ^ j)) w) ∧191    ones (maskU B 2 (2 ^ j)) = 2 ∧ ExactDeg (B * 2) (deltaSign (R := ℝ) B j) 2 :=192  delta_spectrum hj

Project declarations in the statement: Bridge.bitvecs, Bridge.maskU, Bridge.ones, Fourier.ExactDeg, Fourier.chi, Fourier.deltaSign

Project declarations used by the proof or definition body

Fourier.delta_spectrum

theorem `Misc.nimsum_bit_character`

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

NIM-SUM BITS ARE DEGREE-N CHARACTERS: bit j of nim(P) is the parity of the inputs on a mask with exactly N ones (one coordinate per heap).

Statement as elaborated and printed by Lean 4.26.0

∀ {B N j : ℕ},
  j < B →
    ∀ {x : List Bool},
      x ∈ NimAudit.Bridge.bitvecs (B * N) →
        (NimAudit.nimSum (NimAudit.Bridge.decodeBoard B N x)).testBit j =
            NimAudit.Bridge.pm (NimAudit.Bridge.maskU B N (2 ^ j)) x ∧
          NimAudit.Bridge.ones (NimAudit.Bridge.maskU B N (2 ^ j)) = N

Exact source text, lines 677–685

677/-- NIM-SUM BITS ARE DEGREE-N CHARACTERS: bit j of nim(P) is the parity of the inputs on678    a mask with exactly N ones (one coordinate per heap). -/679theorem nimsum_bit_character {B N j : Nat} (hj : j < B) {x : List Bool} (hx : x ∈ bitvecs (B * N)) :680    (nimSum (decodeBoard B N x)).testBit j = pm (maskU B N (2 ^ j)) x ∧ Bridge.ones (maskU B N (2 ^ j)) = N := by681  refine ⟨by rw [← chi_parity B N (2 ^ j) hx]; exact (dotB_pow _ B hj).symm, ?_⟩682  rw [ones_maskU, ones_toBitsBE_count]683  have : (List.range B).filter (fun k => (2 ^ j).testBit k) = (List.range B).filter (fun k => decide (j = k)) := by684    apply List.filter_congr; intro k _; rw [Nat.testBit_two_pow]685  rw [this, count_eq_one, if_pos hj, Nat.mul_one]

Project declarations in the statement: Bridge.bitvecs, Bridge.decodeBoard, Bridge.maskU, Bridge.ones, Bridge.pm, nimSum

Project declarations used by the proof or definition body

Bridge.bitvecs, Bridge.chi_parity, Bridge.decodeBoard, Bridge.maskU, Bridge.ones, Bridge.ones_maskU, Bridge.pm, Bridge.toBitsBE, Misc.count_eq_one, Misc.dotB_pow, Misc.ones_toBitsBE_count, Prob.dotB, nimSum

theorem `Fourier.nimBit_corr_of_tail`

Module Fourier (lean/phase8/Fourier.lean, lines 550–564) · file SHA-256 afffe6072d707e40… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

A paper-specific application of the named tail premise, with the actual support size: a formula of depth ≤ d and size ≤ M reading the B·N board bits has squared correlation at most η with nim-sum bit j (a character of degree N), provided the premise holds at some k < N.

Statement as elaborated and printed by Lean 4.26.0

∀ {R : Type} [inst : Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Grind.OrderedRing R] {B N j d M k : ℕ} {η : R},
  j < B →
    k < N →
      NimAudit.Fourier.TailPremise (B * N) d M k η →
        ∀ (C : NimAudit.AC0.Circ),
          C.depth ≤ d →
            C.size ≤ M →
              C.maxInput ≤ B * N →
                NimAudit.Fourier.ip (B * N)
                      (fun x =>
                        NimAudit.Noise.sg (NimAudit.AC0.Circ.eval (NimAudit.Bridge.vfun x) C))
                      (NimAudit.Fourier.nimBitSign B N j) ^
                    2 ≤
                  η

Exact source text, lines 550–564

550/-- A paper-specific application of the named tail premise, with the actual support size: a551    formula of depth ≤ d and size ≤ M reading the B·N board bits has squared correlation at552    most η with nim-sum bit j (a character of degree N), provided the premise holds at some553    k < N. -/554theorem nimBit_corr_of_tail {B N j d M k : Nat} {η : R} (hj : j < B) (hk : k < N)555    (hT : TailPremise (B * N) d M k η) (C : Circ) (hd : depth C ≤ d) (hs : size C ≤ M) (hm : maxInput C ≤ B * N) :556    ip (B * N) (fun x => sg (eval (vfun x) C)) (nimBitSign B N j) ^ 2 ≤ η := by557  have hc : ∀ x ∈ bitvecs (B * N), (nimBitSign B N j x : R) = chi (maskU B N (2 ^ j)) x :=558    fun x hx => nimBitSign_chi hj hx559  have e : ip (B * N) (fun x => sg (eval (vfun x) C)) (nimBitSign B N j) =560      coef (R := R) (B * N) (fun x => sg (eval (vfun x) C)) (maskU B N (2 ^ j)) := by561    unfold coef ip; apply congrArg (· * _); apply gs_congr; intro x hx; rw [hc x hx]562  rw [e]563  have hones := (Misc.nimsum_bit_character hj (x := maskU B N (2 ^ j)) (maskU_mem B N _)).2564  exact Std.le_trans (coef_sq_le_tail _ (maskU_mem B N _) (by rw [hones]; exact hk)) (hT C hd hs hm)

Project declarations in the statement: AC0.Circ, AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, Bridge.vfun, Fourier.TailPremise, Fourier.ip, Fourier.nimBitSign, Noise.sg

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, Bridge.bitvecs, Bridge.decodeBoard, Bridge.maskU, Bridge.ones, Bridge.pm, Bridge.vfun, Fourier.TailPremise, Fourier.chi, Fourier.coef, Fourier.coef_sq_le_tail, Fourier.ip, Fourier.maskU_mem, Fourier.nimBitSign, Fourier.nimBitSign_chi, Fourier.tail, Misc.nimsum_bit_character, Noise.gs, Noise.gs_congr, Noise.sg, nimSum

Definitions these statements use

def `Fourier.TailPremise`

Module Fourier (lean/phase8/Fourier.lean, lines 514–518) · file SHA-256 afffe6072d707e40…

NAMED EXTERNAL PREMISE (not proved here, not assumed by any other theorem): every formula of depth ≤ d and size ≤ M reading only inputs below n has degree-> k tail of its sign encoding at most η. Classical results of Linial–Mansour–Nisan and Tal give such η.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → [LE R] → ℕ → ℕ → ℕ → ℕ → R → Prop

Exact source text, lines 514–518

514/-- NAMED EXTERNAL PREMISE (not proved here, not assumed by any other theorem): every515    formula of depth ≤ d and size ≤ M reading only inputs below n has degree-> k tail of its516    sign encoding at most η.  Classical results of Linial–Mansour–Nisan and Tal give such η. -/517def TailPremise (n d M k : Nat) (η : R) : Prop :=518  ∀ C : Circ, depth C ≤ d → size C ≤ M → maxInput C ≤ n → tail n (fun x => sg (eval (vfun x) C)) k ≤ η

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, Bridge.vfun, Fourier.tail, Noise.sg

def `Bridge.bitvecs`

Module BitBridge (lean/phase3/BitBridge.lean, lines 27–29) · file SHA-256 000644dc271d27f9…

Statement as elaborated and printed by Lean 4.26.0

ℕ → List (List Bool)

Exact source text, lines 27–29

27def bitvecs : Nat → List (List Bool)28  | 0 => [[]]29  | n + 1 => (bitvecs n).map (false :: ·) ++ (bitvecs n).map (true :: ·)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Bridge.maskU`

Module BitBridge (lean/phase3/BitBridge.lean, lines 207–210) · file SHA-256 000644dc271d27f9…

Mask for the character chi_u on N heaps: N copies of u's B bits.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → List Bool

Exact source text, lines 207–210

207/-- Mask for the character chi_u on N heaps: N copies of u's B bits. -/208def maskU (B : Nat) : Nat → Nat → List Bool209  | 0, _ => []210  | N + 1, u => toBitsBE B u ++ maskU B N u

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.toBitsBE

def `Bridge.ones`

Module BitBridge (lean/phase3/BitBridge.lean, lines 275–276) · file SHA-256 000644dc271d27f9…

Number of ones in a bit list.

Statement as elaborated and printed by Lean 4.26.0

List Bool → ℕ

Exact source text, lines 275–276

275/-- Number of ones in a bit list. -/276def ones (l : List Bool) : Nat := (l.filter id).length

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Fourier.ExactDeg`

Module Fourier (lean/phase8/Fourier.lean, lines 390–392) · file SHA-256 afffe6072d707e40…

Exact Fourier degree d.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → ℕ → (List Bool → R) → ℕ → Prop

Exact source text, lines 390–392

390/-- Exact Fourier degree d. -/391def ExactDeg (n : Nat) (f : List Bool → R) (d : Nat) : Prop :=392  DegLe n f d ∧ ∃ T ∈ bitvecs n, ones T = d ∧ coef n f T ≠ 0

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.bitvecs, Bridge.ones, Fourier.DegLe, Fourier.coef

def `Fourier.coef`

Module Fourier (lean/phase8/Fourier.lean, lines 218–219) · file SHA-256 afffe6072d707e40…

Fourier coefficient f̂(S) = E_x[f(x) χ_S(x)].

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → ℕ → (List Bool → R) → List Bool → R

Exact source text, lines 218–219

218/-- Fourier coefficient f̂(S) = E_x[f(x) χ_S(x)]. -/219def coef (n : Nat) (f : List Bool → R) (S : List Bool) : R := ip n f (chi S)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Fourier.chi, Fourier.ip

def `Fourier.nimBitSign`

Module Fourier (lean/phase8/Fourier.lean, lines 522–523) · file SHA-256 afffe6072d707e40…

Sign encoding of bit j of the nim-sum of the decoded board.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → ℕ → ℕ → ℕ → List Bool → R

Exact source text, lines 522–523

522/-- Sign encoding of bit j of the nim-sum of the decoded board. -/523def nimBitSign (B N j : Nat) (x : List Bool) : R := sg ((nimSum (decodeBoard B N x)).testBit j)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.decodeBoard, Noise.sg, nimSum

def `Fourier.tail`

Module Fourier (lean/phase8/Fourier.lean, lines 380–382) · file SHA-256 afffe6072d707e40…

Degree-> k Fourier tail Tail_{>k}(f) = Σ_{|S| > k} f̂(S)².

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → ℕ → (List Bool → R) → ℕ → R

Exact source text, lines 380–382

380/-- Degree-> k Fourier tail Tail_{>k}(f) = Σ_{|S| > k} f̂(S)². -/381def tail (n : Nat) (f : List Bool → R) (k : Nat) : R :=382  gs (bitvecs n) (fun S => if k < ones S then coef n f S ^ 2 else 0)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.bitvecs, Bridge.ones, Fourier.coef, Noise.gs

def `Fourier.chi`

Module Fourier (lean/phase8/Fourier.lean, lines 198–199) · file SHA-256 afffe6072d707e40…

The Walsh–Hadamard character χ_S(x) = (−1)^{⟨S,x⟩}.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → List Bool → List Bool → R

Exact source text, lines 198–199

198/-- The Walsh–Hadamard character χ_S(x) = (−1)^{⟨S,x⟩}. -/199def chi (S x : List Bool) : R := sg (pm S x)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.pm, Noise.sg

def `Fourier.deltaSign`

Module Fourier (lean/phase8/Fourier.lean, lines 566–568) · file SHA-256 afffe6072d707e40…

Sign of bit j of a ⊕ b, as a function of the two B-bit blocks (u, v) of a = old and b = new value of one heap.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → ℕ → ℕ → List Bool → R

Exact source text, lines 566–568

566/-- Sign of bit j of a ⊕ b, as a function of the two B-bit blocks (u, v) of a = old and567    b = new value of one heap. -/568def deltaSign (B j : Nat) (w : List Bool) : R := sg ((toNatBE (w.take B) ^^^ toNatBE (w.drop B)).testBit j)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.toNatBE, Noise.sg

def `Bridge.decodeBoard`

Module BitBridge (lean/phase3/BitBridge.lean, lines 107–110) · file SHA-256 000644dc271d27f9…

Decode a heap-major big-endian bit vector into N heaps.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → List Bool → List ℕ

Exact source text, lines 107–110

107/-- Decode a heap-major big-endian bit vector into N heaps. -/108def decodeBoard (B : Nat) : Nat → List Bool → List Nat109  | 0, _ => []110  | N + 1, x => toNatBE (x.take B) :: decodeBoard B N (x.drop B)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.toNatBE

def `Bridge.pm`

Module BitBridge (lean/phase3/BitBridge.lean, lines 187–191) · file SHA-256 000644dc271d27f9…

Parity of the coordinates of x selected by the mask.

Statement as elaborated and printed by Lean 4.26.0

List Bool → List Bool → Bool

Exact source text, lines 187–191

187/-- Parity of the coordinates of x selected by the mask. -/188def pm : List Bool → List Bool → Bool189  | [], _ => false190  | _ :: _, [] => false191  | m :: ms, b :: bs => xor (m && b) (pm ms bs)

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 `AC0.Circ`

Module Circuit (lean/phase3/Circuit.lean, lines 35–40) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 35–40

35inductive Circ where36  | input (i : Nat)37  | const (b : Bool)38  | not (c : Circ)39  | and (cs : List Circ)40  | or (cs : List Circ)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `AC0.Circ.depth`

Module Circuit (lean/phase3/Circuit.lean, lines 61–66) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 61–66

61def depth : Circ → Nat62  | input _ => 063  | const _ => 064  | not c => depth c + 165  | and cs => listMax (cs.attach.map (fun ⟨c, _⟩ => depth c)) + 166  | or cs => listMax (cs.attach.map (fun ⟨c, _⟩ => depth c)) + 1

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.listMax, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `AC0.Circ.eval`

Module Circuit (lean/phase3/Circuit.lean, lines 44–49) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

(ℕ → Bool) → NimAudit.AC0.Circ → Bool

Exact source text, lines 44–49

44def eval (x : Nat → Bool) : Circ → Bool45  | input i => x i46  | const b => b47  | not c => !(eval x c)48  | and cs => cs.attach.all (fun ⟨c, _⟩ => eval x c)49  | or cs => cs.attach.any (fun ⟨c, _⟩ => eval x c)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `AC0.Circ.maxInput`

Module Circuit (lean/phase3/Circuit.lean, lines 68–74) · file SHA-256 af97cc0eec7d8464…

One more than the largest input index used (0 if none).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 68–74

68/-- One more than the largest input index used (0 if none). -/69def maxInput : Circ → Nat70  | input i => i + 171  | const _ => 072  | not c => maxInput c73  | and cs => listMax (cs.attach.map (fun ⟨c, _⟩ => maxInput c))74  | or cs => listMax (cs.attach.map (fun ⟨c, _⟩ => maxInput c))

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.listMax, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `AC0.Circ.size`

Module Circuit (lean/phase3/Circuit.lean, lines 51–56) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 51–56

51def size : Circ → Nat52  | input _ => 153  | const _ => 154  | not c => size c + 155  | and cs => (cs.attach.map (fun ⟨c, _⟩ => size c)).sum + 156  | or cs => (cs.attach.map (fun ⟨c, _⟩ => size c)).sum + 1

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `Bridge.vfun`

Module BitBridge (lean/phase3/BitBridge.lean, lines 407–408) · file SHA-256 000644dc271d27f9…

Bit vector as an input assignment.

Statement as elaborated and printed by Lean 4.26.0

List Bool → ℕ → Bool

Exact source text, lines 407–408

407/-- Bit vector as an input assignment. -/408def vfun (x : List Bool) : Nat → Bool := fun j => x.getD j false

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Fourier.ip`

Module Fourier (lean/phase8/Fourier.lean, lines 215–216) · file SHA-256 afffe6072d707e40…

Normalised inner product under the uniform distribution on {0,1}^n.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → ℕ → (List Bool → R) → (List Bool → R) → R

Exact source text, lines 215–216

215/-- Normalised inner product under the uniform distribution on {0,1}^n. -/216def ip (n : Nat) (f g : List Bool → R) : R := gs (bitvecs n) (fun x => f x * g x) * ((2 : R) ^ n)⁻¹

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.bitvecs, Noise.gs

def `Noise.sg`

Module NoiseModel (lean/phase7/NoiseModel.lean, lines 222–223) · file SHA-256 bde0a1ff202682bd…

±1 encoding of a bit.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → Bool → R

Exact source text, lines 222–223

222/-- ±1 encoding of a bit. -/223def sg (b : Bool) : R := if b then -1 else 1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

Full modules

Module	File	Lines	Imports
BitBridge	`lean/phase3/BitBridge.lean`	560	Circuit
Circuit	`lean/phase3/Circuit.lean`	1151	NimProbability
Fourier	`lean/phase8/Fourier.lean`	1379	NoiseModel
Misc	`lean/phase6/Misc.lean`	912	Bypass
NimCore	`lean/NimCore.lean`	139	`Std`
NoiseModel	`lean/phase7/NoiseModel.lean`	1008	Misc
RealFourier	`lean/phase8/RealFourier.lean`	275	`Mathlib.Data.Real.Archimedean`, `Mathlib.Data.Fintype.BigOperators`, `Mathlib.Algebra.BigOperators.Fin`, `Mathlib.Tactic.Linarith`, `Mathlib.Tactic.Positivity`, `Mathlib.Tactic.FieldSimp`, `Mathlib.Tactic.NormNum`, `Mathlib.Tactic.Ring`, Fourier, RealNoise

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

Section 6.4, “Local vs. global parity in NIM”A nim-sum bit is a degree-N character; for a known changed heap a delta bit is a two-coordinate character

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem RealFourier.nimBit_spectrum_real

theorem RealFourier.delta_spectrum_real

theorem Misc.nimsum_bit_character

theorem Fourier.nimBit_corr_of_tail

Definitions these statements use

def Fourier.TailPremise

def Bridge.bitvecs

def Bridge.maskU

def Bridge.ones

def Fourier.ExactDeg

def Fourier.coef

def Fourier.nimBitSign

def Fourier.tail

def Fourier.chi

def Fourier.deltaSign

def Bridge.decodeBoard

def Bridge.pm

def nimSum

inductive AC0.Circ

def AC0.Circ.depth

def AC0.Circ.eval

def AC0.Circ.maxInput

def AC0.Circ.size

def Bridge.vfun

def Fourier.ip

def Noise.sg

Full modules

theorem `RealFourier.nimBit_spectrum_real`

theorem `RealFourier.delta_spectrum_real`

theorem `Misc.nimsum_bit_character`

theorem `Fourier.nimBit_corr_of_tail`

def `Fourier.TailPremise`

def `Bridge.bitvecs`

def `Bridge.maskU`

def `Bridge.ones`

def `Fourier.ExactDeg`

def `Fourier.coef`

def `Fourier.nimBitSign`

def `Fourier.tail`

def `Fourier.chi`

def `Fourier.deltaSign`

def `Bridge.decodeBoard`

def `Bridge.pm`

def `nimSum`

inductive `AC0.Circ`

def `AC0.Circ.depth`

def `AC0.Circ.eval`

def `AC0.Circ.maxInput`

def `AC0.Circ.size`

def `Bridge.vfun`

def `Fourier.ip`

def `Noise.sg`