The uniform Boolean Pauli decision program

Both answers undergo the exact type-directed parser. A faithful finite type route chooses consistency or one of the seven arithmetic rules. The finite Magic Square metadata contains only type indices; field arithmetic, answer tables and polynomial coefficients are processed by uniform programs.

@[reducible, inline]

abbrev MIPRE.QLD.PauliBooleanProgram.Payload : Type

Equations

• MIPRE.QLD.PauliBooleanProgram.Payload = (MIPRE.QLD.Ty × MIPRE.Introspection.PauliStageProgram.Fields × MIPRE.Cost.BitStr)

@[reducible, inline]

abbrev MIPRE.QLD.PauliBooleanProgram.Input : Type

Equations

• MIPRE.QLD.PauliBooleanProgram.Input = (MIPRE.Introspection.PauliStageProgram.Parameters × MIPRE.QLD.PauliBooleanProgram.Payload × MIPRE.QLD.PauliBooleanProgram.Payload)

noncomputable def MIPRE.QLD.PauliBooleanProgram.params : Cost.PolyTimeFun Input Introspection.PauliStageProgram.Parameters

Equations

• MIPRE.QLD.PauliBooleanProgram.params = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.QLD.PauliBooleanProgram.width : Cost.PolyTimeFun Input Cost.Unary

Equations

• MIPRE.QLD.PauliBooleanProgram.width = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.QLD.PauliBooleanProgram.params

noncomputable def MIPRE.QLD.PauliBooleanProgram.dim : Cost.PolyTimeFun Input Cost.Unary

Equations

• MIPRE.QLD.PauliBooleanProgram.dim = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.QLD.PauliBooleanProgram.params)

noncomputable def MIPRE.QLD.PauliBooleanProgram.endpoints : Cost.PolyTimeFun Input (Payload × Payload)

Equations

• MIPRE.QLD.PauliBooleanProgram.endpoints = MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.QLD.PauliBooleanProgram.endpointTypes : Cost.PolyTimeFun Input (Ty × Ty)

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.route : Cost.PolyTimeFun Input PauliBranchProgram.Route

Equations

• MIPRE.QLD.PauliBooleanProgram.route = MIPRE.QLD.PauliBranchProgram.routeProg.comp MIPRE.QLD.PauliBooleanProgram.endpointTypes

noncomputable def MIPRE.QLD.PauliBooleanProgram.basis : Cost.PolyTimeFun Input ℕ

Equations

• MIPRE.QLD.PauliBooleanProgram.basis = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.QLD.PauliBooleanProgram.route))

noncomputable def MIPRE.QLD.PauliBooleanProgram.oriented : Cost.PolyTimeFun Input (Payload × Payload)

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.left : Cost.PolyTimeFun Input Payload

Equations

• MIPRE.QLD.PauliBooleanProgram.left = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.QLD.PauliBooleanProgram.oriented

noncomputable def MIPRE.QLD.PauliBooleanProgram.right : Cost.PolyTimeFun Input Payload

Equations

• MIPRE.QLD.PauliBooleanProgram.right = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.QLD.PauliBooleanProgram.oriented

noncomputable def MIPRE.QLD.PauliBooleanProgram.leftFields : Cost.PolyTimeFun Input Introspection.PauliStageProgram.Fields

Equations

• MIPRE.QLD.PauliBooleanProgram.leftFields = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.QLD.PauliBooleanProgram.left)

noncomputable def MIPRE.QLD.PauliBooleanProgram.rightFields : Cost.PolyTimeFun Input Introspection.PauliStageProgram.Fields

Equations

• MIPRE.QLD.PauliBooleanProgram.rightFields = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.QLD.PauliBooleanProgram.right)

noncomputable def MIPRE.QLD.PauliBooleanProgram.leftBits : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.QLD.PauliBooleanProgram.leftBits = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.QLD.PauliBooleanProgram.left)

noncomputable def MIPRE.QLD.PauliBooleanProgram.rightBits : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.QLD.PauliBooleanProgram.rightBits = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.QLD.PauliBooleanProgram.right)

noncomputable def MIPRE.QLD.PauliBooleanProgram.leftParser : Cost.PolyTimeFun Input (Bool × List Cost.BitStr)

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.rightParser : Cost.PolyTimeFun Input (Bool × List Cost.BitStr)

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.leftRows : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

• MIPRE.QLD.PauliBooleanProgram.leftRows = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.QLD.PauliBooleanProgram.leftParser

noncomputable def MIPRE.QLD.PauliBooleanProgram.rightRows : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

• MIPRE.QLD.PauliBooleanProgram.rightRows = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.QLD.PauliBooleanProgram.rightParser

noncomputable def MIPRE.QLD.PauliBooleanProgram.leftValue : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.QLD.PauliBooleanProgram.leftValue = (MIPRE.Cost.PolyTimeFun.nthD [] 0).comp MIPRE.QLD.PauliBooleanProgram.leftRows

noncomputable def MIPRE.QLD.PauliBooleanProgram.bitAt : Cost.PolyTimeFun (ℕ × List Cost.BitStr) Bool

Equations

• MIPRE.QLD.PauliBooleanProgram.bitAt = (MIPRE.Cost.PolyTimeFun.nthD false 0).comp (MIPRE.SAT.ArrayProg.getD [])

noncomputable def MIPRE.QLD.PauliBooleanProgram.boolEq : Cost.PolyTimeFun (Bool × Bool) Bool

Equations

• MIPRE.QLD.PauliBooleanProgram.boolEq = MIPRE.Cost.PolyTimeFun.finiteFunction fun (p : Bool × Bool) => p.1 == p.2

noncomputable def MIPRE.QLD.PauliBooleanProgram.boolAnd : Cost.PolyTimeFun (Bool × Bool) Bool

Equations

• MIPRE.QLD.PauliBooleanProgram.boolAnd = MIPRE.Cost.PolyTimeFun.finiteFunction fun (p : Bool × Bool) => p.1 && p.2

noncomputable def MIPRE.QLD.PauliBooleanProgram.boolOr : Cost.PolyTimeFun (Bool × Bool) Bool

Equations

• MIPRE.QLD.PauliBooleanProgram.boolOr = MIPRE.Cost.PolyTimeFun.finiteFunction fun (p : Bool × Bool) => p.1 || p.2

noncomputable def MIPRE.QLD.PauliBooleanProgram.boolNot : Cost.PolyTimeFun Bool Bool

Equations

• MIPRE.QLD.PauliBooleanProgram.boolNot = MIPRE.Cost.PolyTimeFun.finiteFunction fun (x : Bool) => !x

noncomputable def MIPRE.QLD.PauliBooleanProgram.point : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

• MIPRE.QLD.PauliBooleanProgram.point = MIPRE.Introspection.FieldQuestionProgram.selectedPoint.comp (MIPRE.QLD.PauliBooleanProgram.basis.pair MIPRE.QLD.PauliBooleanProgram.leftFields)

noncomputable def MIPRE.QLD.PauliBooleanProgram.origin : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

• MIPRE.QLD.PauliBooleanProgram.origin = MIPRE.Introspection.FieldQuestionProgram.selectedPoint.comp (MIPRE.QLD.PauliBooleanProgram.basis.pair MIPRE.QLD.PauliBooleanProgram.rightFields)

noncomputable def MIPRE.QLD.PauliBooleanProgram.scalar : Cost.PolyTimeFun Input Cost.BitStr

Equations

• MIPRE.QLD.PauliBooleanProgram.scalar = MIPRE.Introspection.FieldQuestionProgram.selectedScalar.comp (MIPRE.QLD.PauliBooleanProgram.basis.pair MIPRE.QLD.PauliBooleanProgram.rightFields)

noncomputable def MIPRE.QLD.PauliBooleanProgram.axis : Cost.PolyTimeFun Input (List Cost.BitStr)

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.consistency : Cost.PolyTimeFun Input Bool

Equations

• MIPRE.QLD.PauliBooleanProgram.consistency = MIPRE.SAT.ArrayProg.eqBits.ap₂ MIPRE.QLD.PauliBooleanProgram.leftBits MIPRE.QLD.PauliBooleanProgram.rightBits

noncomputable def MIPRE.QLD.PauliBooleanProgram.axisCheck : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.diagonalCheck : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.tableCheck : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.gamma : Cost.PolyTimeFun Input Bool

All commutation and Magic Square rules use the omega tuple at the right, distinguished endpoint after the orientation normalization.

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.probe : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.leftBit : Cost.PolyTimeFun Input Bool

Equations

• MIPRE.QLD.PauliBooleanProgram.leftBit = MIPRE.QLD.PauliBooleanProgram.bitAt.comp ((MIPRE.Cost.PolyTimeFun.const 0).pair MIPRE.QLD.PauliBooleanProgram.leftRows)

noncomputable def MIPRE.QLD.PauliBooleanProgram.rightBit : Cost.PolyTimeFun Input Bool

Equations

• MIPRE.QLD.PauliBooleanProgram.rightBit = MIPRE.QLD.PauliBooleanProgram.bitAt.comp ((MIPRE.Cost.PolyTimeFun.const 0).pair MIPRE.QLD.PauliBooleanProgram.rightRows)

noncomputable def MIPRE.QLD.PauliBooleanProgram.pairCheck : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.probeCheck : Cost.PolyTimeFun Input Bool

Equations

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

def MIPRE.QLD.PauliBooleanProgram.magicInfo : Ty × Ty → Bool × Bool × ℕ

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.QLD.PauliBooleanProgram.magicInfo x✝ = (false, false, 0)

noncomputable def MIPRE.QLD.PauliBooleanProgram.magicTypes : Cost.PolyTimeFun Input (Ty × Ty)

Equations

• MIPRE.QLD.PauliBooleanProgram.magicTypes = (MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.QLD.PauliBooleanProgram.left).pair (MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.QLD.PauliBooleanProgram.right)

noncomputable def MIPRE.QLD.PauliBooleanProgram.magicMetadata : Cost.PolyTimeFun Input (Bool × Bool × ℕ)

Equations

• MIPRE.QLD.PauliBooleanProgram.magicMetadata = (MIPRE.Cost.PolyTimeFun.finiteFunction MIPRE.QLD.PauliBooleanProgram.magicInfo).comp MIPRE.QLD.PauliBooleanProgram.magicTypes

noncomputable def MIPRE.QLD.PauliBooleanProgram.parityProg : Cost.PolyTimeFun (Bool × Bool × Bool) Bool

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.leftParity : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.magicCheck : Cost.PolyTimeFun Input Bool

Equations

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

def MIPRE.QLD.PauliBooleanProgram.probeEligible : Ty × Ty → Bool

Equations

• MIPRE.QLD.PauliBooleanProgram.probeEligible (MIPRE.QLD.Ty.point MIPRE.QLD.Bas.X, MIPRE.QLD.Ty.var j) = decide (j = MIPRE.LCS.MagicSquare.v 0 MIPRE.QLD.PauliBooleanProgram.probeEligible._proof_4)
• MIPRE.QLD.PauliBooleanProgram.probeEligible (MIPRE.QLD.Ty.point MIPRE.QLD.Bas.Z, MIPRE.QLD.Ty.var j) = decide (j = MIPRE.LCS.MagicSquare.v 4 MIPRE.QLD.PauliBooleanProgram.probeEligible._proof_5)
• MIPRE.QLD.PauliBooleanProgram.probeEligible x✝ = false

noncomputable def MIPRE.QLD.PauliBooleanProgram.magicProbeCheck : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.checks : Cost.PolyTimeFun Input (List Bool)

Equations

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

noncomputable def MIPRE.QLD.PauliBooleanProgram.program : Cost.PolyTimeFun Input Bool

Equations

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

theorem MIPRE.QLD.PauliBooleanProgram.program_apply (input : Input) : program.toFun input = ((leftParser.toFun input).1 && (rightParser.toFun input).1 && [consistency.toFun input, axisCheck.toFun input, diagonalCheck.toFun input, tableCheck.toFun input, pairCheck.toFun input, probeCheck.toFun input, magicCheck.toFun input, magicProbeCheck.toFun input].getD (route.toFun input).1 true)