GapCVP proof, part 04, continuation 03

def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerScanTrace (polynomial : Polynomial ℕ) (stage : CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial) (input source base baseScratch accumulator product output : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 0 stage input source base baseScratch accumulator product output) (some (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 1 stage [] (input.reverse ++ source) (List.replicate input.length true ++ base) baseScratch accumulator product output)) (input.length + 1)

Save the input and record its length as a unary base count.

Equations

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

def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerBaseTrace (polynomial : Polynomial ℕ) (stage : CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial) (baseCount : ℕ) (source baseScratch accumulator product output : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 2 stage [] source (List.replicate baseCount true) baseScratch accumulator product output) (some (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 3 stage [] source [] (List.replicate baseCount true ++ baseScratch) accumulator (List.replicate baseCount true ++ product) output)) (baseCount + 1)

Copy the unary base to scratch and add one base-sized block to the product.

Equations

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

def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerRestoreBaseTrace (polynomial : Polynomial ℕ) (stage : CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial) (scratchCount : ℕ) (source base accumulator product output : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 3 stage [] source base (List.replicate scratchCount true) accumulator product output) (some (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 1 stage [] source (List.replicate scratchCount true ++ base) [] accumulator product output)) (scratchCount + 1)

Restore the unary base from scratch for another multiplication cycle.

Equations

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

def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerMultiplyTrace (polynomial : Polynomial ℕ) (stage : CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial) (baseCount accumulatorCount productCount : ℕ) (source output : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 1 stage [] source (List.replicate baseCount true) [] (List.replicate accumulatorCount true) (List.replicate productCount true) output) (some (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 4 stage [] source (List.replicate baseCount true) [] [] (List.replicate (baseCount * accumulatorCount + productCount) true) output)) (accumulatorCount * (2 * baseCount + 3) + 1)

Multiply the unary accumulator by the unary input length.

Equations

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

def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerProductTrace (polynomial : Polynomial ℕ) (stage : CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial) (productCount : ℕ) (source base accumulator output : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 4 stage [] source base [] accumulator (List.replicate productCount true) output) (some (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 4 stage [] source base [] (List.replicate productCount true ++ accumulator) [] output)) productCount

Transfer the completed product into the accumulator.

Equations

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

def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerHornerCostPolynomial (polynomial : Polynomial ℕ) : ℕ → Polynomial ℕ → Polynomial ℕ

Bound the machine steps for the remaining Horner evaluation stages.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerHornerCostPolynomial polynomial 0 x✝ = 0

noncomputable def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerHornerTrace (polynomial : Polynomial ℕ) (baseCount stages : ℕ) (stage : CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial) (hstage : ↑stage + 1 = stages) (accumulatorPolynomial : Polynomial ℕ) (source output : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 1 stage [] source (List.replicate baseCount true) [] (List.replicate (Polynomial.eval baseCount accumulatorPolynomial) true) [] output) (some (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 5 0 [] source (List.replicate baseCount true) [] (List.replicate (CNFPolynomialRowMarkerTM.polynomialRowMarkerHorner polynomial baseCount stages (Polynomial.eval baseCount accumulatorPolynomial)) true) [] output)) (Polynomial.eval baseCount (polynomialRowMarkerHornerCostPolynomial polynomial stages accumulatorPolynomial))

Execute the remaining Horner stages of the marker polynomial.

Equations

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

def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerPayloadTrace (polynomial : Polynomial ℕ) (stage : CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial) (markerCount : ℕ) (source base product output : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 5 stage [] source base [] (List.replicate markerCount true) product output) (some (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 6 stage [] source base [] [] (List.replicate markerCount true ++ product) (false :: (List.replicate markerCount true ++ output)))) (markerCount + 1)

Copy the marker count into the product and encoded output payload.

Equations

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

def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerHeaderTrace (polynomial : Polynomial ℕ) (stage : CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial) (markerCount : ℕ) (source base output : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 6 stage [] source base [] [] (List.replicate markerCount true) output) (some (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 7 stage [] source base [] [] [] (List.replicate markerCount true ++ output))) (markerCount + 1)

Write the unary length header for the marker payload.

Equations

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

def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerSourceTrace (polynomial : Polynomial ℕ) (stage : CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial) (source base output : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 7 stage [] source base [] [] [] output) (some (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 8 stage [] [] base [] [] [] (false :: (source.reverse ++ output)))) (source.length + 1)

Copy the saved source word into output after a separator.

Equations

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

def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerPrefixTrace (polynomial : Polynomial ℕ) (stage : CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial) (baseCount : ℕ) (output : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 8 stage [] [] (List.replicate baseCount true) [] [] [] output) (some (Turing.haltList (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial) (List.replicate baseCount true ++ output))) (baseCount + 1)

Prefix the output with the unary base count and halt.

Equations

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

noncomputable def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerTotalTimePolynomial (polynomial : Polynomial ℕ) : Polynomial ℕ

Polynomial time bound for the complete row-marker machine.

Equations

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

noncomputable def GapCVP.CLStructuralCNFOutputMachinesUnconditional.polynomialRowMarkerTotalTrace (polynomial : Polynomial ℕ) (input : List Bool) : StateTransition.EvalsToInTime (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial).step (CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration polynomial 0 (CNFPolynomialRowMarkerTM.polynomialRowMarkerTopStage polynomial) input [] [] [] [] [] []) (some (Turing.haltList (CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine polynomial) (CNFPolynomialRowMarkerTM.sourcePreservingPolynomialMarkerWord polynomial input))) (Polynomial.eval input.length (polynomialRowMarkerTotalTimePolynomial polynomial))

Run the complete row-marker machine and produce its source-preserving output.

Equations

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

noncomputable def GapCVP.CLStructuralCNFOutputMachinesUnconditional.sourcePreservingPolynomialMarkerComputable (polynomial : Polynomial ℕ) : BitTM (CNFPolynomialRowMarkerTM.sourcePreservingPolynomialMarkerWord polynomial)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFDependentFiveFamilyRecordTM.executableAtLeastOneFamilyClauses (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.CNFDependentFiveFamilyRecordTM.executableAtMostOneFamilyClauses (T S : ℕ) : List (CL.Clause T S)

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFDependentFiveFamilyRecordTM.executableInitialFamilyClauses {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.

def GapCVP.CNFDependentFiveFamilyRecordTM.executableAcceptanceFamilyClauses {T S : ℕ} (specification : CL.Specification T S) : List (CL.Clause T S)

GapCVP reduction support.

Equations

• GapCVP.CNFDependentFiveFamilyRecordTM.executableAcceptanceFamilyClauses specification = [GapCVP.CL.acceptanceClause specification.accept]

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

Internal support shared across GapCVP continuation modules.

Equations

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

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

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFDependentFiveFamilyRecordTM.executableFiveFamilySourceClauseCandidates_toFinset {T S : ℕ} (specification : CL.Specification T S) : (executableFiveFamilySourceClauseCandidates specification).toFinset = CL.tableauFormula specification

Internal support shared across GapCVP continuation modules.

def GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput (valid : List Bool → List Bool) (fallback : List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput valid fallback (true :: input) = valid input
• GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput valid fallback x✝ = fallback

@[reducible, inline]

abbrev GapCVP.OutputPolynomialCompositionClosure.ConditionalLabel (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.OutputPolynomialCompositionClosure.ConditionalLabel tm = (tm.Λ ⊕ Bool)

@[reducible, inline]

abbrev GapCVP.OutputPolynomialCompositionClosure.ConditionalState (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.OutputPolynomialCompositionClosure.ConditionalState tm = (Option Bool × tm.σ)

@[reducible, inline]

abbrev GapCVP.OutputPolynomialCompositionClosure.liftValidStatement (tm : Turing.FinTM2) : Turing.TM2.Stmt (fun (k : tm.K) => tm.Γ (id k)) tm.Λ tm.σ → Turing.TM2.Stmt tm.Γ (tm.Λ ⊕ Bool) (Option Bool × tm.σ)

GapCVP reduction support.

Equations

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

def GapCVP.OutputPolynomialCompositionClosure.fixedOutputStatement {valid : List Bool → List Bool} (computer : BitTM valid) : List Bool → Turing.TM2.Stmt computer.tm.Γ (ConditionalLabel computer.tm) (ConditionalState computer.tm)

Write a fixed fallback word with the output alphabet of the given machine.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.OutputPolynomialCompositionClosure.fixedOutputStatement computer [] = Turing.TM2.Stmt.halt

@[reducible, inline]

noncomputable abbrev GapCVP.OutputPolynomialCompositionClosure.markerConditionalMachine {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) : Turing.FinTM2

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.OutputPolynomialCompositionClosure.validConfiguration {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (configuration : computer.tm.Cfg) : (markerConditionalMachine computer fallback).Cfg

GapCVP reduction support.

Equations

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

theorem GapCVP.OutputPolynomialCompositionClosure.liftValidStatement_stepAux {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (statement : Turing.TM2.Stmt computer.tm.Γ computer.tm.Λ computer.tm.σ) (state : computer.tm.σ) (sourceStacks : (k : computer.tm.K) → List (computer.tm.Γ k)) : Turing.TM2.stepAux (liftValidStatement computer.tm statement) (some true, state) sourceStacks = validConfiguration computer fallback (Turing.TM2.stepAux statement state sourceStacks)

theorem GapCVP.OutputPolynomialCompositionClosure.validConfiguration_step {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (configuration next : computer.tm.Cfg) (hstep : computer.tm.step configuration = some next) : (markerConditionalMachine computer fallback).step (validConfiguration computer fallback configuration) = some (validConfiguration computer fallback next)

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.OutputPolynomialCompositionClosure.initialStack_input (tm : Turing.FinTM2) (input : List (tm.Γ tm.k₀)) : (Turing.initList tm input).stk tm.k₀ = input

@[simp]

theorem GapCVP.OutputPolynomialCompositionClosure.initialStack_empty (tm : Turing.FinTM2) (k : tm.K) : (Turing.initList tm []).stk k = []

noncomputable def GapCVP.OutputPolynomialCompositionClosure.fallbackConfiguration {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (remaining : List (computer.tm.Γ computer.tm.k₀)) : (markerConditionalMachine computer fallback).Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.OutputPolynomialCompositionClosure.fallbackConfigurationStep {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (symbol : computer.tm.Γ computer.tm.k₀) (remaining : List (computer.tm.Γ computer.tm.k₀)) : (markerConditionalMachine computer fallback).step (fallbackConfiguration computer fallback (symbol :: remaining)) = some (fallbackConfiguration computer fallback remaining)

theorem GapCVP.OutputPolynomialCompositionClosure.fallbackConfigurationFinish {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) : (markerConditionalMachine computer fallback).step (fallbackConfiguration computer fallback []) = some (Turing.haltList (markerConditionalMachine computer fallback) (List.map computer.outputAlphabet.invFun fallback))

noncomputable def GapCVP.OutputPolynomialCompositionClosure.fallbackTrace {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (remaining : List (computer.tm.Γ computer.tm.k₀)) : StateTransition.EvalsToInTime (markerConditionalMachine computer fallback).step (fallbackConfiguration computer fallback remaining) (some (Turing.haltList (markerConditionalMachine computer fallback) (List.map computer.outputAlphabet.invFun fallback))) (remaining.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.OutputPolynomialCompositionClosure.markerConditional_start_true {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (remaining : List (computer.tm.Γ computer.tm.k₀)) : (markerConditionalMachine computer fallback).step (Turing.initList (markerConditionalMachine computer fallback) (computer.inputAlphabet.invFun true :: remaining)) = some (validConfiguration computer fallback (Turing.initList computer.tm remaining))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputPolynomialCompositionClosure.markerConditional_start_false {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (remaining : List (computer.tm.Γ computer.tm.k₀)) : (markerConditionalMachine computer fallback).step (Turing.initList (markerConditionalMachine computer fallback) (computer.inputAlphabet.invFun false :: remaining)) = some (fallbackConfiguration computer fallback remaining)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputPolynomialCompositionClosure.markerConditional_start_missing {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) : (markerConditionalMachine computer fallback).step (Turing.initList (markerConditionalMachine computer fallback) []) = some (fallbackConfiguration computer fallback [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputPolynomialCompositionClosure.validConfiguration_halt {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (output : List (computer.tm.Γ computer.tm.k₁)) : validConfiguration computer fallback (Turing.haltList computer.tm output) = Turing.haltList (markerConditionalMachine computer fallback) output

Internal support shared across GapCVP continuation modules.