Source semantics of the assembled auxiliary branches

The runtime context is instantiated with the existing bounded source verifier. Every factor and matrix is obtained from its actual clocked sampler, only at prefixes certified by the scan.

def MIPRE.Introspection.AuxiliaryDecision.canonical {P : Type u_1} (V : Verifier 7) (lam n Q R : ℕ) (parameters : Parameters) (t u : QuestionType P 7) (a b : Cost.BitStr) : Input P 7

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryDecision.padded {n Q : ℕ} (V : Verifier 7) (hQ : V.sampler.dim (2 ^ n) ≤ Q) : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7

Equations

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

theorem MIPRE.Introspection.AuxiliaryDecision.padded_supported {n Q : ℕ} (V : Verifier 7) (hQ : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) : (padded V hQ w).SupportedOn Finset.univ

theorem MIPRE.Introspection.AuxiliaryDecision.directed_canonical {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) (V : Verifier 7) (lam n Q R : ℕ) (t u : QuestionType P 7) (a b : Cost.BitStr) : (directed U X Z project).toFun (canonical V lam n Q R parameters t u a b) = (branch U X Z project (route X Z (t, u)).1).toFun (canonical V lam n Q R parameters t u a b)

theorem MIPRE.Introspection.AuxiliaryDecision.directed_z_sample {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) (V : Verifier 7) (lam n Q R : ℕ) (w : Bool) (a : Cost.BitStr) (z : Fin Q → CL.𝔽₂) (b : Cost.BitStr) : have x := canonical V lam n Q R parameters (Sum.inl Z) (Sum.inr (AuxType.sample, w)) a (AnswerParser.pairBits (CL.toBits z) b); (directed U X Z project).toFun x = true ↔ project.toFun x = CL.toBits z

The Z/Sample edge compares the full register, including padding coordinates.

theorem MIPRE.Introspection.AuxiliaryDecision.directed_sampling {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) {lam n Q R : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (hQ : 4 ≤ Q) (hR : 3 * R ≤ Q) (w : Bool) (y z : Fin Q → CL.𝔽₂) (a b : Cost.BitStr) : (directed U X Z project).toFun (canonical V lam n Q R parameters (Sum.inr (AuxType.introspect, w)) (Sum.inr (AuxType.sample, w)) (AnswerParser.pairBits (CL.toBits y) a) (AnswerParser.pairBits (CL.toBits z) b)) = true ↔ List.length a ≤ R ∧ List.length b ≤ R ∧ CLChecks.sampling (padded V hs w) (y, a) (z, b)

The actual source Sample call enforces the full padded CL relation.

theorem MIPRE.Introspection.AuxiliaryDecision.directed_reading {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) (V : Verifier 7) (lam n : ℕ) {Q R : ℕ} (hQ : 4 ≤ Q) (hR : 3 * R ≤ Q) (w : Bool) (y z zp : Fin Q → CL.𝔽₂) (a b : Cost.BitStr) : (directed U X Z project).toFun (canonical V lam n Q R parameters (Sum.inr (AuxType.introspect, w)) (Sum.inr (AuxType.read, w)) (AnswerParser.pairBits (CL.toBits y) a) (AnswerParser.tripleBits (CL.toBits z) (CL.toBits zp) b)) = true ↔ List.length a ≤ R ∧ List.length b ≤ R ∧ CLChecks.reading (y, a) (z, zp, b)

Introspect/Read retains the ordinary answer cutoff and full-register question.

theorem MIPRE.Introspection.AuxiliaryDecision.directed_first {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) {lam n Q R : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (x y yp z : Fin Q → CL.𝔽₂) (a : Cost.BitStr) (hp : project.toFun (canonical V lam n Q R parameters (Sum.inl X) (Sum.inr (AuxType.hide 0, w)) a (AnswerParser.tripleBits (CL.toBits y) (CL.toBits yp) (CL.toBits z))) = CL.toBits x) : (directed U X Z project).toFun (canonical V lam n Q R parameters (Sum.inl X) (Sum.inr (AuxType.hide 0, w)) a (AnswerParser.tripleBits (CL.toBits y) (CL.toBits yp) (CL.toBits z))) = true ↔ AuxiliaryQuotient.hidingPauli (padded V hs w) x (y, yp, z)

The first hiding edge uses the actual source's initial dual quotient.

theorem MIPRE.Introspection.AuxiliaryDecision.directed_next {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) {lam n Q R : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (k j : Fin 7) (hk : ↑k + 1 = ↑j) (y yp x z zp t : Fin Q → CL.𝔽₂) : (directed U X Z project).toFun (canonical V lam n Q R parameters (Sum.inr (AuxType.hide k, w)) (Sum.inr (AuxType.hide j, w)) (AnswerParser.tripleBits (CL.toBits y) (CL.toBits yp) (CL.toBits x)) (AnswerParser.tripleBits (CL.toBits z) (CL.toBits zp) (CL.toBits t))) = true ↔ (∃ (a : Fin Q → CL.𝔽₂), (CL.CLFun.truncate (↑k) (padded V hs w)).eval a = (padded V hs w).outputPrefix (↑k) y) ∧ (∃ (a : Fin Q → CL.𝔽₂), (CL.CLFun.truncate (↑k + 1) (padded V hs w)).eval a = (padded V hs w).outputPrefix (↑k + 1) z) ∧ AuxiliaryQuotient.hidingNext (padded V hs w) ↑k (y, yp, x) (z, zp, t)

The interior hiding edge is exactly the quotient comparison together with its two legally queried prefix conditions.

theorem MIPRE.Introspection.AuxiliaryDecision.directed_last {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) {lam n Q R : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (k : Fin 7) (hk : ↑k + 1 = 7) (y yp x z zp : Fin Q → CL.𝔽₂) (a : Cost.BitStr) : (directed U X Z project).toFun (canonical V lam n Q R parameters (Sum.inr (AuxType.hide k, w)) (Sum.inr (AuxType.read, w)) (AnswerParser.tripleBits (CL.toBits y) (CL.toBits yp) (CL.toBits x)) (AnswerParser.tripleBits (CL.toBits z) (CL.toBits zp) a)) = true ↔ (∃ (b : Fin Q → CL.𝔽₂), (CL.CLFun.truncate 6 (padded V hs w)).eval b = (padded V hs w).outputPrefix 6 y) ∧ (∃ (b : Fin Q → CL.𝔽₂), (CL.CLFun.truncate 6 (padded V hs w)).eval b = (padded V hs w).outputPrefix 6 z) ∧ CLChecks.hidingRead (padded V hs w) (y, yp, x) (z, zp, a)

The terminal hiding edge compares the penultimate prefixes and full dual labels.

theorem MIPRE.Introspection.AuxiliaryDecision.directed_cross {P : Type u_1} [Fintype P] [DecidableEq P] [Cost.SizedEncoding P] {parameters : Parameters} (U : Cost.ClockedUniversalMachine) (X Z : P) (project : Cost.PolyTimeFun (Input P 7) Cost.BitStr) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (a b : Cost.BitStr) : have g := (2 ^ n, Q, (2 ^ n) ^ lam, V.sampler.dim (2 ^ n), a, b); (directed U X Z project).toFun (canonical V lam n Q ((2 ^ n) ^ lam) parameters (Sum.inr (AuxType.introspect, false)) (Sum.inr (AuxType.introspect, true)) a b) = true ↔ SourceCompiler.GuardReady g ∧ V.decider.Accepts (2 ^ n) (List.take (V.sampler.dim (2 ^ n)) (SourceCompiler.leftParts.toFun g).1) (List.take (V.sampler.dim (2 ^ n)) (SourceCompiler.rightParts.toFun g).1) (SourceCompiler.leftParts.toFun g).2 (SourceCompiler.rightParts.toFun g).2

The cross-Introspect branch runs the original decision program after the full source-membership and original-answer guards.