The uniform auxiliary decision kernel

The finite type labels choose programs, including the fixed-depth hiding scans. Source descriptions, the shared unary clock, dimensions and answer bytes remain runtime data. Pauli arithmetic and conversion are supplied by their separately verified uniform programs.

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliaryDecision.Endpoint (P : Type u_2) (ℓ : ℕ) : Type u_2

Equations

• MIPRE.Introspection.AuxiliaryDecision.Endpoint P ℓ = (MIPRE.Introspection.QuestionType P ℓ × MIPRE.Cost.BitStr)

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliaryDecision.Parameters : Type

Equations

• MIPRE.Introspection.AuxiliaryDecision.Parameters = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliaryDecision.Bounds : Type

Equations

• MIPRE.Introspection.AuxiliaryDecision.Bounds = ((ℕ × ℕ × ℕ × MIPRE.Cost.Prog) × MIPRE.Introspection.AuxiliaryDecision.Parameters)

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliaryDecision.Input (P : Type u_2) (ℓ : ℕ) : Type u_2

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.context {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) AuxiliarySource.Context

Equations

• MIPRE.Introspection.AuxiliaryDecision.context = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Introspection.AuxiliaryDecision.bounds {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) (ℕ × ℕ × ℕ × Cost.Prog)

Equations

• MIPRE.Introspection.AuxiliaryDecision.bounds = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.fst)

noncomputable def MIPRE.Introspection.AuxiliaryDecision.pauliParameters {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) Parameters

Equations

• MIPRE.Introspection.AuxiliaryDecision.pauliParameters = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.fst)

noncomputable def MIPRE.Introspection.AuxiliaryDecision.width {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) ℕ

Equations

• MIPRE.Introspection.AuxiliaryDecision.width = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Introspection.AuxiliaryDecision.bounds

noncomputable def MIPRE.Introspection.AuxiliaryDecision.originalBound {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) ℕ

Equations

• MIPRE.Introspection.AuxiliaryDecision.originalBound = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Introspection.AuxiliaryDecision.bounds)

noncomputable def MIPRE.Introspection.AuxiliaryDecision.sourceDim {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) ℕ

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.sourceDecider {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) Cost.Prog

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.left {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) (Endpoint P ℓ)

Equations

• MIPRE.Introspection.AuxiliaryDecision.left = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Introspection.AuxiliaryDecision.right {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) (Endpoint P ℓ)

Equations

• MIPRE.Introspection.AuxiliaryDecision.right = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Introspection.AuxiliaryDecision.leftType {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) (QuestionType P ℓ)

Equations

• MIPRE.Introspection.AuxiliaryDecision.leftType = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Introspection.AuxiliaryDecision.left

noncomputable def MIPRE.Introspection.AuxiliaryDecision.rightType {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) (QuestionType P ℓ)

Equations

• MIPRE.Introspection.AuxiliaryDecision.rightType = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Introspection.AuxiliaryDecision.right

noncomputable def MIPRE.Introspection.AuxiliaryDecision.leftBits {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) Cost.BitStr

Equations

• MIPRE.Introspection.AuxiliaryDecision.leftBits = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Introspection.AuxiliaryDecision.left

noncomputable def MIPRE.Introspection.AuxiliaryDecision.rightBits {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) Cost.BitStr

Equations

• MIPRE.Introspection.AuxiliaryDecision.rightBits = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Introspection.AuxiliaryDecision.right

noncomputable def MIPRE.Introspection.AuxiliaryDecision.swap {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) (Input P ℓ)

Equations

• MIPRE.Introspection.AuxiliaryDecision.swap = MIPRE.Cost.PolyTimeFun.fst.pair (MIPRE.Introspection.AuxiliaryDecision.right.pair MIPRE.Introspection.AuxiliaryDecision.left)

@[simp]

theorem MIPRE.Introspection.AuxiliaryDecision.swap_apply {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} (ctx : AuxiliarySource.Context) (b : Bounds) (a d : Endpoint P ℓ) : swap.toFun ((ctx, b), a, d) = ((ctx, b), d, a)

noncomputable def MIPRE.Introspection.AuxiliaryDecision.rightPair {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) (Cost.BitStr × Cost.BitStr)

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.leftTriple {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) (Cost.BitStr × Cost.BitStr × Cost.BitStr)

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.rightTriple {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) (Cost.BitStr × Cost.BitStr × Cost.BitStr)

Equations

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

def MIPRE.Introspection.AuxiliaryDecision.formatKind {P : Type u_1} {ℓ : ℕ} : QuestionType P ℓ → Fin 4

Pauli format validation is delegated to its field-aware parser.

Equations

• MIPRE.Introspection.AuxiliaryDecision.formatKind (Sum.inl val) = 0
• MIPRE.Introspection.AuxiliaryDecision.formatKind (Sum.inr (MIPRE.Introspection.AuxType.introspect, snd)) = 1
• MIPRE.Introspection.AuxiliaryDecision.formatKind (Sum.inr (MIPRE.Introspection.AuxType.sample, snd)) = 1
• MIPRE.Introspection.AuxiliaryDecision.formatKind (Sum.inr (MIPRE.Introspection.AuxType.read, snd)) = 2
• MIPRE.Introspection.AuxiliaryDecision.formatKind (Sum.inr (MIPRE.Introspection.AuxType.hide k, snd)) = 3

noncomputable def MIPRE.Introspection.AuxiliaryDecision.formatBranch {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} (tag : Fin 4) : Cost.PolyTimeFun (Input P ℓ) Bool

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.format {P : Type u_1} [Fintype P] [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) Bool

Equations

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

theorem MIPRE.Introspection.AuxiliaryDecision.format_apply {P : Type u_1} [Fintype P] [Cost.SizedEncoding P] {ℓ : ℕ} (x : Input P ℓ) : format.toFun x = match leftType.toFun x with | Sum.inl val => true | Sum.inr (AuxType.introspect, snd) => decide (AnswerParser.pairValid (width.toFun x) (originalBound.toFun x) (leftBits.toFun x)) | Sum.inr (AuxType.sample, snd) => decide (AnswerParser.pairValid (width.toFun x) (originalBound.toFun x) (leftBits.toFun x)) | Sum.inr (AuxType.read, snd) => decide (AnswerParser.tripleValid (width.toFun x) (originalBound.toFun x) false (leftBits.toFun x)) | Sum.inr (AuxType.hide k, snd) => decide (AnswerParser.tripleValid (width.toFun x) (width.toFun x) true (leftBits.toFun x))

noncomputable def MIPRE.Introspection.AuxiliaryDecision.contextWith {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} (role : Cost.PolyTimeFun (Input P ℓ) Bool) : Cost.PolyTimeFun (Input P ℓ) AuxiliarySource.Context

Replace the player's role while retaining the common clock and source.

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.guardFields {P : Type u_1} [Cost.SizedEncoding P] {ℓ : ℕ} : Cost.PolyTimeFun (Input P ℓ) SourceCompiler.GuardInput

Equations

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

def MIPRE.Introspection.AuxiliaryDecision.route {P : Type u_1} [DecidableEq P] {ℓ : ℕ} (X Z : P) : QuestionType P ℓ × QuestionType P ℓ → Fin 8 × Bool × Option (Fin ℓ)

Each directed auxiliary edge has one rule, a role and an optional hiding level.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.AuxiliaryDecision.route X Z (Sum.inl p, Sum.inr (MIPRE.Introspection.AuxType.sample, w)) = if p = Z then (0, w, none) else (7, w, none)
• MIPRE.Introspection.AuxiliaryDecision.route X Z (Sum.inl p, Sum.inr (MIPRE.Introspection.AuxType.hide k, w)) = if p = X ∧ ↑k = 0 then (5, w, none) else (7, w, none)
• MIPRE.Introspection.AuxiliaryDecision.route X Z (Sum.inr (MIPRE.Introspection.AuxType.introspect, false), Sum.inr (MIPRE.Introspection.AuxType.introspect, true)) = (6, false, none)
• MIPRE.Introspection.AuxiliaryDecision.route X Z x✝ = (7, false, none)

noncomputable def MIPRE.Introspection.AuxiliaryDecision.metadata {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {ℓ : ℕ} (X Z : P) : Cost.PolyTimeFun (Input P ℓ) (Fin 8 × Bool × Option (Fin ℓ))

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.sourceContext {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {ℓ : ℕ} (X Z : P) : Cost.PolyTimeFun (Input P ℓ) AuxiliarySource.Context

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.nextBranch {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {ℓ : ℕ} (U : Cost.ClockedUniversalMachine) (X Z : P) (k : Option (Fin ℓ)) : Cost.PolyTimeFun (Input P ℓ) Bool

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.AuxiliaryDecision.nextBranch U X Z none = MIPRE.Cost.PolyTimeFun.const true

noncomputable def MIPRE.Introspection.AuxiliaryDecision.branch {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {ℓ : ℕ} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P ℓ) Cost.BitStr) (tag : Fin 8) : Cost.PolyTimeFun (Input P ℓ) Bool

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.directed {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {ℓ : ℕ} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P ℓ) Cost.BitStr) : Cost.PolyTimeFun (Input P ℓ) Bool

The complete directed auxiliary program, including the source game call.

Equations

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

theorem MIPRE.Introspection.AuxiliaryDecision.directed_apply {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {ℓ : ℕ} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P ℓ) Cost.BitStr) (x : Input P ℓ) : (directed U X Z project).toFun x = (branch U X Z project (route X Z (leftType.toFun x, rightType.toFun x)).1).toFun x

noncomputable def MIPRE.Introspection.AuxiliaryDecision.check {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {ℓ : ℕ} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P ℓ) Cost.BitStr) : Cost.PolyTimeFun (Input P ℓ) Bool

Both orientations and exact same-type byte consistency are checked. The Pauli predicate and its format checks are conjoined by the caller.

Equations

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

theorem MIPRE.Introspection.AuxiliaryDecision.check_iff {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {ℓ : ℕ} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P ℓ) Cost.BitStr) (x : Input P ℓ) : (check U X Z project).toFun x = true ↔ format.toFun x = true ∧ format.toFun (swap.toFun x) = true ∧ (leftType.toFun x = rightType.toFun x → leftBits.toFun x = rightBits.toFun x) ∧ (directed U X Z project).toFun x = true ∧ (directed U X Z project).toFun (swap.toFun x) = true