Proposition 14 (unconditional)

Proposition 14 (unconditional). On [P] × [2^K]^D × [S] with bit ρ of every chunk selected, the layer procedure whose C-layer is the recursive complex-network program (cRecC) returns exactly Q_p(H0^{⊗D} z); for disk inputs every output coefficient lies in the unit disk and differs from the exact layer H0^{⊗D} z by less than √2 · 2^{-p}.

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

theorem GlueP14.prop14_unconditional {P K D S ρ r : ℕ} (hρ : ρ < K) (p : ℕ)
    (xs : List (Fin r → ℂ)) (hxs : ∀ j (h : j < xs.length), ‖xs[j]‖ ≤ 1) :
    prop14Proc (P := P) (S := S) hρ p (cRecC D) xs = QpArr p (layerH P K D S ρ hρ xs) ∧
    (∀ j (h : j < (prop14Proc (P := P) (S := S) hρ p (cRecC D) xs).length), ∀ c,
      ‖(prop14Proc (P := P) (S := S) hρ p (cRecC D) xs)[j] c‖ ≤ 1) ∧
    (∀ j (h : j < (prop14Proc (P := P) (S := S) hρ p (cRecC D) xs).length)
      (h' : j < (layerH P K D S ρ hρ xs).length), ∀ c,
      ‖(prop14Proc (P := P) (S := S) hρ p (cRecC D) xs)[j] c - (layerH P K D S ρ hρ xs)[j] c‖
        < Real.sqrt 2 * 2⁻¹ ^ p)

Context. The lemma belongs to the part Glue 1: Proposition 14 unconditionally (through complexIface): ButterflyProp14.prop14_output takes an implementation Cimpl of C^{⊗D} on the D selected bits together with a proof Cimpl = tens Cm. Here we build that implementation from the recursive program recOp of an arbitrary Prop8Iface (the network recursion of §5.1), cutting the D selected bits into consecutive pieces of sizes u · m^k given by the base-m digits of D (piece k = the depth-k program with leaf width u = k-th digit), embedding each piece on its block of bits and multiplying (tens_blocks, embed_tens).

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.