GapCVP proof, part 03

noncomputable def GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptancePhaseSymbolAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CL.WindowSymbols (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptancePhaseSpecification (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : CL.Specification (Polynomial.eval x.length (CLNondeterminism.nondeterministicTableauDimensionPolynomial bound machine)) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptanceLocalTableauCompiler (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : CLNondeterminism.LocalTableauCompiler bound machine

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CLStructuralCNFVariableBounds.tableauFiniteVariableCodeBound (T S : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.CLStructuralCNFVariableBounds.tableauFiniteVariableCodeBound T S = ((T + S + 2) ^ 2 + 1) ^ 2

theorem GapCVP.CLStructuralCNFVariableBounds.tableauVariable_encode_lt {T S : ℕ} (v : CL.Variable T S) : Encodable.encode v < tableauFiniteVariableCodeBound T S

theorem GapCVP.CLStructuralCNFVariableBounds.sourceVariable_lt_tableauFiniteBound {T S : ℕ} (v : CL.Variable T S) : ThreeCNFReduction.sourceVariable v < 4 * tableauFiniteVariableCodeBound T S

def GapCVP.CLStructuralPrefixWriter.tacticPrefixWriterStepTac : Lean.ParserDescr

Executes the prefixWriterStepTac machine-step simplifier.

Equations

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

noncomputable def GapCVP.CLStructuralPrefixWriter.structuralPrefixWriterComputable : Turing.TM2ComputableInPolyTime bitEncoding bitEncoding fun (input : List Bool) => BinaryEncoding.lengthPrefixedWord input

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceMachineCert.prependBitComputable (bit : Bool) : BitTM fun (input : List Bool) => bit :: input

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceMachineCert.prependWordComputable (word : List Bool) : BitTM fun (input : List Bool) => word ++ input

GapCVP reduction support.

Equations

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

def GapCVP.SourceMachineCert.formulaVariables (formula : ThreeCNF) : List ℕ

GapCVP reduction support.

Equations

• GapCVP.SourceMachineCert.formulaVariables formula = List.flatMap (fun (clause : GapCVP.ThreeClause) => [(clause 0).1, (clause 1).1, (clause 2).1]) formula

@[simp]

theorem GapCVP.SourceMachineCert.formulaVariables_length (formula : ThreeCNF) : (formulaVariables formula).length = 3 * List.length formula

theorem GapCVP.SourceMachineCert.mem_formulaVariables (formula : ThreeCNF) (clause : ThreeClause) (hclause : clause ∈ formula) (i : Fin 3) : (clause i).1 ∈ formulaVariables formula

def GapCVP.SourceMachineCert.variableRank (formula : ThreeCNF) (index : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.SourceMachineCert.variableRank formula index = List.idxOf index (GapCVP.SourceMachineCert.formulaVariables formula)

def GapCVP.SourceMachineRouting.canonicalYesInstance : GapCVPInstance

GapCVP reduction support.

Equations

• GapCVP.SourceMachineRouting.canonicalYesInstance = { dimension := 1, basis := Matrix.of fun (x x_1 : Fin 1) => 1, target := fun (x : Fin 1) => 0, radius := 1 }

theorem GapCVP.SourceMachineRouting.canonicalYesInstance_wellFormed : gapCVPWellFormed canonicalYesInstance = true

theorem GapCVP.SourceMachineRouting.canonicalYesInstance_gapYES : gapYES canonicalYesInstance = true

def GapCVP.SourceMachineRouting.canonicalYesWord : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceMachineRouting.canonicalYesWord = GapCVP.BinaryEncoding.encodeGapCVPInstance GapCVP.SourceMachineRouting.canonicalYesInstance

noncomputable def GapCVP.SourceUniformTuringTM.constantWordComputable (word : List Bool) : BitTM fun (x : List Bool) => word

GapCVP reduction support.

Equations

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

def GapCVP.SourceStructuralTuringTM.unaryPrefixLength : List Bool → ℕ

GapCVP reduction support.

Equations

• GapCVP.SourceStructuralTuringTM.unaryPrefixLength [] = 0
• GapCVP.SourceStructuralTuringTM.unaryPrefixLength (false :: tail) = 0
• GapCVP.SourceStructuralTuringTM.unaryPrefixLength (true :: rest) = GapCVP.SourceStructuralTuringTM.unaryPrefixLength rest + 1

def GapCVP.SourceStructuralTuringTM.unaryPrefixHasDelimiter : List Bool → Bool

GapCVP reduction support.

Equations

• GapCVP.SourceStructuralTuringTM.unaryPrefixHasDelimiter [] = false
• GapCVP.SourceStructuralTuringTM.unaryPrefixHasDelimiter (false :: tail) = true
• GapCVP.SourceStructuralTuringTM.unaryPrefixHasDelimiter (true :: rest) = GapCVP.SourceStructuralTuringTM.unaryPrefixHasDelimiter rest

def GapCVP.SourceStructuralTuringTM.unaryPrefixOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceStructuralTuringTM.unaryPrefixComputable : BitTM unaryPrefixOutput

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceStructuralTuringTM.unaryPrefixOutput_replicate_delimiter (count : ℕ) (suffix : List Bool) : unaryPrefixOutput (List.replicate count true ++ false :: suffix) = true :: List.replicate count true

@[reducible, inline]

abbrev GapCVP.SourceStructuralDecoder.payloadDecoderMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceStructuralDecoder.payloadConfiguration (phase : Fin 5) (input counter reversed output : List Bool) : payloadDecoderMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceStructuralDecoder.payloadConfiguration phase input counter reversed output = { l := some phase, var := none, stk := ![input, counter, reversed, output] }

theorem GapCVP.SourceStructuralDecoder.payload_prefix_true (input counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 0 (true :: input) counter reversed output) = some (payloadConfiguration 0 input (true :: counter) reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_prefix_missing_delimiter (counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 0 [] counter reversed output) = some (payloadConfiguration 4 [] counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_copy_step (bit : Bool) (input counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 1 (bit :: input) (true :: counter) reversed output) = some (payloadConfiguration 1 input counter (bit :: reversed) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_insufficient (counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 1 [] (true :: counter) reversed output) = some (payloadConfiguration 4 [] (true :: counter) reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_counter_complete (input reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 1 input [] reversed output) = some (payloadConfiguration 2 input [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_reverse_complete (input output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 2 input [] [] output) = some (payloadConfiguration 3 input [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_failure_drop_input (bit : Bool) (input counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 4 (bit :: input) counter reversed output) = some (payloadConfiguration 4 input counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_failure_drop_counter (bit : Bool) (counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 4 [] (bit :: counter) reversed output) = some (payloadConfiguration 4 [] counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_failure_drop_reversed (bit : Bool) (reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 4 [] [] (bit :: reversed) output) = some (payloadConfiguration 4 [] [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_failure_finish (output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 4 [] [] [] output) = some (Turing.haltList payloadDecoderMachine (false :: output))

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.SourceStructuralDecoder.replicate_true_append_cons (count : ℕ) (tail : List Bool) : List.replicate count true ++ true :: tail = true :: (List.replicate count true ++ tail)

def GapCVP.SourceStructuralDecoder.payloadPrefixTrace (count : ℕ) (tail counter reversed output : List Bool) : StateTransition.EvalsToInTime payloadDecoderMachine.step (payloadConfiguration 0 (List.replicate count true ++ false :: tail) counter reversed output) (some (payloadConfiguration 1 tail (List.replicate count true ++ counter) reversed output)) (count + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceStructuralDecoder.payloadCopyTrace (payload suffix reversed output : List Bool) : StateTransition.EvalsToInTime payloadDecoderMachine.step (payloadConfiguration 1 (payload ++ suffix) (List.replicate payload.length true) reversed output) (some (payloadConfiguration 1 suffix [] (payload.reverse ++ reversed) output)) payload.length

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceStructuralDecoder.payloadReverseTrace (input reversed output : List Bool) : StateTransition.EvalsToInTime payloadDecoderMachine.step (payloadConfiguration 2 input [] reversed output) (some (payloadConfiguration 2 input [] [] (reversed.reverse ++ output))) reversed.length

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceStructuralDecoder.payloadDrainTrace (suffix output : List Bool) : StateTransition.EvalsToInTime payloadDecoderMachine.step (payloadConfiguration 3 suffix [] [] output) (some (Turing.haltList payloadDecoderMachine (true :: output))) (suffix.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.SourceStructuralDecoder.payloadDecoderMachine_init (input : List Bool) : Turing.initList payloadDecoderMachine input = payloadConfiguration 0 input [] [] []

Internal support shared across GapCVP continuation modules.