The subgroup test associated with a tailored game #
Paper I, Definition I:2086, for the tailored games of MIPRE/TailoredGameValue.lean. The test
assocTest g has the generators J (index 0) and one generator X(x, i) for each vertex x
and each i < Λ (index 1 + x Λ + i, Λ = g.ansLen); those with i ≥ ℓ(x) appear in no word.
It has one challenge per question pair (x, y), weighted by the pair's weight in g (with the
game's convention when every weight vanishes: a single challenge at (0, 0)). The words K of
the challenge at (x, y) are, in order:
- the fixed words (
fixedLits):J(required out ofH), thenJ²,[J, X]for every variableXatxand aty,X²for the same, and[X, X']for the pairs of variables atxand aty(all required inH) — Checks 1 and 2; - the readable words (
readWords): for each readable variable atx, then aty, the pairX,J X— Check 3; - the constraint words (
consWords): the distinct words of the entries ofg.consat(x, y), the word of a constraintcbeingJ^{c_J} ∏ X(x, i)^{c_i} ∏ X(y, i)^{c_{ℓ(x) + i}}, orJwhenchas the wrong length (the game rejects it, andJ ∈ Hcontradicts Check 1) — Check 4.
The decision is one clause per value r of the readable variables: the fixed literals, the
readable word of r at each readable variable (X when its bit is 0, J X when 1), and
the constraint words of the entries whose readable part is r. Exactly the subgroups the paper's
decision D̃_{xy} accepts satisfy some clause.
Words #
The inverse of a word.
Equations
- MIPRE.Tailored.Sofic.invW w = (List.map (fun (l : SubgroupTestValue.Letter) => (l.1, !l.2)) w).reverse
Instances For
The commutator [u, v] = u v u⁻¹ v⁻¹.
Equations
Instances For
The one-letter word of a generator.
Instances For
The generator of J.
Equations
Instances For
The question weights of g, as a GameData (g.weights, computably).
Instances For
The generator X(x, i).
Instances For
The number of generators.
Instances For
The word J.
Instances For
The word X(x, i).
Equations
Instances For
The variables at x: X(x, i) for i < ℓ(x).
Equations
- MIPRE.Tailored.Sofic.varsAt g x = List.map (MIPRE.Tailored.Sofic.wX g x) (List.range (g.lenAt x))
Instances For
The words of a challenge #
The fixed words, Checks 1 and 2, with the membership each must have.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The readable variables at x, then at y.
Equations
- MIPRE.Tailored.Sofic.readVars g x y = List.map (MIPRE.Tailored.Sofic.wX g x) (List.range (g.lenRAt x)) ++ List.map (MIPRE.Tailored.Sofic.wX g y) (List.range (g.lenRAt y))
Instances For
The readable words: X then J X for each readable variable.
Equations
- MIPRE.Tailored.Sofic.readWords g x y = List.flatMap (fun (X : SubgroupTestValue.Word) => [X, MIPRE.Tailored.Sofic.wJ ++ X]) (MIPRE.Tailored.Sofic.readVars g x y)
Instances For
The entries of g.cons at (x, y).
Equations
Instances For
The word of a constraint c at (x, y): J^{c_J} ∏ X(x, i)^{c_i} ∏ X(y, i)^{c_{ℓ(x)+i}},
or J when c has the wrong length.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The constraint words at (x, y): the distinct words of its entries. Distinct constraints of
the right length give at most 2^{ℓ(x) + ℓ(y) + 1} words, which bounds the significance
(Proposition I:2283) however often g.cons repeats an entry.
Equations
- MIPRE.Tailored.Sofic.consWords g x y = (List.map (fun (e : ℕ × ℕ × List Bool × List Bool) => MIPRE.Tailored.Sofic.consWord g x y e.2.2.2) (MIPRE.Tailored.Sofic.consAt g x y)).dedup
Instances For
The words K of the challenge at (x, y).
Equations
Instances For
The clauses #
The clause of the readable value r: the fixed literals, the readable words of r, and the
constraint words of the entries whose readable part is r.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The clauses at (x, y), one per readable value.
Equations
- MIPRE.Tailored.Sofic.clauses g x y = List.map (MIPRE.Tailored.Sofic.clause g x y) (MIPRE.Tailored.Sofic.allBits (g.lenRAt x + g.lenRAt y))
Instances For
The test #
The challenge at (x, y), with weight w.
Equations
- MIPRE.Tailored.Sofic.challenge g w x y = (w, MIPRE.Tailored.Sofic.words g x y, MIPRE.Tailored.Sofic.clauses g x y)
Instances For
The synchronous subgroup test associated with a tailored game (Definition I:2086).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Actions passing Checks 1–3 #
The permutation of the generator k under a finite action.
Equations
Instances For
An action passing Checks 1–3 of the associated test at every point and every question
pair (Proposition I:2279, the strategies it applies to): J is a fixed-point-free involution
commuting with every variable X(x, i), i < ℓ(x); these are involutions, commuting at each
vertex; and each readable variable acts at every point as the identity or as J (Z-alignment,
Definition I:2026).