Programs for the Pauli clauses of the tailored introspection verifier

The Z-basis guard of Typed.pauliDir compares the kernel's projection of the readable Z answer with a register of the Sample answer. zGuardProg decides it in polynomial time from the kernel's parameter triple, the readable answer and the register: it runs the kernel's full answer program (QLD.PauliBinaryProgram.fullAnswer), whose second output is the projection's bits, and compares them with the register cut or padded to the same length. zGuardProg_eq is its correctness at answers of the label's length.

pauliConsProg computes the Pauli basis test's constraints PauliCons.pauliCons from the parameter triple, Q = 2^(2^j) k in unary (the constraints have up to 2Q + 1 bits, more than a polynomial in the questions alone), and the two labelled question payloads. It follows the kernel's own route (PauliBranchProgram.route): equal labels give the bitwise comparison (sameP, same_eq), and rule r of pairTest gives r1, …, r7. Every check of pairChecks is affine in the answer bits, so its constraint vector is its value at the unit vectors (PauliConsUnit): the program runs over the unit vectors of the answer bits, decodes each into the two answers with the kernel's parser, and evaluates the rule's expression with the kernel's field programs (the line parameter and Horner evaluation, the low-degree table, the trace probe, bit reads); a field equation contributes the k coordinates of its values (fieldCons, by transposition), a bit equation its values (boolCon). The question-only conditions (the point on the line, γ(ω), the Magic Square incidences) are the kernel's own programs (memberProg, gammaProg, magicInfo, probeEligible).

• rule1, …, rule7: each rule program against its pairChecks branch, for either orientation;
• pauliConsProg_eq: the program computes pauliCons, for j ≤ k and payloads of length (3·2^j + 3) k (the kernel's question parser is characterized there).

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.fitTo : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr

A bit string cut or padded with zeros to the length of a reference string.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.PauliConsProg.fitTo_apply (r z : Cost.BitStr) : fitTo.toFun (r, z) = List.take (List.length r) (z ++ List.replicate (List.length r) false)

theorem MIPRE.Tailored.Intro.PauliConsProg.toBits_ofBits_eq_fit (s : ℕ) (z : Cost.BitStr) : CL.toBits (CL.ofBits s z) = List.take s (z ++ List.replicate s false)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.zGuardProg : Cost.PolyTimeFun (Introspection.PauliSamplerParameters.Parameters × Cost.BitStr × Cost.BitStr) Bool

The Z-basis guard: the projection of the readable Z answer is the register.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.PauliConsProg.zGuardProg_eq (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (aR z : Cost.BitStr) (ha : List.length aR = pauliLen (2 ^ j) k (QLD.Ty.pauli QLD.Bas.Z)) : zGuardProg.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), aR, z) = decide (Typed.proj k hk hodd j (Typed.pDec k hk j (QLD.Ty.pauli QLD.Bas.Z) aR) = CL.ofBits (Typed.Q k j) z)

The Z-basis guard is decided by zGuardProg, at readable answers of the label's length.

The Pauli basis test's constraints: the programs

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.PauliConsProg.PIn : Type

The input: parameters, Q in unary, and the two labelled question payloads.

Equations

• MIPRE.Tailored.Intro.PauliConsProg.PIn = (MIPRE.Introspection.PauliSamplerParameters.Parameters × MIPRE.Cost.Unary × (MIPRE.QLD.Ty × MIPRE.Cost.BitStr) × MIPRE.QLD.Ty × MIPRE.Cost.BitStr)

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.PauliConsProg.PPos : Type

An input and a unit vector of the answer bits.

Equations

• MIPRE.Tailored.Intro.PauliConsProg.PPos = (MIPRE.Tailored.Intro.PauliConsProg.PIn × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.pP : Cost.PolyTimeFun PIn Introspection.PauliSamplerParameters.Parameters

Equations

• MIPRE.Tailored.Intro.PauliConsProg.pP = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.uK : Cost.PolyTimeFun PIn Cost.Unary

Equations

• MIPRE.Tailored.Intro.PauliConsProg.uK = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Tailored.Intro.PauliConsProg.pP

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.uM : Cost.PolyTimeFun PIn Cost.Unary

Equations

• MIPRE.Tailored.Intro.PauliConsProg.uM = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Tailored.Intro.PauliConsProg.pP)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.uQ : Cost.PolyTimeFun PIn Cost.Unary

Equations

• MIPRE.Tailored.Intro.PauliConsProg.uQ = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.tA : Cost.PolyTimeFun PIn QLD.Ty

Equations

• MIPRE.Tailored.Intro.PauliConsProg.tA = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.xA : Cost.PolyTimeFun PIn Cost.BitStr

Equations

• MIPRE.Tailored.Intro.PauliConsProg.xA = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.tB : Cost.PolyTimeFun PIn QLD.Ty

Equations

• MIPRE.Tailored.Intro.PauliConsProg.tB = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.xB : Cost.PolyTimeFun PIn Cost.BitStr

Equations

• MIPRE.Tailored.Intro.PauliConsProg.xB = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.lenBranch : QLD.Ty → Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.Unary × QLD.Ty) Cost.Unary

The answer length of a label, pauliLen m k T, in unary, from k, m and 2^m k.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.Intro.PauliConsProg.lenBranch (MIPRE.QLD.Ty.point W) = MIPRE.Cost.PolyTimeFun.fst
• MIPRE.Tailored.Intro.PauliConsProg.lenBranch (MIPRE.QLD.Ty.aline W) = MIPRE.Cost.PolyTimeFun.append.comp (MIPRE.Cost.PolyTimeFun.fst.pair MIPRE.Cost.PolyTimeFun.fst)
• MIPRE.Tailored.Intro.PauliConsProg.lenBranch (MIPRE.QLD.Ty.pauli W) = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)
• MIPRE.Tailored.Intro.PauliConsProg.lenBranch (MIPRE.QLD.Ty.pairB W) = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 1)
• MIPRE.Tailored.Intro.PauliConsProg.lenBranch (MIPRE.QLD.Ty.var j) = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 1)
• MIPRE.Tailored.Intro.PauliConsProg.lenBranch MIPRE.QLD.Ty.pair = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 2)
• MIPRE.Tailored.Intro.PauliConsProg.lenBranch (MIPRE.QLD.Ty.con i) = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 3)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.lenProg : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.Unary × QLD.Ty) Cost.Unary

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.lenA : Cost.PolyTimeFun PIn Cost.Unary

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.lenB : Cost.PolyTimeFun PIn Cost.Unary

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.lenN : Cost.PolyTimeFun PIn Cost.Unary

Equations

• MIPRE.Tailored.Intro.PauliConsProg.lenN = MIPRE.Cost.PolyTimeFun.append.comp (MIPRE.Tailored.Intro.PauliConsProg.lenA.pair MIPRE.Tailored.Intro.PauliConsProg.lenB)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.fA : Cost.PolyTimeFun PIn Introspection.PauliStageProgram.Fields

Equations

• MIPRE.Tailored.Intro.PauliConsProg.fA = MIPRE.QLD.PauliBinaryProgram.fieldsProg.comp (MIPRE.Tailored.Intro.PauliConsProg.pP.pair MIPRE.Tailored.Intro.PauliConsProg.xA)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.fB : Cost.PolyTimeFun PIn Introspection.PauliStageProgram.Fields

Equations

• MIPRE.Tailored.Intro.PauliConsProg.fB = MIPRE.QLD.PauliBinaryProgram.fieldsProg.comp (MIPRE.Tailored.Intro.PauliConsProg.pP.pair MIPRE.Tailored.Intro.PauliConsProg.xB)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.rt : Cost.PolyTimeFun PIn QLD.PauliBranchProgram.Route

Equations

• MIPRE.Tailored.Intro.PauliConsProg.rt = MIPRE.QLD.PauliBranchProgram.routeProg.comp (MIPRE.Tailored.Intro.PauliConsProg.tA.pair MIPRE.Tailored.Intro.PauliConsProg.tB)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.sw : Cost.PolyTimeFun PIn Bool

Equations

• MIPRE.Tailored.Intro.PauliConsProg.sw = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Tailored.Intro.PauliConsProg.rt)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.bas : Cost.PolyTimeFun PIn ℕ

Equations

• MIPRE.Tailored.Intro.PauliConsProg.bas = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Tailored.Intro.PauliConsProg.rt))

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.lF : Cost.PolyTimeFun PIn Introspection.PauliStageProgram.Fields

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.rF : Cost.PolyTimeFun PIn Introspection.PauliStageProgram.Fields

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.lT : Cost.PolyTimeFun PIn QLD.Ty

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.rT : Cost.PolyTimeFun PIn QLD.Ty

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.ptL : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• MIPRE.Tailored.Intro.PauliConsProg.ptL = MIPRE.Introspection.FieldQuestionProgram.selectedPoint.comp (MIPRE.Tailored.Intro.PauliConsProg.bas.pair MIPRE.Tailored.Intro.PauliConsProg.lF)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.ptR : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• MIPRE.Tailored.Intro.PauliConsProg.ptR = MIPRE.Introspection.FieldQuestionProgram.selectedPoint.comp (MIPRE.Tailored.Intro.PauliConsProg.bas.pair MIPRE.Tailored.Intro.PauliConsProg.rF)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.axisR : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.dirR : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• MIPRE.Tailored.Intro.PauliConsProg.dirR = MIPRE.Introspection.PauliStageProgram.direction.comp MIPRE.Tailored.Intro.PauliConsProg.rF

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.tauA : Cost.PolyTimeFun PIn Cost.BitStr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.tauD : Cost.PolyTimeFun PIn Cost.BitStr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.memA : Cost.PolyTimeFun PIn Bool

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.memD : Cost.PolyTimeFun PIn Bool

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.gamR : Cost.PolyTimeFun PIn Bool

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.scR : Cost.PolyTimeFun PIn Cost.BitStr

Equations

• MIPRE.Tailored.Intro.PauliConsProg.scR = MIPRE.Introspection.FieldQuestionProgram.selectedScalar.comp (MIPRE.Tailored.Intro.PauliConsProg.bas.pair MIPRE.Tailored.Intro.PauliConsProg.rF)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.magic : Cost.PolyTimeFun PIn (Bool × Bool × ℕ)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.elig : Cost.PolyTimeFun PIn Bool

Equations

• One or more equations did not get rendered due to their size.

Reading the unit vector

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.rowsA : Cost.PolyTimeFun PPos (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.rowsB : Cost.PolyTimeFun PPos (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.lR : Cost.PolyTimeFun PPos (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.rR : Cost.PolyTimeFun PPos (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.lV : Cost.PolyTimeFun PPos Cost.BitStr

Equations

• MIPRE.Tailored.Intro.PauliConsProg.lV = (MIPRE.Cost.PolyTimeFun.nthD [] 0).comp MIPRE.Tailored.Intro.PauliConsProg.lR

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.boolXor : Cost.PolyTimeFun (Bool × Bool) Bool

Equations

• MIPRE.Tailored.Intro.PauliConsProg.boolXor = MIPRE.Cost.PolyTimeFun.finiteFunction fun (p : Bool × Bool) => p.1 ^^ p.2

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.bitOf (i : ℕ) (rows : Cost.PolyTimeFun PPos (List Cost.BitStr)) : Cost.PolyTimeFun PPos Bool

Equations

• MIPRE.Tailored.Intro.PauliConsProg.bitOf i rows = MIPRE.QLD.PauliBooleanProgram.bitAt.comp ((MIPRE.Cost.PolyTimeFun.const i).pair rows)

The values at a unit vector

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.v1 : Cost.PolyTimeFun PPos Cost.BitStr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.v2 : Cost.PolyTimeFun PPos Cost.BitStr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.v3 : Cost.PolyTimeFun PPos Cost.BitStr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.v4 : Cost.PolyTimeFun PPos Bool

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.v5 : Cost.PolyTimeFun PPos Bool

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.v6a : Cost.PolyTimeFun PPos Bool

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.v6b : Cost.PolyTimeFun PPos Bool

Equations

• One or more equations did not get rendered due to their size.

Constraint vectors

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.units : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• MIPRE.Tailored.Intro.PauliConsProg.units = MIPRE.LowDegree.BinaryLinear.identityBitsProg.comp MIPRE.Tailored.Intro.PauliConsProg.lenN

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.fieldCons (val : Cost.PolyTimeFun PPos Cost.BitStr) : Cost.PolyTimeFun PIn (List Cost.BitStr)

The k constraints of a field equation, from its values at the unit vectors.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.boolCon (val : Cost.PolyTimeFun PPos Bool) (target : Cost.PolyTimeFun PIn Bool) : Cost.PolyTimeFun PIn Cost.BitStr

The constraint of a bit equation, from its values at the unit vectors and its target.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.rejectP : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.r1 : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.r2 : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.r3 : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• MIPRE.Tailored.Intro.PauliConsProg.r3 = MIPRE.Tailored.Intro.PauliConsProg.fieldCons MIPRE.Tailored.Intro.PauliConsProg.v3

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.r4 : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.r5 : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.r6 : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.r7 : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.isRule (r : ℕ) : Cost.PolyTimeFun PIn Bool

Equations

• MIPRE.Tailored.Intro.PauliConsProg.isRule r = MIPRE.SAT.ArrayProg.eqNat.ap₂ (MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Tailored.Intro.PauliConsProg.rt) (MIPRE.Cost.PolyTimeFun.const r)

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.sameP : Cost.PolyTimeFun PIn (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.PauliConsProg.pauliConsProg : Cost.PolyTimeFun PIn (List Cost.BitStr)

The Pauli basis test's constraints, as a program.

Equations

• One or more equations did not get rendered due to their size.

The Pauli basis test's constraints: correctness

theorem MIPRE.Tailored.Intro.PauliConsProg.range_map_eq_ofFn {α : Type u_1} (n : ℕ) (g : ℕ → α) : List.map g (List.range n) = List.ofFn fun (p : Fin n) => g ↑p

theorem MIPRE.Tailored.Intro.PauliConsProg.units_eq {inp : PIn} {N : ℕ} (hN : lenN.toFun inp = Cost.unary N) : units.toFun inp = List.ofFn fun (p : Fin N) => LowDegree.BinaryLinear.unitBits N ↑p

The unit vectors of the answer bits.

theorem MIPRE.Tailored.Intro.PauliConsProg.fieldCons_eq {k : ℕ} {hk : 1 ≤ k} {inp : PIn} {N : ℕ} (hK : uK.toFun inp = Cost.unary k) (hN : lenN.toFun inp = Cost.unary N) (val : Cost.PolyTimeFun PPos Cost.BitStr) (E : (Fin N → ZMod 2) →ₗ[ZMod 2] (SAT.shoupBinField k hk).carrier) (hval : ∀ (p : Fin N), val.toFun (inp, LowDegree.BinaryLinear.unitBits N ↑p) = (SAT.shoupBinField k hk).toBits (E (PauliHideProg.unitV p))) : (fieldCons val).toFun inp = List.map LinCheck.toCon (fieldChecks k hk E 0)

Field constraints from unit values.

theorem MIPRE.Tailored.Intro.PauliConsProg.boolCon_eq {inp : PIn} {N : ℕ} (hN : lenN.toFun inp = Cost.unary N) (val : Cost.PolyTimeFun PPos Bool) (target : Cost.PolyTimeFun PIn Bool) (χ : LinCheck N) (hval : ∀ (p : Fin N), val.toFun (inp, LowDegree.BinaryLinear.unitBits N ↑p) = LowDegree.BinaryLinear.bit (χ.φ (PauliHideProg.unitV p))) (ht : target.toFun inp = LowDegree.BinaryLinear.bit χ.c) : (boolCon val target).toFun inp = χ.toCon

A bit constraint from unit values.

theorem MIPRE.Tailored.Intro.PauliConsProg.rejectP_eq {inp : PIn} {N : ℕ} (hN : lenN.toFun inp = Cost.unary N) : rejectP.toFun inp = [(LinCheck.reject N).toCon]

Reading the unit vectors

theorem MIPRE.Tailored.Intro.PauliConsProg.parser_snd_eq {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (T : QLD.Ty) (a : Cost.BitStr) (ha : List.length a = pauliLen M k T) : (QLD.PauliAnswerProgram.parser.toFun (T, Cost.unary M, Cost.unary k, Cost.unary 1, a)).2 = QLD.PauliAnswerProgram.answerRows (SAT.shoupBinField k hk) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 T a)

theorem MIPRE.Tailored.Intro.PauliConsProg.pos_facts {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB : QLD.Ty} {LA LB : ℕ} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (p : Fin (LA + LB)) : PauliCons.Reads (PauliHideProg.unitV p) 0 (QLD.PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 TA (List.take LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p)))) ∧ PauliCons.Reads (PauliHideProg.unitV p) LA (QLD.PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 TB (List.drop LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p)))) ∧ rowsA.toFun (inp, LowDegree.BinaryLinear.unitBits (LA + LB) ↑p) = QLD.PauliAnswerProgram.answerRows (SAT.shoupBinField k hk) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 TA (List.take LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p))) ∧ rowsB.toFun (inp, LowDegree.BinaryLinear.unitBits (LA + LB) ↑p) = QLD.PauliAnswerProgram.answerRows (SAT.shoupBinField k hk) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 TB (List.drop LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p)))

The decoded answers at a unit vector, and what the programs and the checks read of them.

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.PauliConsProg.dL {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (TA TB : QLD.Ty) (LA N : ℕ) (s : Bool) (p : Fin N) : QLD.Answer (SAT.shoupBinField k hk).carrier M 1

The left and right decoded answers at a unit vector (after the route's orientation).

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.PauliConsProg.dR {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (TA TB : QLD.Ty) (LA N : ℕ) (s : Bool) (p : Fin N) : QLD.Answer (SAT.shoupBinField k hk).carrier M 1

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.PauliConsProg.lr_facts {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB : QLD.Ty} {LA LB : ℕ} {s : Bool} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (hs : sw.toFun inp = s) (p : Fin (LA + LB)) : PauliCons.Reads (PauliHideProg.unitV p) (if s = true then LA else 0) (QLD.PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) (dL TA TB LA (LA + LB) s p)) ∧ PauliCons.Reads (PauliHideProg.unitV p) (if s = true then 0 else LA) (QLD.PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) (dR TA TB LA (LA + LB) s p)) ∧ lR.toFun (inp, LowDegree.BinaryLinear.unitBits (LA + LB) ↑p) = QLD.PauliAnswerProgram.answerRows (SAT.shoupBinField k hk) (dL TA TB LA (LA + LB) s p) ∧ rR.toFun (inp, LowDegree.BinaryLinear.unitBits (LA + LB) ↑p) = QLD.PauliAnswerProgram.answerRows (SAT.shoupBinField k hk) (dR TA TB LA (LA + LB) s p)

theorem MIPRE.Tailored.Intro.PauliConsProg.lr_facts₂ {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB TL TR : QLD.Ty} {LA LB : ℕ} {s : Bool} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (hs : sw.toFun inp = s) (hTL : (if s = true then TB else TA) = TL) (hTR : (if s = true then TA else TB) = TR) (p : Fin (LA + LB)) : PauliCons.Reads (PauliHideProg.unitV p) (if s = true then LA else 0) (QLD.PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 TL (if s = true then List.drop LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p) else List.take LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p)))) ∧ PauliCons.Reads (PauliHideProg.unitV p) (if s = true then 0 else LA) (QLD.PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 TR (if s = true then List.take LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p) else List.drop LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p)))) ∧ lR.toFun (inp, LowDegree.BinaryLinear.unitBits (LA + LB) ↑p) = QLD.PauliAnswerProgram.answerRows (SAT.shoupBinField k hk) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 TL (if s = true then List.drop LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p) else List.take LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p))) ∧ rR.toFun (inp, LowDegree.BinaryLinear.unitBits (LA + LB) ↑p) = QLD.PauliAnswerProgram.answerRows (SAT.shoupBinField k hk) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 TR (if s = true then List.take LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p) else List.drop LA (LowDegree.BinaryLinear.unitBits (LA + LB) ↑p)))

The facts of lr_facts, with the labels of the two sides named.

theorem MIPRE.Tailored.Intro.PauliConsProg.dec_point {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (W : QLD.Bas) (a : Cost.BitStr) : ∃ (x : (SAT.shoupBinField k hk).carrier), QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 (QLD.Ty.point W) a = QLD.Answer.val x

theorem MIPRE.Tailored.Intro.PauliConsProg.dec_aline {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (W : QLD.Bas) (a : Cost.BitStr) : ∃ (f : LIDT.LinePoly (SAT.shoupBinField k hk).carrier 1), QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 (QLD.Ty.aline W) a = QLD.Answer.apoly f

theorem MIPRE.Tailored.Intro.PauliConsProg.dec_dline {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (W : QLD.Bas) (a : Cost.BitStr) : ∃ (f : LIDT.LinePoly (SAT.shoupBinField k hk).carrier (M * 1)), QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 (QLD.Ty.dline W) a = QLD.Answer.dpoly f

theorem MIPRE.Tailored.Intro.PauliConsProg.dec_pauli {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (W : QLD.Bas) (a : Cost.BitStr) : ∃ (h : (Fin M → Bool) → (SAT.shoupBinField k hk).carrier), QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 (QLD.Ty.pauli W) a = QLD.Answer.pauliAns h

theorem MIPRE.Tailored.Intro.PauliConsProg.dec_pairB {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (W : QLD.Bas) (a : Cost.BitStr) : ∃ (b : ZMod 2), QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 (QLD.Ty.pairB W) a = QLD.Answer.bit b

theorem MIPRE.Tailored.Intro.PauliConsProg.dec_pair {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (a : Cost.BitStr) : ∃ (β : QLD.Bas → ZMod 2), QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 QLD.Ty.pair a = QLD.Answer.bitPair β

theorem MIPRE.Tailored.Intro.PauliConsProg.dec_con {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (a : Cost.BitStr) (i : Fin LCS.MagicSquare.layout.r) : ∃ (α : Fin 3 → ZMod 2), QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 (QLD.Ty.con i) a = QLD.Answer.bitTriple α

theorem MIPRE.Tailored.Intro.PauliConsProg.dec_var {k : ℕ} {hk : 1 ≤ k} {M : ℕ} (a : Cost.BitStr) (j : Fin LCS.MagicSquare.layout.s) : ∃ (b : ZMod 2), QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 (QLD.Ty.var j) a = QLD.Answer.bit b

theorem MIPRE.Tailored.Intro.PauliConsProg.bit_add (x y : ZMod 2) : LowDegree.BinaryLinear.bit (x + y) = (LowDegree.BinaryLinear.bit x ^^ LowDegree.BinaryLinear.bit y)

theorem MIPRE.Tailored.Intro.PauliConsProg.bit_ne (x : ZMod 2) : LowDegree.BinaryLinear.bit x = true ↔ x ≠ 0

theorem MIPRE.Tailored.Intro.PauliConsProg.bitAt_apply (i : ℕ) (rows : List Cost.BitStr) : QLD.PauliBooleanProgram.bitAt.toFun (i, rows) = List.getD (rows.getD i []) 0 false

Rules 1 and 2: a line against a point

theorem MIPRE.Tailored.Intro.PauliConsProg.xorBits_toBits {k : ℕ} {hk : 1 ≤ k} (a b : (SAT.shoupBinField k hk).carrier) : LowDegree.BinaryPolynomial.xorBits ((SAT.shoupBinField k hk).toBits a) ((SAT.shoupBinField k hk).toBits b) = (SAT.shoupBinField k hk).toBits (a + b)

theorem MIPRE.Tailored.Intro.PauliConsProg.line_core {k : ℕ} {hk : 1 ≤ k} {inp : PIn} {N n oL oR : ℕ} (hK : uK.toFun inp = Cost.unary k) (hN : lenN.toFun inp = Cost.unary N) (τ : (SAT.shoupBinField k hk).carrier) (val : Cost.PolyTimeFun PPos Cost.BitStr) (hv : ∀ (u : Cost.BitStr), val.toFun (inp, u) = LowDegree.BinaryPolynomial.xorBits (Introspection.FieldPolynomialProgram.shoupHornerProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).toBits τ, rR.toFun (inp, u))) (lV.toFun (inp, u))) (hp : ∀ (p : Fin N), ∃ (f : Fin (n + 1) → (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier), rR.toFun (inp, LowDegree.BinaryLinear.unitBits N ↑p) = (SAT.shoupBinField k hk).vecBits f ∧ lR.toFun (inp, LowDegree.BinaryLinear.unitBits N ↑p) = [(SAT.shoupBinField k hk).toBits a] ∧ (fldAt k hk N oL) (PauliHideProg.unitV p) = a ∧ ∀ (i : Fin (n + 1)), (fldAt k hk N (oR + ↑i * k)) (PauliHideProg.unitV p) = f i) : (fieldCons val).toFun inp = List.map LinCheck.toCon (fieldChecks k hk (∑ i : Fin (n + 1), LinearMap.mulRight (ZMod 2) (τ ^ ↑i) ∘ₗ fldAt k hk N (oR + ↑i * k) - fldAt k hk N oL) 0)

The line values at the unit vectors are the line equation's.

theorem MIPRE.Tailored.Intro.PauliConsProg.rule1 {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB : QLD.Ty} {LA LB : ℕ} {s : Bool} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hN : lenN.toFun inp = Cost.unary (LA + LB)) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (hs : sw.toFun inp = s) {W : QLD.Bas} (hTL : (if s = true then TB else TA) = QLD.Ty.point W) (hTR : (if s = true then TA else TB) = QLD.Ty.aline W) (u₀ w y : Fin M → (SAT.shoupBinField k hk).carrier) (htau : tauA.toFun inp = (SAT.shoupBinField k hk).toBits (LIDT.CL.lineParam u₀ w y)) (hmem : memA.toFun inp = decide (∃ (t : (SAT.shoupBinField k hk).carrier), y = u₀ + t • w)) : r1.toFun inp = List.map LinCheck.toCon (PauliCons.lineChecks k hk (LA + LB) 1 (if s = true then LA else 0) (if s = true then 0 else LA) u₀ w y)

Rule 1, the axis-parallel line against a point.

theorem MIPRE.Tailored.Intro.PauliConsProg.rule2 {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB : QLD.Ty} {LA LB : ℕ} {s : Bool} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hN : lenN.toFun inp = Cost.unary (LA + LB)) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (hs : sw.toFun inp = s) {W : QLD.Bas} (hTL : (if s = true then TB else TA) = QLD.Ty.point W) (hTR : (if s = true then TA else TB) = QLD.Ty.dline W) (u₀ w y : Fin M → (SAT.shoupBinField k hk).carrier) (htau : tauD.toFun inp = (SAT.shoupBinField k hk).toBits (LIDT.CL.lineParam u₀ w y)) (hmem : memD.toFun inp = decide (∃ (t : (SAT.shoupBinField k hk).carrier), y = u₀ + t • w)) : r2.toFun inp = List.map LinCheck.toCon (PauliCons.lineChecks k hk (LA + LB) (M * 1) (if s = true then LA else 0) (if s = true then 0 else LA) u₀ w y)

Rule 2, the diagonal line against a point.

theorem MIPRE.Tailored.Intro.PauliConsProg.rule3 {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB : QLD.Ty} {LA LB : ℕ} {s : Bool} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hN : lenN.toFun inp = Cost.unary (LA + LB)) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (hs : sw.toFun inp = s) {W : QLD.Bas} (hTL : (if s = true then TB else TA) = QLD.Ty.point W) (hTR : (if s = true then TA else TB) = QLD.Ty.pauli W) (y : Fin M → (SAT.shoupBinField k hk).carrier) (hpt : ptL.toFun inp = (SAT.shoupBinField k hk).vecBits y) : r3.toFun inp = List.map LinCheck.toCon (PauliCons.pauliChecks k hk (LA + LB) (if s = true then LA else 0) (if s = true then 0 else LA) y)

Rule 3, the point probe against the full Pauli outcome.

theorem MIPRE.Tailored.Intro.PauliConsProg.rule4 {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB : QLD.Ty} {LA LB : ℕ} {s : Bool} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hN : lenN.toFun inp = Cost.unary (LA + LB)) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (hs : sw.toFun inp = s) {W : QLD.Bas} (hTL : (if s = true then TB else TA) = QLD.Ty.pairB W) (hTR : (if s = true then TA else TB) = QLD.Ty.pair) (ω : QLD.Omega (SAT.shoupBinField k hk).carrier M) (hgam : gamR.toFun inp = LowDegree.BinaryLinear.bit (QLD.gam ω)) (hbas : bas.toFun inp = PauliCons.basIdx W) : r4.toFun inp = List.map LinCheck.toCon (if QLD.gam ω ≠ 0 then [] else [PauliCons.bitEq (LA + LB) (if s = true then LA else 0) ((if s = true then 0 else LA) + PauliCons.basIdx W)])

Rule 4, the commutation check.

theorem MIPRE.Tailored.Intro.PauliConsProg.prb_core {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB : QLD.Ty} {LA LB : ℕ} {s : Bool} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hN : lenN.toFun inp = Cost.unary (LA + LB)) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (hs : sw.toFun inp = s) {TL TR : QLD.Ty} (hTL : (if s = true then TB else TA) = TL) (hTR : (if s = true then TA else TB) = TR) (hTL' : ∀ (a : Cost.BitStr), ∃ (x : (SAT.shoupBinField k hk).carrier), QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 TL a = QLD.Answer.val x) (hTR' : ∀ (a : Cost.BitStr), ∃ (b : ZMod 2), QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) M 1 TR a = QLD.Answer.bit b) (r : (SAT.shoupBinField k hk).carrier) (hsc : scR.toFun inp = (SAT.shoupBinField k hk).toBits r) : (boolCon v5 (Cost.PolyTimeFun.const false)).toFun inp = (PauliCons.prbCheck k hk (LA + LB) r (if s = true then LA else 0) (if s = true then 0 else LA)).toCon

The probe values at the unit vectors.

theorem MIPRE.Tailored.Intro.PauliConsProg.rule5 {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB : QLD.Ty} {LA LB : ℕ} {s : Bool} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hN : lenN.toFun inp = Cost.unary (LA + LB)) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (hs : sw.toFun inp = s) {W : QLD.Bas} (hTL : (if s = true then TB else TA) = QLD.Ty.point W) (hTR : (if s = true then TA else TB) = QLD.Ty.pairB W) (ω : QLD.Omega (SAT.shoupBinField k hk).carrier M) (hgam : gamR.toFun inp = LowDegree.BinaryLinear.bit (QLD.gam ω)) (hsc : scR.toFun inp = (SAT.shoupBinField k hk).toBits (ω.r W)) : r5.toFun inp = List.map LinCheck.toCon (if QLD.gam ω ≠ 0 then [] else [PauliCons.prbCheck k hk (LA + LB) (ω.r W) (if s = true then LA else 0) (if s = true then 0 else LA)])

Rule 5, the commutation consistency check.

theorem MIPRE.Tailored.Intro.PauliConsProg.rule6 {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB : QLD.Ty} {LA LB : ℕ} {s : Bool} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hN : lenN.toFun inp = Cost.unary (LA + LB)) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (hs : sw.toFun inp = s) {i : Fin LCS.MagicSquare.layout.r} {j' : Fin LCS.MagicSquare.layout.s} (hTL : (if s = true then TB else TA) = QLD.Ty.con i) (hTR : (if s = true then TA else TB) = QLD.Ty.var j') (ω : QLD.Omega (SAT.shoupBinField k hk).carrier M) (hgam : gamR.toFun inp = LowDegree.BinaryLinear.bit (QLD.gam ω)) (hmagic : magic.toFun inp = QLD.PauliBooleanProgram.magicInfo (QLD.Ty.con i, QLD.Ty.var j')) : r6.toFun inp = List.map LinCheck.toCon (PauliCons.conVarChecks k hk (LA + LB) i j' ω (if s = true then LA else 0) (if s = true then 0 else LA))

Rule 6, the Magic Square check.

theorem MIPRE.Tailored.Intro.PauliConsProg.rule7 {k : ℕ} {hk : 1 ≤ k} {M : ℕ} {inp : PIn} {TA TB : QLD.Ty} {LA LB : ℕ} {s : Bool} (hK : uK.toFun inp = Cost.unary k) (hM : uM.toFun inp = Cost.unary M) (hA : tA.toFun inp = TA) (hB : tB.toFun inp = TB) (hLA : lenA.toFun inp = Cost.unary LA) (hN : lenN.toFun inp = Cost.unary (LA + LB)) (hA' : LA = pauliLen M k TA) (hB' : LB = pauliLen M k TB) (hs : sw.toFun inp = s) {W : QLD.Bas} {j' : Fin LCS.MagicSquare.layout.s} (hTL : (if s = true then TB else TA) = QLD.Ty.point W) (hTR : (if s = true then TA else TB) = QLD.Ty.var j') (ω : QLD.Omega (SAT.shoupBinField k hk).carrier M) (hgam : gamR.toFun inp = LowDegree.BinaryLinear.bit (QLD.gam ω)) (hsc : scR.toFun inp = (SAT.shoupBinField k hk).toBits (ω.r W)) (helig : elig.toFun inp = QLD.PauliBooleanProgram.probeEligible (QLD.Ty.point W, QLD.Ty.var j')) : r7.toFun inp = List.map LinCheck.toCon (PauliCons.pointVarChecks k hk (LA + LB) W j' ω (if s = true then LA else 0) (if s = true then 0 else LA))

Rule 7, the Magic Square consistency check.

Lengths and equal labels

theorem MIPRE.Tailored.Intro.PauliConsProg.lenProg_apply (k m : ℕ) (T : QLD.Ty) : lenProg.toFun (Cost.unary k, Cost.unary m, Cost.unary (2 ^ m * k), T) = Cost.unary (pauliLen m k T)

theorem MIPRE.Tailored.Intro.PauliConsProg.same_eq (L : ℕ) : (List.ofFn fun (l : Fin L) => LowDegree.BinaryLinear.unitBits L ↑l ++ LowDegree.BinaryLinear.unitBits L ↑l ++ [false]) = List.map LinCheck.toCon (PauliCons.sameChecks (L + L) L)

The concrete input

def MIPRE.Tailored.Intro.PauliConsProg.inputOf (k j : ℕ) (t u : QLD.Ty) (x y : Cost.BitStr) : PIn

The program's input at labels t, u and question payloads x, y.

Equations

• MIPRE.Tailored.Intro.PauliConsProg.inputOf k j t u x y = ((MIPRE.Cost.unary k, MIPRE.Cost.unary j, MIPRE.Cost.unary (2 ^ j)), MIPRE.Cost.unary (2 ^ 2 ^ j * k), (t, x), u, y)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.PauliConsProg.qv (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (x : Cost.BitStr) : QLD.PauliCL.Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier

The question vector a payload decodes to.

Equations

• MIPRE.Tailored.Intro.PauliConsProg.qv k hk hodd j x = (MIPRE.QLD.PauliCL.binaryVectorEquiv (MIPRE.SAT.shoupSelfDualNormalBasis k hk hodd)).symm (MIPRE.CL.ofBits ((3 * 2 ^ j + 3) * k) x)

theorem MIPRE.Tailored.Intro.PauliConsProg.dispatch (inp : PIn) (h : tA.toFun inp ≠ tB.toFun inp) : pauliConsProg.toFun inp = if (rt.toFun inp).1 = 1 then r1.toFun inp else if (rt.toFun inp).1 = 2 then r2.toFun inp else if (rt.toFun inp).1 = 3 then r3.toFun inp else if (rt.toFun inp).1 = 4 then r4.toFun inp else if (rt.toFun inp).1 = 5 then r5.toFun inp else if (rt.toFun inp).1 = 6 then r6.toFun inp else if (rt.toFun inp).1 = 7 then r7.toFun inp else []

theorem MIPRE.Tailored.Intro.PauliConsProg.pt_content (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (π : (SAT.shoupBinField k hk).carrier ≃ (SAT.shoupBinField k hk).carrier) (X : QLD.PauliCL.Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) (W : QLD.Bas) : ((QLD.PauliCL.ExplicitSeed.contentPermutation π) (QLD.PauliCL.vectorContent X)).pt W = fun (i : Fin (2 ^ j)) => X (QLD.PauliCL.Coord.point W i)

theorem MIPRE.Tailored.Intro.PauliConsProg.omega_content (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (π : (SAT.shoupBinField k hk).carrier ≃ (SAT.shoupBinField k hk).carrier) (X : QLD.PauliCL.Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) : ((QLD.PauliCL.ExplicitSeed.contentPermutation π) (QLD.PauliCL.vectorContent X)).omega = (QLD.PauliCL.vectorContent X).omega

theorem MIPRE.Tailored.Intro.PauliConsProg.r_omega (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (X : QLD.PauliCL.Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) (W : QLD.Bas) : (QLD.PauliCL.vectorContent X).omega.r W = X (QLD.PauliCL.Coord.scalar W)

theorem MIPRE.Tailored.Intro.PauliConsProg.basisIndex_eq (W : QLD.Bas) : QLD.PauliBranchProgram.basisIndex W = PauliCons.basIdx W

theorem MIPRE.Tailored.Intro.PauliConsProg.memberProg_eq {k : ℕ} {hk : 1 ≤ k} {m : ℕ} (o d p : Fin m → (SAT.shoupBinField k hk).carrier) : Introspection.FieldLineCheck.memberProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).vecBits o, (SAT.shoupBinField k hk).vecBits d, (SAT.shoupBinField k hk).vecBits p) = decide (∃ (t : (SAT.shoupBinField k hk).carrier), p = o + t • d)

theorem MIPRE.Tailored.Intro.PauliConsProg.pauliConsProg_eq {k : ℕ} {hk : 1 ≤ k} [NeZero k] {hodd : Odd k} {j : ℕ} (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (t u : QLD.Ty) (x y aR bR : Cost.BitStr) (hx : List.length x = (3 * 2 ^ j + 3) * k) (hy : List.length y = (3 * 2 ^ j + 3) * k) : pauliConsProg.toFun (inputOf k j t u x y) = PauliCons.pauliCons k hk hodd j hm t u x y aR bR

The program computes the Pauli basis test's constraints, exactly, at question payloads of the right length.