The actual bounded source supplies every hiding-scan query

The seven source levels have three-bit indices. The common source clock therefore covers all matrix and factor queries at every attained prefix. This instantiates the generic scan interface with the executable padded source programs, without assuming any source-query oracle.

theorem MIPRE.Introspection.AuxiliarySourceScan.level_size_le {lam n j : ℕ} (hlam : 2 ≤ lam) (hn : 1 ≤ n) (hj : j < 7) : (j + 1).size ≤ (2 ^ n) ^ lam

theorem MIPRE.Introspection.AuxiliarySourceScan.queriesCorrectAt (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hQ : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (initialLevel : ℕ) (initial : Fin Q → CL.𝔽₂) (j : ℕ) (hj : j < 7) : AuxiliaryScan.QueriesCorrectAt (SourcePadding.Program.factorFromContext U) (SourcePadding.Program.matrixFromContext U) (SourcePadding.Program.queryContext V lam n w initialLevel initial) (SourcePadding.depthFamily (AuxiliaryProgram.firstEmbedding hQ) (SourcePadding.Program.sourceFamily V n) w) j

Any initial context prefix and level are replaced before the queried stage. Only its fixed source, clock, index and player matter.

theorem MIPRE.Introspection.AuxiliarySourceScan.queriesCorrectBelow (U : Cost.ClockedUniversalMachine) {lam n Q : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hQ : V.sampler.dim (2 ^ n) ≤ Q) (w : Bool) (initialLevel : ℕ) (initial : Fin Q → CL.𝔽₂) (k : ℕ) (hk : k ≤ 7) (j : ℕ) : j < k → AuxiliaryScan.QueriesCorrectAt (SourcePadding.Program.factorFromContext U) (SourcePadding.Program.matrixFromContext U) (SourcePadding.Program.queryContext V lam n w initialLevel initial) (SourcePadding.depthFamily (AuxiliaryProgram.firstEmbedding hQ) (SourcePadding.Program.sourceFamily V n) w) j