The pipeline with three separate computed values (round six, `pipeline_err3`)

The pipeline with three separate computed values (per-call procedures): U ≈ F u, V ≈ F v, and Z ≈ F(conj z) for z = Q_p(U V).

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

theorem NLogN.KFZ.pipeline_err3 {κ : Type*} [Fintype κ] (p : ℕ) {F : (κ → ℂ) → (κ → ℂ)} (hF : LinC F)
    (Es : ℝ) (hEs : Es * hp p ≤ 1 / 100) {u v : κ → ℂ} (hu1 : ‖u‖ ≤ 1 / 4) (hv1 : ‖v‖ ≤ 1 / 4)
    {U V Z : κ → ℂ} (hU : ‖U - F u‖ ≤ Es * hp p) (hV : ‖V - F v‖ ≤ Es * hp p)
    (hZ : ‖Z - F (cnj (QA p (U * V)))‖ ≤ Es * hp p) :
    Grid p (QA p (U * V)) ∧ ‖QA p (U * V)‖ ≤ 1 / 2 ∧
    ‖cnj Z - cnj (F (cnj (F u * F v)))‖ ≤ (3 * Es + 2) * hp p

Context. KFZ: the per-call form of the chirp interface

ChirpNeed fixes M̃r per n before the input and the machine state, and asks the procedure to output exactly C̃(x) = chirpT p (mcT p M̃r θ̃ θ̃⁻) b̃ ã x. With P18IL as the only source of M̃r, this cannot be met. P18IL gives, for each initial state encK s f (unmanaged part s, tail l on stack 0), some run with some result zh within the Prop 18 bound. Nothing ties the results of two different states together, and a P18IL procedure may legally read s or l and restore it. The dependence on the input tape Isym can be removed (KFZIsym); the dependence on s and l cannot. The obvious workaround, computing mrX exactly, is an integer product of size Θ(V) and does not fit the V · Ncost · polylog budget.

This file gives the per-call statement and shows that it gives the chain everything it uses:

• ChirpNeedR: ChirpNeed with ∃ Mrt (and its ErC · hp bound) moved after the input. The tables θ̃, θ̃⁻, ã, b̃ and ζ stay fixed per n (they are explicit FM table outputs).
• ChirpNeed.toR: ChirpNeed → ChirpNeedR.
• chirp_call_err: for any M̃r with the Prop 18 bound and the fixed tables, one call satisfies ‖C̃ x − Q F_t x‖ ≤ (Er + 22) hp, ‖C̃ x‖ ≤ 1, Grid p (C̃ x). These are exactly the conclusions chain_close uses about the chirp step (its hCt).
• pipeline_err3: pipeline_err with three separate computed values F̃u, F̃v, F̃(z̄) instead of one

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).