Proposition 11 for the bit network (m = 10⁶, W = W_b, τ = 1 − 2^{−50})

Proposition 11 for the bit network (m = 10⁶, W = W_b, τ = 1 − 2^{−50}).

The following holds (Lean statement, in the scope of module Solutions.NetProp7Num):

theorem NetProp7.prop7_prop11 :
    ∃ q₀ : ℕ, ∀ q, q.Prime → q₀ < q →
      (∀ K k, k ≤ K → ∀ (P L : ℕ) (A B Cs : Shape) (xs : List (ZMod 2)),
        Fintype.card (NetScalar.Wr NetProp7.ind₀) ^ k ∣ L →
        xs.length = vol (P :: L :: hdShape A B Cs ((100 ^ 3) ^ k) q) →
        AModel.prog ((bitQC NetProp7.ind₀).toCircuit (q ^ (100 ^ 3) ^ K)) q k P L A B Cs xs =
          pull (P :: L :: hdShape A B Cs ((100 ^ 3) ^ k) q)
            (P :: L :: hdShape A B Cs ((100 ^ 3) ^ k) q)
            (blockSwap (A.length + 2) (A.length + B.length + (100 ^ 3) ^ k + 2)
              ((100 ^ 3) ^ k)) 0 xs) ∧
      ∃ K₀ : ℝ, 0 ≤ K₀ ∧ ∀ K k V, 0 ≤ V →
        progCost ((bitQC NetProp7.ind₀).toCircuit (q ^ (100 ^ 3) ^ K)) q k V ≤
          K₀ * V * (((100 ^ 3 : ℕ) : ℝ) ^ k) ^ (1 - (2 : ℝ)⁻¹ ^ 50)

Context. The lemma belongs to the part Prop. 7, part 7: the concrete bit network (h = 100) and Prop. 11: T₀ = card-3 subsets of Fin 100 (v = 161700), each with z_b = 3·C(97,2) = 13968 neighbours, W_b = 177176569091445000000 wires, m = 10⁶, and the rank sum s_b = W_b m − N + 2L_b = 177176569088785861287000000. With τ = 1 − 2^{−50}: s_b / W_b < m^τ (hs_bit), since m^τ ≥ m (1 − 20·2^{−50}) (log m < 20). Then prop7_prop11 applies AModelRat.prop11_ratLabels.

Formalization Note. This lemma belongs to the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the array model of tape data (mixed-radix arrays and pull maps), the interchange networks of §3–4 (Propositions 7, 8, 11, Lemmas 9–12), the butterfly layers of §5 (Lemma 13, Proposition 14), the synthesis of §6–7 (Lemma 16, Proposition 18), the resampling and parameter choices of §8–9, and the final glue IntMul.OpenAI.Glue.kappaBound_of_machine, which derives the platform bound KappaBound (1/2^182) (from Def_IntMul_MultitapeModel) for any correct multitape machine meeting the paper's time recurrence. All names refer to the definition bundles IntMul_Kappa_K_Defs1–IntMul_Kappa_K_Defs9.