GapCVP proof, part 05, continuation 03

def GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusUnaryOutput : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusUnaryOutput [] = [false]
• GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusUnaryOutput (false :: tail) = [false]
• GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusUnaryOutput (true :: input) = GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusScanOutput✝ input 0

noncomputable def GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusUnaryComputable : BitTM rationalRadiusUnaryOutput

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusUnaryOutput_marked (number : ℕ) : rationalRadiusUnaryOutput (true :: List.replicate number true) = true :: List.replicate (4 * number ^ 2 + 2 * number + 1) true

theorem GapCVP.SourceInterpolationRowTM.readUnaryPrefix_some_decompose (input : List Bool) (count : ℕ) (suffix : List Bool) (hread : BinaryEncoding.readUnaryPrefix input = some (count, suffix)) : input = List.replicate count true ++ false :: suffix

theorem GapCVP.SourceInterpolationRowTM.readUnaryPrefix_none_eq_replicate (input : List Bool) (hread : BinaryEncoding.readUnaryPrefix input = none) : input = List.replicate input.length true

def GapCVP.SourceWholeOutputAssemblyTM.sourceVectorStructuralRecords {α : Type u_1} [Encodable α] (n : ℕ) (values : Fin n → α) : List (List Bool)

Encode each entry of a fixed-length vector as a separate structural record.

Equations

• GapCVP.SourceWholeOutputAssemblyTM.sourceVectorStructuralRecords n values = List.ofFn fun (index : Fin n) => GapCVP.BinaryEncoding.encodeAtomic (values index)

theorem GapCVP.SourceWholeOutputAssemblyTM.sourceVectorStructuralRecords_flatten {α : Type u_1} [Encodable α] (n : ℕ) (values : Fin n → α) : (sourceVectorStructuralRecords n values).flatten = BinaryEncoding.encodeFinValues n values

def GapCVP.SourceWholeOutputAssemblyTM.sourceMatrixStructuralRecords (m n : ℕ) (matrix : Fin m → Fin n → ℤ) : List (List Bool)

Flatten the structural records for each row of an integer matrix.

Equations

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

theorem GapCVP.SourceWholeOutputAssemblyTM.sourceMatrixStructuralRecords_flatten (m n : ℕ) (matrix : Fin m → Fin n → ℤ) : (sourceMatrixStructuralRecords m n matrix).flatten = BinaryEncoding.encodeMatrixRows m n matrix

@[simp]

theorem GapCVP.SourceWholeOutputAssemblyTM.sourceVectorStructuralRecords_length {α : Type u_1} [Encodable α] (n : ℕ) (values : Fin n → α) : (sourceVectorStructuralRecords n values).length = n

@[simp]

theorem GapCVP.SourceWholeOutputAssemblyTM.sourceMatrixStructuralRecords_length (m n : ℕ) (matrix : Fin m → Fin n → ℤ) : (sourceMatrixStructuralRecords m n matrix).length = m * n

def GapCVP.SourceWholeOutputAssemblyTM.sourceLatticeStructuralRecords (lattice : GapCVPInstance) : List (List Bool)

Record a lattice instance's dimension, radius, target, and basis.

Equations

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

theorem GapCVP.SourceWholeOutputAssemblyTM.sourceLatticeStructuralRecords_flatten (lattice : GapCVPInstance) : (sourceLatticeStructuralRecords lattice).flatten = BinaryEncoding.encodeGapCVPInstance lattice

@[simp]

theorem GapCVP.SourceWholeOutputAssemblyTM.sourceLatticeStructuralRecords_length (lattice : GapCVPInstance) : (sourceLatticeStructuralRecords lattice).length = 2 + lattice.dimension + lattice.dimension * lattice.dimension

def GapCVP.SourceWholeOutputAssemblyTM.constructiveCanonicalSourceMarker (input : List Bool) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceWholeOutputAssemblyTM.constructiveCanonicalSourceMarkerComputable : BitTM fun (input : List Bool) => constructiveCanonicalSourceMarker input :: input

GapCVP reduction support.

Equations

• GapCVP.SourceWholeOutputAssemblyTM.constructiveCanonicalSourceMarkerComputable = ⋯.mpr GapCVP.SourceLatticeDependentSectionComputation.validatedPreservedFormulaComputable

def GapCVP.SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicDescriptor (record : List Bool) : List Bool

The length-prefixed descriptor of one atomic source record.

Equations

• GapCVP.SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicDescriptor record = GapCVP.BinaryEncoding.lengthPrefixedWord record

def GapCVP.SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicRecordStep (input : List Bool) : List Bool

Move the first length-prefixed record behind the remaining input.

Equations

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

@[simp]

theorem GapCVP.SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicRecordStep_descriptor (record pending : List Bool) : sourceFlatAtomicRecordStep (sourceFlatAtomicDescriptor record ++ pending) = pending ++ record

def GapCVP.SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicDescriptorStream (records : List (List Bool)) : List Bool

Concatenate the length-prefixed descriptors of the source records.

Equations

• GapCVP.SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicDescriptorStream records = List.flatMap GapCVP.SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicDescriptor records

theorem GapCVP.SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicRecordStep_iterate_descriptors (records : List (List Bool)) (emitted : List Bool) : sourceFlatAtomicRecordStep^[records.length] (sourceFlatAtomicDescriptorStream records ++ emitted) = emitted ++ records.flatten

def GapCVP.SourceWholeOutputValidBranchRecordTM.tacticSourceFlatAtomicStepTac : Lean.ParserDescr

Executes the sourceFlatAtomicStepTac machine-step simplifier.

Equations

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

noncomputable def GapCVP.SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicRecordComputable : BitTM sourceFlatAtomicRecordStep

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicRecordFoldComputable : BitTM (OutputBoundedDependentRecordFold.boundedRecordFoldOutput sourceFlatAtomicRecordStep)

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceWholeOutputValidBranchRecordTM.boundedRecordFoldOutput_sourceFlatAtomicDescriptors (records : List (List Bool)) : OutputBoundedDependentRecordFold.boundedRecordFoldOutput sourceFlatAtomicRecordStep (OutputBoundedDependentRecordFold.unaryBoundedFoldWord records.length (sourceFlatAtomicDescriptorStream records)) = records.flatten

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceCanonicalUnaryGridIndexDescriptor (index : ℕ) : List Bool

The length-prefixed unary encoding of a grid index.

Equations

• GapCVP.SourceCanonicalUnaryGridIndexTM.sourceCanonicalUnaryGridIndexDescriptor index = GapCVP.BinaryEncoding.lengthPrefixedWord (List.replicate index true)

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceCanonicalUnaryGridIndexDescriptors (count : ℕ) : List Bool

Concatenate the grid-index descriptors below the given count.

Equations

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

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceCanonicalUnaryGridIndexDescriptors_succ (count : ℕ) : sourceCanonicalUnaryGridIndexDescriptors (count + 1) = sourceCanonicalUnaryGridIndexDescriptors count ++ sourceCanonicalUnaryGridIndexDescriptor count

Internal support shared across GapCVP continuation modules.

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceCanonicalUnaryGridIndexOutput (input : List Bool) : List Bool

Replace the leading unary count with its grid-index descriptors, preserving the source.

Equations

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

@[simp]

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceCanonicalUnaryGridIndexOutput_valid (count : ℕ) (source : List Bool) : sourceCanonicalUnaryGridIndexOutput (List.replicate count true ++ false :: source) = sourceCanonicalUnaryGridIndexDescriptors count ++ source

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndexPrefixStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndexArchiveStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndexSourceRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndexOuterStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndexCopyStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndexTemplateRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndexFailureStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

@[reducible, inline]

abbrev GapCVP.SourceCanonicalUnaryGridIndexTM.sourceCanonicalUnaryGridIndexMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndexConfiguration (phase : Fin 7) (input counter scratch archive output : List Bool) : sourceCanonicalUnaryGridIndexMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndexConfiguration phase input counter scratch archive output = { l := some phase, var := none, stk := ![input, counter, scratch, archive, output] }

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceCanonicalUnaryGridIndexMachine_init (input : List Bool) : Turing.initList sourceCanonicalUnaryGridIndexMachine input = sourceGridIndexConfiguration 0 input [] [] [] []

Internal support shared across GapCVP continuation modules.

def GapCVP.SourceCanonicalUnaryGridIndexTM.tacticSourceGridIndexStepTac : Lean.ParserDescr

Executes the sourceGridIndexStepTac machine-step simplifier.

Equations

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

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_prefix_true (input counter scratch archive output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 0 (true :: input) counter scratch archive output) = some (sourceGridIndexConfiguration 0 input (true :: counter) scratch archive output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_prefix_false (input counter scratch archive output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 0 (false :: input) counter scratch archive output) = some (sourceGridIndexConfiguration 1 input counter scratch archive output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_prefix_missing (counter scratch archive output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 0 [] counter scratch archive output) = some (sourceGridIndexConfiguration 6 [] counter scratch archive output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_archive_step (bit : Bool) (input counter scratch archive output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 1 (bit :: input) counter scratch archive output) = some (sourceGridIndexConfiguration 1 input counter scratch (bit :: archive) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_archive_finish (counter scratch archive output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 1 [] counter scratch archive output) = some (sourceGridIndexConfiguration 2 [] counter scratch archive output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_source_restore_step (bit : Bool) (counter scratch archive output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 2 [] counter scratch (bit :: archive) output) = some (sourceGridIndexConfiguration 2 [] counter scratch archive (bit :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_source_restore_finish (counter scratch output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 2 [] counter scratch [] output) = some (sourceGridIndexConfiguration 3 [] counter scratch [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_outer_step (counter output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 3 [] (true :: counter) [] [] output) = some (sourceGridIndexConfiguration 4 [] counter [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_outer_finish (output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 3 [] [] [] [] output) = some (Turing.haltList sourceCanonicalUnaryGridIndexMachine output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_copy_step (counter scratch output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 4 [] (true :: counter) scratch [] output) = some (sourceGridIndexConfiguration 4 [] counter (true :: scratch) [] (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_copy_finish (scratch output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 4 [] [] scratch [] output) = some (sourceGridIndexConfiguration 5 [] [] scratch [] (false :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_template_restore_step (counter scratch output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 5 [] counter (true :: scratch) [] output) = some (sourceGridIndexConfiguration 5 [] (true :: counter) scratch [] (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_template_restore_finish (counter output : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 5 [] counter [] [] output) = some (sourceGridIndexConfiguration 3 [] counter [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_failure_step (counter : List Bool) : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 6 [] (true :: counter) [] [] []) = some (sourceGridIndexConfiguration 6 [] counter [] [] [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceCanonicalUnaryGridIndexTM.sourceGridIndex_failure_finish : sourceCanonicalUnaryGridIndexMachine.step (sourceGridIndexConfiguration 6 [] [] [] [] []) = some (Turing.haltList sourceCanonicalUnaryGridIndexMachine [])

Internal support shared across GapCVP continuation modules.