Pell Light All Matching Certificates 002

import Init
import Mathlib.Data.List.Defs
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_001
import Definitions.Def_D1Bound5_PellLightMatchingBridge_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField127_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField151_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField167_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField191_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField199_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField223_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField239_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField263_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField271_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField287_Definitions
import Definitions.Def_D1Bound5_PellLightMatching_Definitions
import Definitions.Def_D1Bound5_PellMatchingCheck_Definitions

section
namespace D1Bound5
set_option maxRecDepth 32768
set_option maxHeartbeats 12000000

































































































































def pellMasks_127 : List PellSquareMasks :=
  PellMatchingLightProduction.pellMasks_127.map pellLightMasksToOriginal

def pellWitnesses_127 : List (List (ℕ × ℕ)) :=
  PellMatchingLightProduction.pellWitnesses_127

theorem pellMasks_127_valid : ∀ m ∈ pellMasks_127, m.Valid 127 := by
  exact pellLightMasks_valid 127 PellMatchingLightProduction.pellMasks_127 PellMatchingLightProduction.pellMasks_127_valid

theorem pellMatching_127_checked :
    pellMatchingCheck pellMasks_127 pellMagnitudes_127 pellWitnesses_127 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_127
    PellMatchingLightProduction.pellMagnitudes_127 PellMatchingLightProduction.pellWitnesses_127).symm.trans
      PellMatchingLightProduction.pellMatching_127_checked

theorem pellMagnitudes_127_large : ∀ x ∈ pellMagnitudes_127, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_127 PellMatchingLightProduction.pellMagnitudes_127_large

def pellGraphCertificate_127 : PellMatchingCertificate 127 where
  magnitudes := pellMagnitudes_127
  masks := pellMasks_127
  witnesses := pellWitnesses_127
  masks_valid := pellMasks_127_valid
  checked := pellMatching_127_checked
  large := pellMagnitudes_127_large

def pellMagnitudes_151 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_151

def pellMasks_151 : List PellSquareMasks :=
  PellMatchingLightProduction.pellMasks_151.map pellLightMasksToOriginal

def pellWitnesses_151 : List (List (ℕ × ℕ)) :=
  PellMatchingLightProduction.pellWitnesses_151

theorem pellMasks_151_valid : ∀ m ∈ pellMasks_151, m.Valid 151 := by
  exact pellLightMasks_valid 151 PellMatchingLightProduction.pellMasks_151 PellMatchingLightProduction.pellMasks_151_valid

theorem pellMatching_151_checked :
    pellMatchingCheck pellMasks_151 pellMagnitudes_151 pellWitnesses_151 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_151
    PellMatchingLightProduction.pellMagnitudes_151 PellMatchingLightProduction.pellWitnesses_151).symm.trans
      PellMatchingLightProduction.pellMatching_151_checked

theorem pellMagnitudes_151_large : ∀ x ∈ pellMagnitudes_151, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_151 PellMatchingLightProduction.pellMagnitudes_151_large

def pellGraphCertificate_151 : PellMatchingCertificate 151 where
  magnitudes := pellMagnitudes_151
  masks := pellMasks_151
  witnesses := pellWitnesses_151
  masks_valid := pellMasks_151_valid
  checked := pellMatching_151_checked
  large := pellMagnitudes_151_large

def pellMagnitudes_167 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_167

def pellMasks_167 : List PellSquareMasks :=
  PellMatchingLightProduction.pellMasks_167.map pellLightMasksToOriginal

def pellWitnesses_167 : List (List (ℕ × ℕ)) :=
  PellMatchingLightProduction.pellWitnesses_167

theorem pellMasks_167_valid : ∀ m ∈ pellMasks_167, m.Valid 167 := by
  exact pellLightMasks_valid 167 PellMatchingLightProduction.pellMasks_167 PellMatchingLightProduction.pellMasks_167_valid

theorem pellMatching_167_checked :
    pellMatchingCheck pellMasks_167 pellMagnitudes_167 pellWitnesses_167 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_167
    PellMatchingLightProduction.pellMagnitudes_167 PellMatchingLightProduction.pellWitnesses_167).symm.trans
      PellMatchingLightProduction.pellMatching_167_checked

theorem pellMagnitudes_167_large : ∀ x ∈ pellMagnitudes_167, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_167 PellMatchingLightProduction.pellMagnitudes_167_large

def pellGraphCertificate_167 : PellMatchingCertificate 167 where
  magnitudes := pellMagnitudes_167
  masks := pellMasks_167
  witnesses := pellWitnesses_167
  masks_valid := pellMasks_167_valid
  checked := pellMatching_167_checked
  large := pellMagnitudes_167_large

def pellMagnitudes_191 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_191

def pellMasks_191 : List PellSquareMasks :=
  PellMatchingLightProduction.pellMasks_191.map pellLightMasksToOriginal

def pellWitnesses_191 : List (List (ℕ × ℕ)) :=
  PellMatchingLightProduction.pellWitnesses_191

theorem pellMasks_191_valid : ∀ m ∈ pellMasks_191, m.Valid 191 := by
  exact pellLightMasks_valid 191 PellMatchingLightProduction.pellMasks_191 PellMatchingLightProduction.pellMasks_191_valid

theorem pellMatching_191_checked :
    pellMatchingCheck pellMasks_191 pellMagnitudes_191 pellWitnesses_191 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_191
    PellMatchingLightProduction.pellMagnitudes_191 PellMatchingLightProduction.pellWitnesses_191).symm.trans
      PellMatchingLightProduction.pellMatching_191_checked

theorem pellMagnitudes_191_large : ∀ x ∈ pellMagnitudes_191, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_191 PellMatchingLightProduction.pellMagnitudes_191_large

def pellGraphCertificate_191 : PellMatchingCertificate 191 where
  magnitudes := pellMagnitudes_191
  masks := pellMasks_191
  witnesses := pellWitnesses_191
  masks_valid := pellMasks_191_valid
  checked := pellMatching_191_checked
  large := pellMagnitudes_191_large

def pellMagnitudes_199 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_199

def pellMasks_199 : List PellSquareMasks :=
  PellMatchingLightProduction.pellMasks_199.map pellLightMasksToOriginal

def pellWitnesses_199 : List (List (ℕ × ℕ)) :=
  PellMatchingLightProduction.pellWitnesses_199

theorem pellMasks_199_valid : ∀ m ∈ pellMasks_199, m.Valid 199 := by
  exact pellLightMasks_valid 199 PellMatchingLightProduction.pellMasks_199 PellMatchingLightProduction.pellMasks_199_valid

theorem pellMatching_199_checked :
    pellMatchingCheck pellMasks_199 pellMagnitudes_199 pellWitnesses_199 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_199
    PellMatchingLightProduction.pellMagnitudes_199 PellMatchingLightProduction.pellWitnesses_199).symm.trans
      PellMatchingLightProduction.pellMatching_199_checked

theorem pellMagnitudes_199_large : ∀ x ∈ pellMagnitudes_199, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_199 PellMatchingLightProduction.pellMagnitudes_199_large

def pellGraphCertificate_199 : PellMatchingCertificate 199 where
  magnitudes := pellMagnitudes_199
  masks := pellMasks_199
  witnesses := pellWitnesses_199
  masks_valid := pellMasks_199_valid
  checked := pellMatching_199_checked
  large := pellMagnitudes_199_large

def pellMagnitudes_223 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_223

def pellMasks_223 : List PellSquareMasks :=
  PellMatchingLightProduction.pellMasks_223.map pellLightMasksToOriginal

def pellWitnesses_223 : List (List (ℕ × ℕ)) :=
  PellMatchingLightProduction.pellWitnesses_223

theorem pellMasks_223_valid : ∀ m ∈ pellMasks_223, m.Valid 223 := by
  exact pellLightMasks_valid 223 PellMatchingLightProduction.pellMasks_223 PellMatchingLightProduction.pellMasks_223_valid

theorem pellMatching_223_checked :
    pellMatchingCheck pellMasks_223 pellMagnitudes_223 pellWitnesses_223 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_223
    PellMatchingLightProduction.pellMagnitudes_223 PellMatchingLightProduction.pellWitnesses_223).symm.trans
      PellMatchingLightProduction.pellMatching_223_checked

theorem pellMagnitudes_223_large : ∀ x ∈ pellMagnitudes_223, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_223 PellMatchingLightProduction.pellMagnitudes_223_large

def pellGraphCertificate_223 : PellMatchingCertificate 223 where
  magnitudes := pellMagnitudes_223
  masks := pellMasks_223
  witnesses := pellWitnesses_223
  masks_valid := pellMasks_223_valid
  checked := pellMatching_223_checked
  large := pellMagnitudes_223_large

def pellMagnitudes_239 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_239

def pellMasks_239 : List PellSquareMasks :=
  PellMatchingLightProduction.pellMasks_239.map pellLightMasksToOriginal

def pellWitnesses_239 : List (List (ℕ × ℕ)) :=
  PellMatchingLightProduction.pellWitnesses_239

theorem pellMasks_239_valid : ∀ m ∈ pellMasks_239, m.Valid 239 := by
  exact pellLightMasks_valid 239 PellMatchingLightProduction.pellMasks_239 PellMatchingLightProduction.pellMasks_239_valid

theorem pellMatching_239_checked :
    pellMatchingCheck pellMasks_239 pellMagnitudes_239 pellWitnesses_239 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_239
    PellMatchingLightProduction.pellMagnitudes_239 PellMatchingLightProduction.pellWitnesses_239).symm.trans
      PellMatchingLightProduction.pellMatching_239_checked

theorem pellMagnitudes_239_large : ∀ x ∈ pellMagnitudes_239, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_239 PellMatchingLightProduction.pellMagnitudes_239_large

def pellGraphCertificate_239 : PellMatchingCertificate 239 where
  magnitudes := pellMagnitudes_239
  masks := pellMasks_239
  witnesses := pellWitnesses_239
  masks_valid := pellMasks_239_valid
  checked := pellMatching_239_checked
  large := pellMagnitudes_239_large

def pellMagnitudes_263 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_263

def pellMasks_263 : List PellSquareMasks :=
  PellMatchingLightProduction.pellMasks_263.map pellLightMasksToOriginal

def pellWitnesses_263 : List (List (ℕ × ℕ)) :=
  PellMatchingLightProduction.pellWitnesses_263

theorem pellMasks_263_valid : ∀ m ∈ pellMasks_263, m.Valid 263 := by
  exact pellLightMasks_valid 263 PellMatchingLightProduction.pellMasks_263 PellMatchingLightProduction.pellMasks_263_valid

theorem pellMatching_263_checked :
    pellMatchingCheck pellMasks_263 pellMagnitudes_263 pellWitnesses_263 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_263
    PellMatchingLightProduction.pellMagnitudes_263 PellMatchingLightProduction.pellWitnesses_263).symm.trans
      PellMatchingLightProduction.pellMatching_263_checked

theorem pellMagnitudes_263_large : ∀ x ∈ pellMagnitudes_263, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_263 PellMatchingLightProduction.pellMagnitudes_263_large

def pellGraphCertificate_263 : PellMatchingCertificate 263 where
  magnitudes := pellMagnitudes_263
  masks := pellMasks_263
  witnesses := pellWitnesses_263
  masks_valid := pellMasks_263_valid
  checked := pellMatching_263_checked
  large := pellMagnitudes_263_large

def pellMagnitudes_271 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_271

def pellMasks_271 : List PellSquareMasks :=
  PellMatchingLightProduction.pellMasks_271.map pellLightMasksToOriginal

def pellWitnesses_271 : List (List (ℕ × ℕ)) :=
  PellMatchingLightProduction.pellWitnesses_271

theorem pellMasks_271_valid : ∀ m ∈ pellMasks_271, m.Valid 271 := by
  exact pellLightMasks_valid 271 PellMatchingLightProduction.pellMasks_271 PellMatchingLightProduction.pellMasks_271_valid

theorem pellMatching_271_checked :
    pellMatchingCheck pellMasks_271 pellMagnitudes_271 pellWitnesses_271 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_271
    PellMatchingLightProduction.pellMagnitudes_271 PellMatchingLightProduction.pellWitnesses_271).symm.trans
      PellMatchingLightProduction.pellMatching_271_checked

theorem pellMagnitudes_271_large : ∀ x ∈ pellMagnitudes_271, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_271 PellMatchingLightProduction.pellMagnitudes_271_large

def pellGraphCertificate_271 : PellMatchingCertificate 271 where
  magnitudes := pellMagnitudes_271
  masks := pellMasks_271
  witnesses := pellWitnesses_271
  masks_valid := pellMasks_271_valid
  checked := pellMatching_271_checked
  large := pellMagnitudes_271_large

def pellMagnitudes_287 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_287

def pellMasks_287 : List PellSquareMasks :=
  PellMatchingLightProduction.pellMasks_287.map pellLightMasksToOriginal































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































end D1Bound5
end