34.5. Complete Weights

CLRS-Lean
Chapter 34. NP-Completeness
34.5. NP-Complete Problems
34.5. Decision traveling-salesperson problem
34.5. HAM-CYCLE to TSP reduction machine
34.5. Complete Weights

Imports
                import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.ReductionMachine.Codec
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.ReductionMachine.DiagonalWeights
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.ReductionMachine.SymmetricWeights
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.ReductionMachine.WeightSemantics

              
                
                  Fixed generation of the complete HAM-CYCLE to TSP weight table 
                
              

              noncomputable sectionnamespace CLRS.Chapter34.Turing.TSPReductionopen _root_.Turingopen PolyBuilderdef completeWeightFields (I : CliqueInstance) : List TSPSym :=
  diagonalWeightFields I ++ symmetricWeightFields I

theorem completeWeightFields_eq (I : CliqueInstance) :
    completeWeightFields I = encodeTSPFields
      (CLRS.Chapter34.TSPReduction.hamiltonianWeights I) := by
  rw [← completeHamiltonianWeights_eq]
  simp [completeWeightFields, diagonalWeightFields, symmetricWeightFields,
    completeHamiltonianWeights, encodeTSPFields, List.flatMap_append]noncomputable def completeWeightFieldsComputableInPolyTime :
    TM2ComputableInPolyTime encodeCliqueInstance id completeWeightFields := by
  exact fixedPairSameInputConcat_computableInPolyTime
    encodeTSPSymPair decodeTSPSymPair decode_encodeTSPSymPair
    diagonalWeightFieldsComputableInPolyTime
    symmetricWeightFieldsComputableInPolyTimeend CLRS.Chapter34.Turing.TSPReduction