The actual introspection decision kernel

The preparer supplies one shared clock, the source programs, the exponential index, and the canonical Pauli parameters. This kernel parses the raw typed input, runs the actual Pauli predicate and endpoint parsers, and composes them with both orientations of the guarded auxiliary predicate.

noncomputable def MIPRE.Introspection.DecisionKernel.questionDimension : Cost.PolyTimeFun Input ℕ

The ambient question dimension is polynomial in the explicit unary parameters.

Equations

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

theorem MIPRE.Introspection.DecisionKernel.questionDimension_apply (z : Input) : questionDimension.toFun z = (3 * List.length (parameters.toFun z).2.2 + 3) * List.length (parameters.toFun z).1

noncomputable def MIPRE.Introspection.DecisionKernel.questionLengths : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.zeroPrefix : Cost.PolyTimeFun Input Cost.BitStr

Allocate only as many dummy prefix bits as the input already supplies. Every formatted auxiliary endpoint supplies at least one full register.

Equations

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

theorem MIPRE.Introspection.DecisionKernel.zeroPrefix_apply (z : Input) : zeroPrefix.toFun z = List.replicate (min (registerWidth.toFun z) (List.length (leftBits.toFun z) + List.length (rightBits.toFun z))) false

theorem MIPRE.Introspection.DecisionKernel.zeroPrefix_of_length (z : Input) (h : registerWidth.toFun z ≤ List.length (leftBits.toFun z) + List.length (rightBits.toFun z)) : zeroPrefix.toFun z = List.replicate (registerWidth.toFun z) false

noncomputable def MIPRE.Introspection.DecisionKernel.sourceContext : Cost.PolyTimeFun Input AuxiliarySource.Context

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.sourceDimension (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Input ℕ

Equations

• MIPRE.Introspection.DecisionKernel.sourceDimension U = (MIPRE.Introspection.SourcePadding.Program.dimension U).comp MIPRE.Introspection.DecisionKernel.sourceContext

noncomputable def MIPRE.Introspection.DecisionKernel.auxiliaryInput (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Input (AuxiliaryDecision.Input QLD.Ty 7)

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.project : Cost.PolyTimeFun (AuxiliaryDecision.Input QLD.Ty 7) Cost.BitStr

Full Pauli answer bytes are converted to the same self-dual register coordinates used by the source checks.

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.auxiliary (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Input Bool

Equations

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

def MIPRE.Introspection.DecisionKernel.isPauli : Label → Bool

Equations

• MIPRE.Introspection.DecisionKernel.isPauli (Sum.inl val) = true
• MIPRE.Introspection.DecisionKernel.isPauli (Sum.inr val) = false

def MIPRE.Introspection.DecisionKernel.pauliLabel : Label → QLD.Ty

Equations

• MIPRE.Introspection.DecisionKernel.pauliLabel (Sum.inl val) = val
• MIPRE.Introspection.DecisionKernel.pauliLabel (Sum.inr val) = MIPRE.QLD.Ty.pauli MIPRE.QLD.Bas.X

noncomputable def MIPRE.Introspection.DecisionKernel.leftIsPauli : Cost.PolyTimeFun Input Bool

Equations

• MIPRE.Introspection.DecisionKernel.leftIsPauli = (MIPRE.Cost.PolyTimeFun.finiteFunction MIPRE.Introspection.DecisionKernel.isPauli).comp MIPRE.Introspection.DecisionKernel.leftType

noncomputable def MIPRE.Introspection.DecisionKernel.rightIsPauli : Cost.PolyTimeFun Input Bool

Equations

• MIPRE.Introspection.DecisionKernel.rightIsPauli = (MIPRE.Cost.PolyTimeFun.finiteFunction MIPRE.Introspection.DecisionKernel.isPauli).comp MIPRE.Introspection.DecisionKernel.rightType

noncomputable def MIPRE.Introspection.DecisionKernel.leftPauliPayload : Cost.PolyTimeFun Input QLD.PauliBinaryProgram.Payload

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.rightPauliPayload : Cost.PolyTimeFun Input QLD.PauliBinaryProgram.Payload

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.leftPauliFormat : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.rightPauliFormat : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.pauli : Cost.PolyTimeFun Input Bool

Equations

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

noncomputable def MIPRE.Introspection.DecisionKernel.program (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun Input Bool

One polynomial-time kernel handles every raw input.

Equations

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

theorem MIPRE.Introspection.DecisionKernel.program_iff (U : Cost.ClockedUniversalMachine) (z : Input) : (program U).toFun z = true ↔ canonical.toFun z = true ∧ questionLengths.toFun z = true ∧ leftPauliFormat.toFun z = true ∧ rightPauliFormat.toFun z = true ∧ pauli.toFun z = true ∧ (auxiliary U).toFun z = true

theorem MIPRE.Introspection.DecisionKernel.auxiliaryInput_apply (U : Cost.ClockedUniversalMachine) (z : Input) : (auxiliaryInput U).toFun z = ((sourceContext.toFun z, (registerWidth.toFun z, originalCutoff.toFun z, (sourceDimension U).toFun z, sourceDecider.toFun z), parameters.toFun z), (leftType.toFun z, leftBits.toFun z), rightType.toFun z, rightBits.toFun z)

theorem MIPRE.Introspection.DecisionKernel.sourceContext_apply (z : Input) : sourceContext.toFun z = (budget.toFun z, sourceSampler.toFun z, sourceIndex.toFun z, false, 1, zeroPrefix.toFun z)

theorem MIPRE.Introspection.DecisionKernel.pauli_apply (z : Input) : pauli.toFun z = if (AuxiliaryProgram.andCheck leftIsPauli rightIsPauli).toFun z = true then QLD.PauliBinaryProgram.program.toFun (parameters.toFun z, leftPauliPayload.toFun z, rightPauliPayload.toFun z) else true