Completeness of the output tailored verifier, in the contract's form

Phase 3c of planning/aldous-lyons-track.md (issue #281), the counterpart of Output.soundness_contract. For a λ-bounded tailored verifier T with a perfect ZPC strategy at index 2^n, whose normal form verifier T.ofTNFVT U0 is Cλ-bounded (C ≥ 2), the output tailored verifier at Cλ has a perfect ZPC strategy at index n as soon as its programs meet the specification IntroSpec.

The strategy is the honest strategy of the reference verifier's typed game (HonestChain.honest_zpc_ofTNFVT), which meets the three conditions of Complete.hasPerfectZPC_tpresented; Output.hasPerfectZPC_outTV carries it to the output. The input's answers fit the cutoff (2^n)^(Cλ) by the length bound of a λ-bounded verifier (Output.maxLen_le_of_isBounded).

theorem MIPRE.Tailored.Intro.Output.completeness_contract (T : TailoredVerifier 7) (U0 : Cost.UniversalMachine) {C lam n : ℕ} (hC : 2 ≤ C) (hl : 1 ≤ lam) (hn : 1 ≤ n) (hT : T.IsBounded lam) (hV : (T.ofTNFVT U0).IsBounded (C * lam)) {hs : (T.ofTNFVT U0).sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits Introspection.sevenConstant (C * lam) n} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits Introspection.sevenConstant (C * lam) n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits Introspection.sevenConstant (C * lam) n) → CL.𝔽₂)} {L P : Decider} (hkg : KerGens (Introspection.SourceCompiler.registerBits Introspection.sevenConstant (C * lam) n) kg) {hl' : 1 ≤ C * lam} (h : IntroSpec Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ Cost.selfClockedUniversal (T.ofTNFVT U0) hl' hn (presented Introspection.DecisionCompiler.graph (Sound.H Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ (C * lam) n Cost.selfClockedUniversal (T.ofTNFVT U0)) (Sound.tdata Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ (C * lam) n T (T.ofTNFVT U0) hs kg)) L P) (hZ : T.HasPerfectZPC (2 ^ n)) : (outTV Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ (C * lam) L P).HasPerfectZPC n

Completeness of the output, in the contract's form: for a λ-bounded input T with a perfect ZPC strategy at index 2^n, whose normal form verifier is Cλ-bounded (C ≥ 2), when the output's programs meet the specification at Cλ, the output's n-th game has a perfect ZPC strategy.