Proposition 8 for the complex network (h = 100, m = 10⁶)

Proposition 8 for the complex network (h = 100, m = 10⁶).

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

theorem NetComplexP8.prop8 :
    Fintype.card (Wr NetComplex.ind₀) = 1873807244643542670000 ∧
    FramesOK2 (fun a b => EdgeP (dec a) (dec b)) (gatesF NetComplex.ind₀) (MinF NetComplex.ind₀) (MoutF NetComplex.ind₀) ∧
    frameSum2 (fun a b => Fd (dec a) (dec b)) (gatesF NetComplex.ind₀) (MinF NetComplex.ind₀) (MoutF NetComplex.ind₀) =
      1873807244636671267308000000 ∧
    (1873807244636671267308000000 : ℕ) < Fintype.card (Wr NetComplex.ind₀) * (100 ^ 3) ∧
    mapG (fun a => qL (dec a)) (gatesF NetComplex.ind₀) = cxFixGatesL ℂ NetComplex.ind₀ (fun n => qL (labS NetComplex.ind₀ n)) ∧
    (∀ w, NetComplexProp8.Min8 (NetComplexP8.uA NetComplex.ind₀) w = qL (dec (MinF NetComplex.ind₀ w))) ∧
    (∀ w, NetComplexProp8.Mout8 (NetComplexP8.uA NetComplex.ind₀) w = qL (dec (MoutF NetComplex.ind₀ w))) ∧
    (∀ a, NetComplexPhase.wt (NetComplexP8.uA NetComplex.ind₀ a) = 27 ∧ NetComplexP8.uA NetComplex.ind₀ a ⬝ᵥ NetComplexP8.uA NetComplex.ind₀ a = 1) ∧
    (∀ (f : Wr NetComplex.ind₀ → NetComplexInterface.Arr (100 ^ 3)) (w : Wr NetComplex.ind₀), (∀ a, w ≠ Sum.inl a) →
      netRun PhiQ (cxFixGatesL ℂ NetComplex.ind₀ (fun n => qL (labS NetComplex.ind₀ n)))
        (NetComplexProp8.Min8 (NetComplexP8.uA NetComplex.ind₀)) (NetComplexProp8.Mout8 (NetComplexP8.uA NetComplex.ind₀)) f (ρ NetComplex.ind₀ w) =
        Cten (f w)) ∧
    (∀ (f : Wr NetComplex.ind₀ → NetComplexInterface.Arr (100 ^ 3)) a (f' : NetComplexInterface.Arr (100 ^ 3)), f (Sum.inl a) = Zu (NetComplexP8.uA NetComplex.ind₀ a) f' →
      I ^ 27 • Zu (NetComplexP8.uA NetComplex.ind₀ a) (netRun PhiQ (cxFixGatesL ℂ NetComplex.ind₀ (fun n => qL (labS NetComplex.ind₀ n)))
        (NetComplexProp8.Min8 (NetComplexP8.uA NetComplex.ind₀)) (NetComplexProp8.Mout8 (NetComplexP8.uA NetComplex.ind₀)) f
          (ρ NetComplex.ind₀ (Sum.inl a))) = Cten f')

Context. The lemma belongs to the part Proposition 8 (complex network, binary phase interface), assembled: The corrected complex network cxFixNamed (Lemma 5, physical gate order) carries the labels of table (6) (labS). To use the generic network bookkeeping (FramesOK2, frameSum2, which need an additive group of labels) we label the gates by FreeAddGroup.of (labS g) and decode with dec (dec ∘ of = id); relabelling by q_U = wt ∘ P_U (mod 4) gives exactly the phase-frame network cxFixGatesL ℂ ind (q ∘ labS) of NetComplexProp8.

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.