Open candidate: exact-support MCA bound on the NTT domain for lower 68.16
OpenDirectMCAResearch.NTT.exact_support_mca_bound_6816Open sufficient MCA subgoal; unproved. A sufficient exact-support MCA counting subgoal for lower 68.16 on the NTT evaluation domain. This is not the full protocol root or an unconditional numerical theorem. List contribution, larger-support reduction, embedding into benchmark definitions, and final radius/protocol assembly remain outside this statement.
The cardinality and root conditions select the full set of 262144th roots of unity, with all nodes Frobenius-fixed, independently of a primitive-root choice or indexing. The power condition excludes zero. The general all-subfield-domains root is preserved separately.
Arbitrary fields of characteristic p and cardinality p^6. Arbitrary polynomial words; only their values on S enter the predicate. For each counted parameter the excluded set E may vary; the combined word is code on S minus E while the two originals are not both code on that same selected support. The excluded set has exactly 80909 nodes, so its selected support has 181235 nodes. The proposed bound is 274980718450187492 distinct affine parameters. The nontriviality condition is evaluated on the same selected support as the combined-word agreement.
Universal rank-gate coverage or a bound for its failure is unresolved. The NTT domain condition is available to future reciprocal-Pade arguments but is not used by the existing conditional rank child. The existing conditional child additionally assumes an injective ring map from K[X] into a field, a selected nonzero minor at the generic pencil rank, and equality of the augmented and unaugmented generic ranks. That child is locally checked on Lean 4.32.2 only; it is not a proof of this open statement and is not uploaded here.
This publication records a candidate research question. Only statement elaboration is checked on the provider target Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. No root proof, accepted solution, full protocol certificate, or official score improvement is asserted.
import Mathlib.Algebra.CharP.Defs import Mathlib.Algebra.Polynomial.Degree.Defs import Mathlib.Algebra.Polynomial.Eval.Defs import Mathlib.Data.Finset.Card import Mathlib.Data.Finset.SDiff set_option autoImplicit false
theorem DirectMCAResearch.NTT.exact_support_mca_bound_6816 :
∀ (K : Type) [Field K] [Fintype K] [DecidableEq K] [CharP K 2130706433],
Fintype.card K = 2130706433^6 →
∀ S : Finset K, S.card = 262144 →
(∀ x ∈ S, x^2130706433 = x ∧ x^262144 = 1) →
let codeOn : Polynomial K → Finset K → Prop := fun Y A =>
∃ f : Polynomial K, f.natDegree < 131072 ∧ ∀ x ∈ A, Y.eval x = f.eval x
∀ (Y0 Y1 : Polynomial K) (Gamma : Finset K),
(∀ t ∈ Gamma, ∃ E : Finset K, E ⊆ S ∧ E.card = 80909 ∧
codeOn (Y0 + t • Y1) (S \ E) ∧
¬(codeOn Y0 (S \ E) ∧ codeOn Y1 (S \ E))) →
Gamma.card ≤ 274980718450187492 := by
sorry