chirpNeedR_of_P18 (KFZ Main: `P18IL → ChirpNeedR`)

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

theorem NLogN.KFZ.chirpNeedR_of_P18 (H : P18IL) : ChirpNeedR

Context. The lemma belongs to the part KFZ Main: P18IL → ChirpNeedR: The chirp procedure body (KFZFull) is kmain's own procedure 0 in the merged table mExt ext₁₈ ∅ ∅ [body]; the Prop 18 procedure is reached through gI (mTable_g1, IRuns.relabel). The descriptor stack is cS = 36 (the chirp descriptor stays there and is restored by setupP).

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.