GapCVP proof, part 04, continuation 04

noncomputable def GapCVP.OutputPolynomialCompositionClosure.markerConditionalTrueTrace {valid : List Bool → List Bool} (computer : BitTM valid) (fallback input : List Bool) : StateTransition.EvalsToInTime (markerConditionalMachine computer fallback).step (Turing.initList (markerConditionalMachine computer fallback) (computer.inputAlphabet.invFun true :: List.map computer.inputAlphabet.invFun input)) (some (Turing.haltList (markerConditionalMachine computer fallback) (List.map computer.outputAlphabet.invFun (valid input)))) (Polynomial.eval input.length computer.time + 1)

Execute the supplied computer when the input begins with a true marker.

Equations

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

noncomputable def GapCVP.OutputPolynomialCompositionClosure.markerConditionalFalseTrace {valid : List Bool → List Bool} (computer : BitTM valid) (fallback input : List Bool) : StateTransition.EvalsToInTime (markerConditionalMachine computer fallback).step (Turing.initList (markerConditionalMachine computer fallback) (computer.inputAlphabet.invFun false :: List.map computer.inputAlphabet.invFun input)) (some (Turing.haltList (markerConditionalMachine computer fallback) (List.map computer.outputAlphabet.invFun fallback))) (input.length + 2)

Return the fallback word when the input begins with a false marker.

Equations

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

noncomputable def GapCVP.OutputPolynomialCompositionClosure.markerConditionalMissingTrace {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) : StateTransition.EvalsToInTime (markerConditionalMachine computer fallback).step (Turing.initList (markerConditionalMachine computer fallback) []) (some (Turing.haltList (markerConditionalMachine computer fallback) (List.map computer.outputAlphabet.invFun fallback))) 2

Return the fallback word in two steps when the input has no marker.

Equations

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

noncomputable def GapCVP.OutputPolynomialCompositionClosure.markerConditionalTotalTrace {valid : List Bool → List Bool} (computer : BitTM valid) (fallback input : List Bool) : StateTransition.EvalsToInTime (markerConditionalMachine computer fallback).step (Turing.initList (markerConditionalMachine computer fallback) (List.map computer.inputAlphabet.invFun input)) (some (Turing.haltList (markerConditionalMachine computer fallback) (List.map computer.outputAlphabet.invFun (markerConditionalOutput valid fallback input)))) (Polynomial.eval input.length (computer.time + Polynomial.X + 3))

A time-bounded execution of the marker-controlled choice for every input.

Equations

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

noncomputable def GapCVP.OutputPolynomialCompositionClosure.markerConditionalComputable {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) : BitTM (markerConditionalOutput valid fallback)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.OutputPolynomialCompositionClosure.sourcePreservingConditionalComputable {selector : List Bool → Bool} {valid : List Bool → List Bool} (selection : BitTM fun (input : List Bool) => selector input :: input) (computer : BitTM valid) (fallback : List Bool) : BitTM fun (input : List Bool) => if selector input = true then valid input else fallback

GapCVP reduction support.

Equations

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

def GapCVP.CNFBoundedRecordFoldTM.actualWindowIndexEquiv (T : ℕ) : CL.Window T ≃ Fin T × CL.Position T

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFBoundedRecordFoldTM.totalAtMostOneFamilyClauses (T S : ℕ) : List (CL.Clause T S)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFBoundedRecordFoldTM.totalForbiddenTransitionFamilyClauses {T S : ℕ} (specification : CL.Specification T S) : List (CL.Clause T S)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFBoundedRecordFoldTM.totalFiveFamilySourceClauseCandidates {T S : ℕ} (specification : CL.Specification T S) : List (CL.Clause T S)

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFBoundedRecordFoldTM.totalFiveFamilySourceClauseCandidates_toFinset {T S : ℕ} (specification : CL.Specification T S) : (totalFiveFamilySourceClauseCandidates specification).toFinset = CL.tableauFormula specification

noncomputable def GapCVP.CNFBoundedRecordFoldTM.totalVerifierFiveFamilySourceClauseCandidates (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (input : List Bool) : List (CL.Clause (Polynomial.eval input.length (CLStructuralWholeCNFOutputTM.paddedStructuralTableauSimulation bound machine).time) (CLStructuralWholeCNFOutputTM.paddedStructuralTableauSimulation bound machine).symbols)

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFBoundedRecordFoldTM.totalVerifierFiveFamilySourceClauseCandidates_sorted (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (input : List Bool) : CNFFiniteRecordSort.sourceOrderedDistinctRecords (totalVerifierFiveFamilySourceClauseCandidates bound machine input) = CLStructuralWholeCNFOutputTM.structuralWholeSourceClauses bound machine input

theorem GapCVP.CNFBoundedRecordFoldTM.encodeThreeCNF_totalVerifierFiveFamilies (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (input : List Bool) : BinaryEncoding.encodeThreeCNF (ThreeCNFReduction.encodeFormulaFrom 0 (CNFFiniteRecordSort.sourceOrderedDistinctRecords (totalVerifierFiveFamilySourceClauseCandidates bound machine input))) = CLStructuralWholeCNFOutputTM.structuralWholeCNFWord bound machine input

Internal support shared across GapCVP continuation modules.

noncomputable def GapCVP.CNFBoundedRecordFoldTM.polynomialValueUnaryComputable (polynomial : Polynomial ℕ) : BitTM fun (input : List Bool) => List.replicate (Polynomial.eval input.length polynomial) true

GapCVP reduction support.

Equations

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

def GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFold : List Bool → Option (ℕ × List Bool)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFold [] = none
• GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFold (false :: remaining) = some (0, remaining)

def GapCVP.OutputBoundedDependentRecordFold.unaryBoundedFoldWord (count : ℕ) (seed : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.OutputBoundedDependentRecordFold.unaryBoundedFoldWord count seed = List.replicate count true ++ false :: seed

@[simp]

theorem GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFold_word (count : ℕ) (seed : List Bool) : parseUnaryBoundedFold (unaryBoundedFoldWord count seed) = some (count, seed)

def GapCVP.OutputBoundedDependentRecordFold.boundedRecordFoldOutput (worker : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.OutputBoundedDependentRecordFold.parsedUnaryFold_count_le_length (input : List Bool) (count : ℕ) (seed : List Bool) (hparse : parseUnaryBoundedFold input = some (count, seed)) : count ≤ input.length

noncomputable def GapCVP.OutputBoundedDependentRecordFold.PolynomiallyBoundedFoldStates (worker : List Bool → List Bool) (bound : Polynomial ℕ) : Bool

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.OutputBoundedDependentRecordFold.BoundedFoldStack (tm : Turing.FinTM2) : Type

Worker stacks extended by a Boolean counter stack and a Boolean scratch stack.

Equations

• GapCVP.OutputBoundedDependentRecordFold.BoundedFoldStack tm = (tm.K ⊕ Bool)

@[reducible, inline]

abbrev GapCVP.OutputBoundedDependentRecordFold.boundedFoldAlphabet (tm : Turing.FinTM2) : BoundedFoldStack tm → Type

Use the worker alphabets on worker stacks and bits on the two auxiliary stacks.

Equations

• GapCVP.OutputBoundedDependentRecordFold.boundedFoldAlphabet tm (Sum.inl k) = tm.Γ k
• GapCVP.OutputBoundedDependentRecordFold.boundedFoldAlphabet tm (Sum.inr val) = Bool

@[reducible, inline]

abbrev GapCVP.OutputBoundedDependentRecordFold.BoundedFoldLabel (tm : Turing.FinTM2) : Type

Worker labels extended by the five bounded-fold control phases.

Equations

• GapCVP.OutputBoundedDependentRecordFold.BoundedFoldLabel tm = (tm.Λ ⊕ Fin 5)

@[reducible, inline]

abbrev GapCVP.OutputBoundedDependentRecordFold.BoundedFoldState (tm : Turing.FinTM2) : Type

The worker state together with an optional bit used by the fold controller.

Equations

• GapCVP.OutputBoundedDependentRecordFold.BoundedFoldState tm = (Option Bool × tm.σ)

@[reducible, inline]

abbrev GapCVP.OutputBoundedDependentRecordFold.liftBoundedFoldWorkerStatement (tm : Turing.FinTM2) : Turing.TM2.Stmt (fun (k : tm.K) => boundedFoldAlphabet tm (Sum.inl k)) tm.Λ tm.σ → Turing.TM2.Stmt (boundedFoldAlphabet tm) (tm.Λ ⊕ Fin 5) (Option Bool × tm.σ)

Embed worker statements and return to fold phase two when the worker halts.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedDependentRecordFoldMachine {worker : List Bool → List Bool} (computer : BitTM worker) : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.OutputBoundedDependentRecordFold.boundedFoldStacks (tm : Turing.FinTM2) (sourceStacks : (k : tm.K) → List (tm.Γ k)) (counter scratch : List Bool) (k : BoundedFoldStack tm) : List (boundedFoldAlphabet tm k)

Combine the worker stacks with the fold counter and scratch contents.

Equations

• GapCVP.OutputBoundedDependentRecordFold.boundedFoldStacks tm sourceStacks counter scratch (Sum.inl k) = sourceStacks k
• GapCVP.OutputBoundedDependentRecordFold.boundedFoldStacks tm sourceStacks counter scratch (Sum.inr false) = counter
• GapCVP.OutputBoundedDependentRecordFold.boundedFoldStacks tm sourceStacks counter scratch (Sum.inr true) = scratch

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldPhaseConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (phase : Fin 5) (sourceStacks : (k : computer.tm.K) → List (computer.tm.Γ k)) (counter scratch : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

A controller-phase configuration with explicit worker and auxiliary stack contents.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldWorkerConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) (configuration : computer.tm.Cfg) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFoldWorkerConfiguration_step {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) (configuration next : computer.tm.Cfg) (hstep : computer.tm.step configuration = some next) : (boundedDependentRecordFoldMachine computer).step (boundedFoldWorkerConfiguration computer counter configuration) = some (boundedFoldWorkerConfiguration computer counter next)

Internal support shared across GapCVP continuation modules.

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldScanConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (remaining : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldDispatchConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldDrainConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (output : List (computer.tm.Γ computer.tm.k₁)) (counter scratch : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldRestoreConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) (counter scratch : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldMalformedConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFoldWorkerConfiguration_halt {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) (output : List (computer.tm.Γ computer.tm.k₁)) : boundedFoldWorkerConfiguration computer counter (Turing.haltList computer.tm output) = boundedFoldDrainConfiguration computer output counter []

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedDependentRecordFoldMachine_init {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) : Turing.initList (boundedDependentRecordFoldMachine computer) input = boundedFoldScanConfiguration computer input []

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_scan_true {worker : List Bool → List Bool} (computer : BitTM worker) (remaining : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldScanConfiguration computer (computer.inputAlphabet.invFun true :: remaining) counter) = some (boundedFoldScanConfiguration computer remaining (true :: counter))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_scan_delimiter {worker : List Bool → List Bool} (computer : BitTM worker) (remaining : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldScanConfiguration computer (computer.inputAlphabet.invFun false :: remaining) counter) = some (boundedFoldDispatchConfiguration computer remaining counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_scan_missing {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldScanConfiguration computer [] counter) = some (boundedFoldMalformedConfiguration computer counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_dispatch_step {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldDispatchConfiguration computer input (true :: counter)) = some (boundedFoldWorkerConfiguration computer counter (Turing.initList computer.tm input))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_dispatch_finish {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) : (boundedDependentRecordFoldMachine computer).step (boundedFoldDispatchConfiguration computer input []) = some (Turing.haltList (boundedDependentRecordFoldMachine computer) input)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_drain_step {worker : List Bool → List Bool} (computer : BitTM worker) (symbol : computer.tm.Γ computer.tm.k₁) (remaining : List (computer.tm.Γ computer.tm.k₁)) (counter scratch : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldDrainConfiguration computer (symbol :: remaining) counter scratch) = some (boundedFoldDrainConfiguration computer remaining counter (computer.outputAlphabet symbol :: scratch))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_drain_finish {worker : List Bool → List Bool} (computer : BitTM worker) (counter scratch : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldDrainConfiguration computer [] counter scratch) = some (boundedFoldRestoreConfiguration computer [] counter scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_restore_step {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) (bit : Bool) (scratch : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldRestoreConfiguration computer input counter (bit :: scratch)) = some (boundedFoldRestoreConfiguration computer (computer.inputAlphabet.invFun bit :: input) counter scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_restore_finish {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldRestoreConfiguration computer input counter []) = some (boundedFoldDispatchConfiguration computer input counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_malformed_step {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldMalformedConfiguration computer (true :: counter)) = some (boundedFoldMalformedConfiguration computer counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_malformed_finish {worker : List Bool → List Bool} (computer : BitTM worker) : (boundedDependentRecordFoldMachine computer).step (boundedFoldMalformedConfiguration computer []) = some (Turing.haltList (boundedDependentRecordFoldMachine computer) [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFTypedRecordWorkerTM.parsedUnaryFold_seed_length_le (raw : List Bool) (count : ℕ) (seed : List Bool) (hparse : OutputBoundedDependentRecordFold.parseUnaryBoundedFold raw = some (count, seed)) : seed.length ≤ raw.length

theorem GapCVP.CNFTypedRecordWorkerTM.acceptanceClause_exact_card {T S : ℕ} (accept : CL.Symbol S) : Finset.card (CL.acceptanceClause accept) = T + 1