Coded polynomials and the upper-bound certificate check #

The coded layer of the upper semidecision of the commuting-operator value (planning/tsirelson-campaign.md, §3.5–§3.6). Everything here is a finite list computation on naturals, primitive recursive, and independent of the algebra NCPoly that gives it meaning; the semantic layer decodes it.

Coded polynomials. A letter (Letter) is inl (x, a), the first player's effect e_xa, or inr (y, b), the second player's f_yb; a word is a List Letter. A coded polynomial (CPoly) is a list of monomials (w, c), a word and a coded Gaussian integer (GInt), and it denotes Σ c·w; the list is not normalized, so a word may occur several times. The operations are the list-level ones: cadd concatenates, cneg and cscale c act on the coefficients, cmul multiplies every monomial of one factor by every monomial of the other, cstar reverses the words and conjugates the coefficients (the letters are self-adjoint), and cconst c, cword w, cletter l are the one-monomial polynomials.

Merged coefficients and dominance. The coefficient of a word w in l is the sum of the coefficients of the monomials of l with word w (coeffRaw). The distinct words of l are words l = (l.map Prod.fst).dedup, and the off-diagonal mass offMass l is the sum, over the nonempty distinct words, of the taxicab norm taxi of the merged coefficient, where taxi z = |Re z| + |Im z| is computed on naturals (taxi_eq). A coded polynomial is dominant (IsDominant) if the real part of its merged constant coefficient strictly exceeds its off-diagonal mass. isDominant_iff_sum restates this over any finite set of words containing those of l: Σ_{w ≠ ∅} (|Re l_w| + |Im l_w|) < Re l_∅.

Relations and the game polynomial. A relation index (RelIdx) is inl x (the first player's normalization Σ_{a ≤ nA} e_xa − 1), inr (inl y) (the second player's, Σ_{b ≤ nA} f_yb − 1), or inr (inr (x, y, a, b)) (the commutator e_xa f_yb − f_yb e_xa); relPoly nA gives the polynomial. For a game description d, Wint d is the integer game polynomial Σ_{x, y ≤ nX} Σ_{a, b ≤ nA} wt(x, y) [Draw(x, y, a, b)] e_xa f_yb, which is W d times the game polynomial of d.game. Letters and relation indices are validated against the alphabets of d.game (questions ≤ nX, answers ≤ nA, for both players): ValidLetter, ValidWord, ValidCPoly, ValidRel, and every construction here preserves validity (validCPoly_certR).

Certificates. A certificate (Cert) is a triple (N, sos, ideal): a natural N, a list of sum-of-squares terms (g, s) standing for s⋆ g s (with g = none read as 1), and a list of ideal monomials (c, w, ρ, w') standing for c · w · relPoly ρ · w'. With D = N², the residual is certR d p q (N, sos, ideal) = D·(p·W d·1 − q·Wint d) − Σ s⋆ g s − Σ c·w·ρ·w', and CheckUpper (d, p, q) cert accepts iff q > 0, N ≥ 1, all letters and relation indices of the certificate are valid, and the hermitian residual certRh = certR + certR⋆ is dominant. The test q > 0 is essential: p / 0 = 0 in the consumer CommutingUpperRE. The test runs on merged coefficients, without which it would be sound but never complete.

The main result is primrecRel_checkUpper : PrimrecRel CheckUpper, which with MIPRE.ValueApprox.REPred.of_primrecRel_exists makes the set of accepted (d, p, q) recursively enumerable.

Main declarations #

Letter, CPoly, cadd, cneg, cscale, cmul, cstar, cconst, cword, cletter;
gneg, ptaxi, taxi, taxi_eq;
coeffRaw, coeffRaw_eq_zero_of_notMem, and the coefficients of cadd, cneg, cscale, cstar;
words, dedup_eq_foldr, offMass, offMass_eq_sum, offMass_eq_sum_of_subset, IsDominant, isDominant_iff, isDominant_iff_sum;
ValidLetter, ValidWord, ValidCPoly, ValidOptLetter, RelIdx, ValidRel, relPoly, Wint, Cert, optPoly, sosSum, idealSum, certR, certRh, ValidCert, CheckUpper, and the validity lemmas validCPoly_certR, validCPoly_certRh;
primitive recursiveness of every definition, ending with primrecRel_checkUpper.

Coded polynomials and the upper-bound certificate check #

Main declarations #

Coded Gaussian integers: negation and the taxicab norm #

Coded polynomials #

Merged coefficients and dominance #

Validation, relations and the game polynomial #

Certificates and the check #

Merged coefficients #

Distinct words and dominance #

Validity #

Primitive recursiveness: coefficients and operations #

Primitive recursiveness: validation #

Primitive recursiveness: relations and the game polynomial #

Primitive recursiveness: certificates and the check #