Lee-O'Sullivan Candidate Normalization

Soundness and existence facts for normalizing raw Lee-O'Sullivan candidates.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.normalizeLeeCandidate?_sound_of_raw {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {points : Array (F × F)} {params : GSInterpParams} {rawQ Q : CBivariate F} (hHigh : ¬params.messageDegree ≤ 1) (hdeg : rawQ.natWeightedDegree 1 (yWeight params) ≤ params.weightedDegreeBound) (hmult : rawQ.SatisfiesMultiplicityConstraints points params.multiplicity) (hnorm : normalizeLeeCandidate? params rawQ = some Q) : ValidInterpolationWitness points params Q

Normalizing a bounded raw Lee candidate preserves the interpolation witness contract when the raw candidate already satisfies the multiplicity constraints.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.normalizeLeeCandidate?_some_of_raw {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {params : GSInterpParams} {rawQ : CBivariate F} (hHigh : ¬params.messageDegree ≤ 1) (hne : rawQ ≠ 0) (hdeg : rawQ.natWeightedDegree 1 (yWeight params) ≤ params.weightedDegreeBound) : ∃ (Q : CBivariate F), normalizeLeeCandidate? params rawQ = some Q

A nonzero bounded raw Lee candidate can be normalized by the shared coefficient-vector policy.