Documentation

MIPRE.Background.Tailored.Intro.HonestChain

The honest strategy of the introspection verifier, explicitly #

The completeness of the introspection compiler MIPRE.Introspection.seven (CanonicalComplete.output_hasPerfectPCC) is proved through a chain of existential statements: the input's strategy is carried to the padded source game (VerifierSource.padded_hasPerfectPCC), the honest binary strategy is built on it and carried back to the canonical coordinates (NumberedComplete.exists_perfectPCC_with_format), its answers are encoded (CanonicalComplete.exists_raw_perfectPCC), and the typed strategy is detyped (DeciderProgram.exists_ambientPerfectPCC). Phase 3c of planning/aldous-lyons-track.md needs the measurement at each question as an explicit formula, so this file restates the chain as definitions, each the construction the existential statement wraps, with its PCC property and its value:

source, padded: the input's strategy on the source game and on the padded source game;
canonical: the honest strategy of the guarded game at the canonical parameters;
raw: its answers encoded, a strategy of the typed game rawGame;
honest: the detyped strategy, of the game H whose predicate is Detyping.accepts of rawPredicate.

The input is any perfect PCC strategy of the input verifier's game at index 2^n.

theorem MIPRE.Tailored.Intro.HonestChain.power_neZero (c lam n : ℕ) :

NeZero (Introspection.SourceCompiler.registerPower c lam n)

theorem MIPRE.Tailored.Intro.HonestChain.dim_le (W : Verifier 7) {lam n : ℕ} (c : ℕ) (hc : 2 ≤ c) (hW : W.IsBounded lam) (hn : 1 ≤ n) :

W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n

The register bound of the input.

The input on the source games #

noncomputable def MIPRE.Tailored.Intro.HonestChain.source (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) :

SyncStrategy (Introspection.Honest.sourceGame (Introspection.SourcePadding.Program.sourceFamily W n) (Introspection.VerifierSource.predicate W n ((2 ^ n) ^ lam))).doubled

The input's strategy, on the source game (the same game, presented by its CL family).

Equations

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

Instances For

theorem MIPRE.Tailored.Intro.HonestChain.source_isPCC (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hRW : RW.IsPCC) :

(source W RW).IsPCC

theorem MIPRE.Tailored.Intro.HonestChain.source_value (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hv : RW.value = 1) :

(source W RW).value = 1

noncomputable def MIPRE.Tailored.Intro.HonestChain.padded {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) :

SyncStrategy (Introspection.Honest.sourceGame (Introspection.AuxiliaryDecision.padded W hs) (Introspection.VerifierSource.paddedPredicate W hs ((2 ^ n) ^ lam))).doubled

The input's strategy on the padded source game, measuring at the unpadded question.

Equations

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

Instances For

theorem MIPRE.Tailored.Intro.HonestChain.padded_game_eq {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) :

Introspection.Honest.sourceGame (Introspection.AuxiliaryDecision.padded W hs) (Introspection.VerifierSource.paddedPredicate W hs ((2 ^ n) ^ lam)) = Introspection.Honest.sourceGame (Introspection.SourcePadding.family (Introspection.AuxiliaryProgram.firstEmbedding hs) (Introspection.SourcePadding.Program.sourceFamily W n)) (Introspection.SourcePadding.decider (Introspection.AuxiliaryProgram.firstEmbedding hs) (Introspection.VerifierSource.predicate W n ((2 ^ n) ^ lam)))

theorem MIPRE.Tailored.Intro.HonestChain.padded_isPCC {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (hRW : RW.IsPCC) :

(padded W RW hs).IsPCC

theorem MIPRE.Tailored.Intro.HonestChain.padded_value {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (hRW : RW.IsPCC) (hv : RW.value = 1) :

(padded W RW hs).value = 1

The honest strategy of the guarded game #

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.HonestChain.family {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) :

Bool → CL.CLFun CL.𝔽₂ (Introspection.BinaryComplete.Coord (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) 7

The source family in the binary Weyl coordinates.

Equations

MIPRE.Tailored.Intro.HonestChain.family W hs = MIPRE.Introspection.SourceReindex.family (MIPRE.Introspection.CanonicalGame.numbering c lam n) (MIPRE.Introspection.AuxiliaryDecision.padded W hs)

Instances For

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.HonestChain.decider {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (x y : (Fin (Introspection.SourceCompiler.registerPower c lam n) → Bool) × Fin (Introspection.SourceCompiler.fieldBits c lam n) → CL.𝔽₂) :

Verifier.Answers ((2 ^ n) ^ lam) → Verifier.Answers ((2 ^ n) ^ lam) → Bool

The source predicate in the binary Weyl coordinates.

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.HonestChain.reindexed {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) :

SyncStrategy (Introspection.Honest.sourceGame (Introspection.SourceReindex.family (Introspection.CanonicalGame.numbering c lam n) (Introspection.AuxiliaryDecision.padded W hs)) (Introspection.SourceReindex.decider (Introspection.CanonicalGame.numbering c lam n) (Introspection.VerifierSource.paddedPredicate W hs ((2 ^ n) ^ lam)))).doubled

The input's strategy in the binary Weyl coordinates.

Equations

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

Instances For

theorem MIPRE.Tailored.Intro.HonestChain.family_supported {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (w : Bool) :

(family W hs w).SupportedOn Finset.univ

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.HonestChain.binary {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) :

SyncStrategy (Introspection.BinaryComplete.game (family W hs) (decider W hs) ⋯ (Introspection.CanonicalGame.basis c he lam n)).doubled

The honest binary strategy (BinaryComplete.strategy), at the canonical parameters.

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.HonestChain.quotient {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) :

SyncStrategy (Introspection.AuxiliaryQuotient.reindexedGame (Introspection.CanonicalGame.numbering c lam n) QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (QLD.PauliCL.ExplicitSeed.binaryPresentation (Introspection.CanonicalGame.selector c hc1 lam n) (Introspection.CanonicalGame.basis c he lam n)) (Introspection.AuxiliaryDecision.padded W hs) (Introspection.NumberedComplete.project (Introspection.CanonicalGame.numbering c lam n) (Introspection.CanonicalGame.basis c he lam n)) (Introspection.VerifierSource.paddedPredicate W hs ((2 ^ n) ^ lam)) (Introspection.ExplicitGame.pauliCheck ⋯ (Introspection.CanonicalGame.permutation c lam n) (Introspection.CanonicalGame.basis c he lam n))).doubled

The honest strategy of the quotient game in the binary Weyl coordinates.

Equations

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

Instances For

noncomputable def MIPRE.Tailored.Intro.HonestChain.canonical {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) :

SyncStrategy (Introspection.CanonicalGame.guarded c hc1 he lam n W hs).doubled

The honest strategy of the guarded game, the strategy of CanonicalGame.exists_perfectPCC.

Equations

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

Instances For

theorem MIPRE.Tailored.Intro.HonestChain.quotient_game_eq {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) :

Introspection.AuxiliaryQuotient.reindexedGame (Introspection.CanonicalGame.numbering c lam n) QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (QLD.PauliCL.ExplicitSeed.binaryPresentation (Introspection.CanonicalGame.selector c hc1 lam n) (Introspection.CanonicalGame.basis c he lam n)) (Introspection.AuxiliaryDecision.padded W hs) (Introspection.NumberedComplete.project (Introspection.CanonicalGame.numbering c lam n) (Introspection.CanonicalGame.basis c he lam n)) (Introspection.VerifierSource.paddedPredicate W hs ((2 ^ n) ^ lam)) (Introspection.ExplicitGame.pauliCheck ⋯ (Introspection.CanonicalGame.permutation c lam n) (Introspection.CanonicalGame.basis c he lam n)) = Introspection.BinaryComplete.explicitQuotientGame (family W hs) (decider W hs) ⋯ (Introspection.CanonicalGame.basis c he lam n) (Introspection.CanonicalGame.selector c hc1 lam n) (Introspection.CanonicalGame.permutation c lam n)

theorem MIPRE.Tailored.Intro.HonestChain.quotient_isPCC {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (hRW : RW.IsPCC) :

(quotient W RW hc1 he hs).IsPCC

theorem MIPRE.Tailored.Intro.HonestChain.quotient_value {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (hRW : RW.IsPCC) (hv : RW.value = 1) :

(quotient W RW hc1 he hs).value = 1

theorem MIPRE.Tailored.Intro.HonestChain.canonical_prefixGuard {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (q : Bool × CL.Detyping.Question Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n))) (a : Introspection.CanonicalComplete.Answer c lam n) (ha : (canonical W RW hc1 he hs).P.M q a ≠ 0) :

Introspection.PrefixGuard.holds (Introspection.AuxiliaryDecision.padded W hs) q.2.1 a

theorem MIPRE.Tailored.Intro.HonestChain.canonical_isPCC {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (hRW : RW.IsPCC) :

(canonical W RW hc1 he hs).IsPCC

theorem MIPRE.Tailored.Intro.HonestChain.canonical_value {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (hRW : RW.IsPCC) (hv : RW.value = 1) :

(canonical W RW hc1 he hs).value = 1

theorem MIPRE.Tailored.Intro.HonestChain.quotient_introspect {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (side w : Bool) (payload : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) (a : Verifier.Answers ((2 ^ n) ^ lam)) (ha : (quotient W RW hc1 he hs).P.M (side, Sum.inr (Introspection.AuxType.introspect , w), payload) (Introspection.ParsedAnswer.pair y a) ≠ 0) :

∃ (x : Introspection.BinaryComplete.Coord (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n) → CL.𝔽₂), (family W hs w).eval x = y

theorem MIPRE.Tailored.Intro.HonestChain.canonical_introspect {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (side w : Bool) (payload : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (y : Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂) (a : Verifier.Answers ((2 ^ n) ^ lam)) (ha : (canonical W RW hc1 he hs).P.M (side, Sum.inr (Introspection.AuxType.introspect , w), payload) (Introspection.ParsedAnswer.pair y a) ≠ 0) :

∃ (x : Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂), (Introspection.AuxiliaryDecision.padded W hs w).eval x = y

theorem MIPRE.Tailored.Intro.HonestChain.quotient_pauli_format {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (side : Bool) (t : QLD.Ty) (payload : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (a : QLD.Answer (Introspection.CanonicalGame.field c lam n).carrier (Introspection.SourceCompiler.registerPower c lam n) 1) (ha : (quotient W RW hc1 he hs).P.M (side, Sum.inl t, payload) (Introspection.ParsedAnswer.pauli a) ≠ 0) :

(QLD.PauliCL.ExplicitSeed.binaryDecode (Introspection.CanonicalGame.permutation c lam n) (Introspection.CanonicalGame.basis c he lam n) t payload).fmtOk a = true

theorem MIPRE.Tailored.Intro.HonestChain.canonical_pauli_format {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (side : Bool) (t : QLD.Ty) (payload : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (a : QLD.Answer (Introspection.CanonicalGame.field c lam n).carrier (Introspection.SourceCompiler.registerPower c lam n) 1) (ha : (canonical W RW hc1 he hs).P.M (side, Sum.inl t, payload) (Introspection.ParsedAnswer.pauli a) ≠ 0) :

(QLD.PauliCL.ExplicitSeed.binaryDecode (Introspection.CanonicalGame.permutation c lam n) (Introspection.CanonicalGame.basis c he lam n) t payload).fmtOk a = true

The encoded and detyped strategies #

theorem MIPRE.Tailored.Intro.HonestChain.one_le_c {c : ℕ} (hc : 2 ≤ c) :

1 ≤ c

noncomputable def MIPRE.Tailored.Intro.HonestChain.raw {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (hW : W.IsBounded lam) (hn : 1 ≤ n) :

SyncStrategy (Introspection.DecisionCompiler.rawGame c ⋯ he U (W.sampler.prog, W.decider.prog) lam n).doubled

The honest strategy of the typed game: the honest strategy of the guarded game, its answers encoded as bit strings (CanonicalComplete.encodeAnswer).

Equations

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

Instances For

theorem MIPRE.Tailored.Intro.HonestChain.raw_isPCC {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (hW : W.IsBounded lam) (hn : 1 ≤ n) (hRW : RW.IsPCC) :

(raw W RW hc he U hW hn).IsPCC

theorem MIPRE.Tailored.Intro.HonestChain.raw_value {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (hW : W.IsBounded lam) (hn : 1 ≤ n) (hRW : RW.IsPCC) (hv : RW.value = 1) :

(raw W RW hc he U hW hn).value = 1

def MIPRE.Tailored.Intro.HonestChain.answer₀ {c lam n : ℕ} :

Verifier.Answers (Introspection.DecisionCompiler.outerBound c lam n)

The constant answer off the decodable views.

Equations

MIPRE.Tailored.Intro.HonestChain.answer₀ = ⟨[], ⋯⟩

Instances For

noncomputable def MIPRE.Tailored.Intro.HonestChain.honest {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (hW : W.IsBounded lam) (hn : 1 ≤ n) :

SyncStrategy (CL.Detyping.game Introspection.DecisionCompiler.graph (CL.Detyping.DeciderProgram.sourceFamily (Introspection.DecisionCompiler.extendedSampler c ⋯ he lam) n) (Introspection.DecisionCompiler.rawPredicate c ⋯ he U (W.sampler.prog, W.decider.prog) lam n)).doubled

The honest strategy of the detyped game H of the introspection verifier (Detyping.complete of raw, the constant answer [] off the decodable views).

Equations

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

Instances For

theorem MIPRE.Tailored.Intro.HonestChain.honest_isPCC {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (hW : W.IsBounded lam) (hn : 1 ≤ n) (hRW : RW.IsPCC) :

(honest W RW hc he U hW hn).IsPCC

theorem MIPRE.Tailored.Intro.HonestChain.honest_value {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (hW : W.IsBounded lam) (hn : 1 ≤ n) (hRW : RW.IsPCC) (hv : RW.value = 1) :

(honest W RW hc he U hW hn).value = 1