Appendix CShared shallow operations: candidate tests, binary index, recurrent update, threshold realisation

67/-- PRIORITY-ENCODER CORRECTNESS, for every input assignment: the binary output decodes68    to exactly the selection readout (first true flag, value bits), and to `none` when69    the readout is invalid or no flag is true. -/70theorem encode_correct (R : RCirc) (N r : Nat) (hlen : R.sel.length = N) (hr : N ≤ 2 ^ r)71    (z : Nat → Bool) : binSem (encode R N r) N z = selReadout R z := by72  unfold binSem selReadout encode73  simp only74  by_cases hv : eval z R.valid = true75  · cases hft : firstTrue (R.sel.map (eval z)) with76    | none =>77      have hany : (R.sel.map (eval z)).any id = false := by78        have := firstTrue_isSome (R.sel.map (eval z)); rw [hft] at this; simpa using this.symm79      have hor : eval z (or ((List.range N).map (getC R.sel))) = false := by80        rw [eval_or, List.any_map]81        have e : ((List.range N).any (eval z ∘ getC R.sel)) = (R.sel.map (eval z)).any id := by82          rw [← flags_eq R.sel N hlen z, List.any_map]; rfl83        rw [e, hany]84      simp [hv, hor]85    | some i =>86      have hiN : i < N := by have := firstTrue_lt hft; simpa [hlen] using this87      have hflag : (R.sel.map (eval z)).getD i false = true := ((firstTrue_some_iff _ i).1 hft).2.188      have hor : eval z (or ((List.range N).map (getC R.sel))) = true := by89        rw [eval_or, List.any_map]90        apply List.any_eq_true.mpr91        exact ⟨i, List.mem_range.mpr hiN, by simp only [Function.comp_apply, eval_getC]; exact hflag⟩92      have hidx : toNatBE (((List.range r).map (idxBit R.sel N r)).map (eval z)) = i := by93        rw [List.map_map]94        apply toNatBE_of_bits (Nat.lt_of_lt_of_le hiN hr)95        intro q _96        simp only [Function.comp_apply]97        apply Bool.eq_iff_iff.mpr98        simp only [idxBit, eval_or, List.any_map, List.any_eq_true, List.mem_filter, List.mem_range,99          Function.comp_apply]100        constructor101        · rintro ⟨i', ⟨hi', hb⟩, he⟩102          rw [firstF_eval R.sel hlen z hi', hft, decide_eq_true_iff] at he103          cases he; exact hb104        · intro hb105          exact ⟨i, ⟨hiN, hb⟩, by rw [firstF_eval R.sel hlen z hiN, hft]; simp⟩106      simp only [eval_and, List.all_cons, List.all_nil, hv, hor, Bool.and_true, if_true, hidx, hiN]107  · simp [hv]

698/-- THE COMPILER THEOREM (all properties of the one network `compileF cs`). -/699theorem compileF_spec (cs : List Circ) (n D : Nat) (hn : ∀ c ∈ cs, maxInput c ≤ n)700    (hD : ∀ c ∈ cs, depth c ≤ D) :701    (∀ x : Nat → Bool, ∀ k (hk : k < cs.length), evalNet (compileF cs) x k = eval x cs[k]) ∧702    (∀ x : Nat → Bool, ∀ k, cs.length ≤ k → evalNet (compileF cs) x k = false) ∧703    NetValid 1 (compileF cs) ∧ Wired n (compileF cs) ∧704    (compileF cs).length ≤ 2 * D + 2 ∧705    NetBounded ((cs.map size).sum + n) (compileF cs) ∧706    gateCount (compileF cs) ≤ (2 * D + 1) * (cs.map size).sum + cs.length := by707  have hd : dmax cs ≤ D := listMax_le (fun a ha => by obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact hD c hc)708  refine ⟨fun x k hk => compileF_eval cs x hk, fun x k hk => compileF_eval_out cs x hk, compileF_valid cs,709    compileF_wired cs n hn, by rw [compileF_length]; omega, compileF_bounded cs n hn, ?_⟩710  rw [compileF_gates]711  have : (2 * dmax cs + 1) * (cs.map size).sum ≤ (2 * D + 1) * (cs.map size).sum :=712    Nat.mul_le_mul_right _ (by omega)713  omega

715/-- FIXED GRID: every gate of a compiled network fires in the paper's rational form with716    denominator D = 1 exactly when it fires in integer form (weights in {0,1}, threshold717    in {0,1}). -/718theorem compileF_fixed_grid (cs : List Circ) :719    ∀ l ∈ compileF cs, ∀ g ∈ l, Gate.Valid 1 g ∧ ∀ z, (ratFires g 1 z ↔ g.eval z = true) :=720  fun l hl g hg => ⟨compileF_valid cs l hl g hg, fun z => gate_rat_iff g (by decide) z⟩

753/-- BOARD-STORAGE NETWORK CERTIFICATE (W = 1, ≤ 34 layers). -/754theorem bs_net : NetFam restAdm bsLen bsNet 1 34 := by755  have spec := fun i => compileF_spec (bsAll i) (bsLen i) 16756    (fun c hc => by757      rcases List.mem_append.mp hc with h | h758      · exact (bsForms_res _ _ _ c h).2.2759      · exact (bsOuts_res (rIdx_width i.2) c h).2.2)760    (fun c hc => by761      rcases List.mem_append.mp hc with h | h762      · have := (bsForms_res _ _ _ c h).1; omega763      · exact (bsOuts_res (rIdx_width i.2) c h).1)764  have hT := polyE bsLen_pos leafBN bs_leaves bsSizeE _ (fun i => (bsSizeE_eval i).symm)765  refine ⟨bsLen_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, ?_, ?_⟩766  · obtain ⟨c, k, h⟩ := polyIn_add bsLen_pos hT (polyIn_leaf (fun i _ => Nat.le_refl (bsLen i)))767    refine ⟨c, k, fun i hi => netBounded_mono (spec i).2.2.2.2.2.1 ?_⟩768    have := bsAll_tsize i; have := h i hi; dsimp only at *; unfold tsize at *; omega769  · refine polyIn_mono (fun i _ => ?_) (polyIn_mul (polyIn_const _ _ 34) hT)770    have g := (spec i).2.2.2.2.2.2771    have h1 := bsAll_tsize i772    have h2 := length_le_tsize (bsAll i)773    unfold tsize at h1 h2774    show gateCount (compileF (bsAll i)) ≤ 34 * _775    omega