Fixed punctures cost at most one MCA parameter per removed node and joint pair
ProvedProximityPadePunctureTransfer.mca_card_le_punctured_addLet F be a field, nodes a finite indexed evaluation domain with injective evaluation points x, and u₀,u₁ arbitrary F-valued words. Fix a set C of indices to remove, a polynomial degree bound w, agreement thresholds A,A′, and an upper bound L on the number of polynomial pairs of degree at most w that simultaneously agree with the two originals at at least A′ nodes of the punctured domain. Assume A′+|C|≤A and w<A′.
For a parameter γ, MCA means that on one support T of at least the stated threshold, u₀+γu₁ admits a degree-at-most-w polynomial fit while the two originals do not both admit such fits on that same T. Given any finite set Γ of original-domain MCA parameters,
|Γ| ≤ |{γ∈Γ : γ remains MCA after removing C at threshold A′}| + |C|·L.
The paired-list premise is explicit: every finite set of distinct low-degree polynomial pairs with at least A′ simultaneous agreements on nodes minus C has cardinality at most L. It is not a bound on two separate lists with unrelated supports. The puncture C is fixed for all parameters; it need not be a subset of nodes, in which case |C| is a conservative charge. All fitting supports and candidate polynomials may depend on γ.
For each lost parameter, the surviving part of its original witness fits both words. More than w injective points force the original combination polynomial to equal P₀+γP₁. Original nonfit supplies a removed node where this chosen pair mismatches. The second-word mismatch is nonzero, so its ratio determines γ. The set of lost parameters is covered by the image of the chosen joint-pair list times C, giving |C|·L.
Relation to the open NTT exact-support MCA target: this bounds only parameters lost under a fixed puncture. A bound or classification for retained punctured MCA parameters is still required. This generic theorem supplies no concrete benchmark list bound, universal classification, complete protocol certificate, novelty claim, or official score improvement.
import Mathlib.Algebra.Polynomial.Eval.SMul import Mathlib.Algebra.Polynomial.Roots import Mathlib.Tactic.LinearCombination import Mathlib.Tactic.Push import Mathlib.Tactic.Choose import Lean.Elab.Tactic.Omega open Polynomial
theorem ProximityPadePunctureTransfer.mca_card_le_punctured_add {F I : Type*} [Field F] [DecidableEq F] [DecidableEq I]
(nodes C : Finset I) (x u0 u1 : I → F) (w A A' L : ℕ)
(hinj : Set.InjOn x (nodes : Set I)) (hA : A' + C.card ≤ A) (hw : w < A') :
let fits : (I → F) → Finset I → Prop := fun u T =>
∃ P : F[X], P.natDegree ≤ w ∧ ∀ i ∈ T, P.eval (x i) = u i
let mca : Finset I → ℕ → F → Prop := fun domain threshold γ =>
∃ T : Finset I, T ⊆ domain ∧ threshold ≤ T.card ∧
fits (fun i => u0 i + γ * u1 i) T ∧ ¬(fits u0 T ∧ fits u1 T)
let joint : F[X] × F[X] → Prop := fun pair =>
pair.1.natDegree ≤ w ∧ pair.2.natDegree ≤ w ∧
A' ≤ ((nodes \ C).filter (fun i => pair.1.eval (x i) = u0 i ∧
pair.2.eval (x i) = u1 i)).card
(∀ D : Finset (F[X] × F[X]), (∀ pair ∈ D, joint pair) → D.card ≤ L) →
∀ Γ : Finset F, (∀ γ ∈ Γ, mca nodes A γ) →
Γ.card ≤ (@Finset.filter F (mca (nodes \ C) A')
(fun _ => Classical.propDecidable _) Γ).card + C.card * L := by
sorry