Pell Light All Matching Certificates 007

import Init
import Mathlib.Data.List.Defs
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_006
import Definitions.Def_D1Bound5_PellLightMatchingBridge_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingData4_Definitions_002
import Definitions.Def_D1Bound5_PellLightMatchingData4_Definitions_003
import Definitions.Def_D1Bound5_PellLightMatchingData4_Definitions_004
import Definitions.Def_D1Bound5_PellLightMatchingData4_Definitions_005
import Definitions.Def_D1Bound5_PellLightMatchingData4_Definitions_006
import Definitions.Def_D1Bound5_PellLightMatching_Definitions
import Definitions.Def_D1Bound5_PellMatchingCheck_Definitions

section
namespace D1Bound5
set_option maxRecDepth 32768
set_option maxHeartbeats 12000000

































































































































































































































































































































































































































































































































































































































































































































































































def pellGraphCertificate_1063 : PellMatchingCertificate 1063 where
  magnitudes := pellMagnitudes_1063
  masks := pellMasks_1063
  witnesses := pellWitnesses_1063
  masks_valid := pellMasks_1063_valid
  checked := pellMatching_1063_checked
  large := pellMagnitudes_1063_large

def pellMagnitudes_1087 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1087

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

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

theorem pellMasks_1087_valid : ∀ m ∈ pellMasks_1087, m.Valid 1087 := by
  exact pellLightMasks_valid 1087 PellMatchingLightProduction.pellMasks_1087 PellMatchingLightProduction.pellMasks_1087_valid

theorem pellMatching_1087_checked :
    pellMatchingCheck pellMasks_1087 pellMagnitudes_1087 pellWitnesses_1087 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1087
    PellMatchingLightProduction.pellMagnitudes_1087 PellMatchingLightProduction.pellWitnesses_1087).symm.trans
      PellMatchingLightProduction.pellMatching_1087_checked

theorem pellMagnitudes_1087_large : ∀ x ∈ pellMagnitudes_1087, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1087 PellMatchingLightProduction.pellMagnitudes_1087_large

def pellGraphCertificate_1087 : PellMatchingCertificate 1087 where
  magnitudes := pellMagnitudes_1087
  masks := pellMasks_1087
  witnesses := pellWitnesses_1087
  masks_valid := pellMasks_1087_valid
  checked := pellMatching_1087_checked
  large := pellMagnitudes_1087_large

def pellMagnitudes_1103 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1103

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

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

theorem pellMasks_1103_valid : ∀ m ∈ pellMasks_1103, m.Valid 1103 := by
  exact pellLightMasks_valid 1103 PellMatchingLightProduction.pellMasks_1103 PellMatchingLightProduction.pellMasks_1103_valid

theorem pellMatching_1103_checked :
    pellMatchingCheck pellMasks_1103 pellMagnitudes_1103 pellWitnesses_1103 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1103
    PellMatchingLightProduction.pellMagnitudes_1103 PellMatchingLightProduction.pellWitnesses_1103).symm.trans
      PellMatchingLightProduction.pellMatching_1103_checked

theorem pellMagnitudes_1103_large : ∀ x ∈ pellMagnitudes_1103, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1103 PellMatchingLightProduction.pellMagnitudes_1103_large

def pellGraphCertificate_1103 : PellMatchingCertificate 1103 where
  magnitudes := pellMagnitudes_1103
  masks := pellMasks_1103
  witnesses := pellWitnesses_1103
  masks_valid := pellMasks_1103_valid
  checked := pellMatching_1103_checked
  large := pellMagnitudes_1103_large

def pellMagnitudes_1151 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1151

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

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

theorem pellMasks_1151_valid : ∀ m ∈ pellMasks_1151, m.Valid 1151 := by
  exact pellLightMasks_valid 1151 PellMatchingLightProduction.pellMasks_1151 PellMatchingLightProduction.pellMasks_1151_valid

theorem pellMatching_1151_checked :
    pellMatchingCheck pellMasks_1151 pellMagnitudes_1151 pellWitnesses_1151 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1151
    PellMatchingLightProduction.pellMagnitudes_1151 PellMatchingLightProduction.pellWitnesses_1151).symm.trans
      PellMatchingLightProduction.pellMatching_1151_checked

theorem pellMagnitudes_1151_large : ∀ x ∈ pellMagnitudes_1151, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1151 PellMatchingLightProduction.pellMagnitudes_1151_large

def pellGraphCertificate_1151 : PellMatchingCertificate 1151 where
  magnitudes := pellMagnitudes_1151
  masks := pellMasks_1151
  witnesses := pellWitnesses_1151
  masks_valid := pellMasks_1151_valid
  checked := pellMatching_1151_checked
  large := pellMagnitudes_1151_large

def pellMagnitudes_1207 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1207

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

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

theorem pellMasks_1207_valid : ∀ m ∈ pellMasks_1207, m.Valid 1207 := by
  exact pellLightMasks_valid 1207 PellMatchingLightProduction.pellMasks_1207 PellMatchingLightProduction.pellMasks_1207_valid

theorem pellMatching_1207_checked :
    pellMatchingCheck pellMasks_1207 pellMagnitudes_1207 pellWitnesses_1207 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1207
    PellMatchingLightProduction.pellMagnitudes_1207 PellMatchingLightProduction.pellWitnesses_1207).symm.trans
      PellMatchingLightProduction.pellMatching_1207_checked

theorem pellMagnitudes_1207_large : ∀ x ∈ pellMagnitudes_1207, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1207 PellMatchingLightProduction.pellMagnitudes_1207_large

def pellGraphCertificate_1207 : PellMatchingCertificate 1207 where
  magnitudes := pellMagnitudes_1207
  masks := pellMasks_1207
  witnesses := pellWitnesses_1207
  masks_valid := pellMasks_1207_valid
  checked := pellMatching_1207_checked
  large := pellMagnitudes_1207_large

def pellMagnitudes_1223 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1223

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

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

theorem pellMasks_1223_valid : ∀ m ∈ pellMasks_1223, m.Valid 1223 := by
  exact pellLightMasks_valid 1223 PellMatchingLightProduction.pellMasks_1223 PellMatchingLightProduction.pellMasks_1223_valid

theorem pellMatching_1223_checked :
    pellMatchingCheck pellMasks_1223 pellMagnitudes_1223 pellWitnesses_1223 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1223
    PellMatchingLightProduction.pellMagnitudes_1223 PellMatchingLightProduction.pellWitnesses_1223).symm.trans
      PellMatchingLightProduction.pellMatching_1223_checked

theorem pellMagnitudes_1223_large : ∀ x ∈ pellMagnitudes_1223, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1223 PellMatchingLightProduction.pellMagnitudes_1223_large

def pellGraphCertificate_1223 : PellMatchingCertificate 1223 where
  magnitudes := pellMagnitudes_1223
  masks := pellMasks_1223
  witnesses := pellWitnesses_1223
  masks_valid := pellMasks_1223_valid
  checked := pellMatching_1223_checked
  large := pellMagnitudes_1223_large

def pellMagnitudes_1231 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1231

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

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

theorem pellMasks_1231_valid : ∀ m ∈ pellMasks_1231, m.Valid 1231 := by
  exact pellLightMasks_valid 1231 PellMatchingLightProduction.pellMasks_1231 PellMatchingLightProduction.pellMasks_1231_valid

theorem pellMatching_1231_checked :
    pellMatchingCheck pellMasks_1231 pellMagnitudes_1231 pellWitnesses_1231 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1231
    PellMatchingLightProduction.pellMagnitudes_1231 PellMatchingLightProduction.pellWitnesses_1231).symm.trans
      PellMatchingLightProduction.pellMatching_1231_checked

theorem pellMagnitudes_1231_large : ∀ x ∈ pellMagnitudes_1231, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1231 PellMatchingLightProduction.pellMagnitudes_1231_large

def pellGraphCertificate_1231 : PellMatchingCertificate 1231 where
  magnitudes := pellMagnitudes_1231
  masks := pellMasks_1231
  witnesses := pellWitnesses_1231
  masks_valid := pellMasks_1231_valid
  checked := pellMatching_1231_checked
  large := pellMagnitudes_1231_large

def pellMagnitudes_1279 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1279

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

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

theorem pellMasks_1279_valid : ∀ m ∈ pellMasks_1279, m.Valid 1279 := by
  exact pellLightMasks_valid 1279 PellMatchingLightProduction.pellMasks_1279 PellMatchingLightProduction.pellMasks_1279_valid

theorem pellMatching_1279_checked :
    pellMatchingCheck pellMasks_1279 pellMagnitudes_1279 pellWitnesses_1279 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1279
    PellMatchingLightProduction.pellMagnitudes_1279 PellMatchingLightProduction.pellWitnesses_1279).symm.trans
      PellMatchingLightProduction.pellMatching_1279_checked

theorem pellMagnitudes_1279_large : ∀ x ∈ pellMagnitudes_1279, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1279 PellMatchingLightProduction.pellMagnitudes_1279_large

def pellGraphCertificate_1279 : PellMatchingCertificate 1279 where
  magnitudes := pellMagnitudes_1279
  masks := pellMasks_1279
  witnesses := pellWitnesses_1279
  masks_valid := pellMasks_1279_valid
  checked := pellMatching_1279_checked
  large := pellMagnitudes_1279_large

def pellMagnitudes_1303 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1303

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

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

theorem pellMasks_1303_valid : ∀ m ∈ pellMasks_1303, m.Valid 1303 := by
  exact pellLightMasks_valid 1303 PellMatchingLightProduction.pellMasks_1303 PellMatchingLightProduction.pellMasks_1303_valid

theorem pellMatching_1303_checked :
    pellMatchingCheck pellMasks_1303 pellMagnitudes_1303 pellWitnesses_1303 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1303
    PellMatchingLightProduction.pellMagnitudes_1303 PellMatchingLightProduction.pellWitnesses_1303).symm.trans
      PellMatchingLightProduction.pellMatching_1303_checked

theorem pellMagnitudes_1303_large : ∀ x ∈ pellMagnitudes_1303, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1303 PellMatchingLightProduction.pellMagnitudes_1303_large

def pellGraphCertificate_1303 : PellMatchingCertificate 1303 where
  magnitudes := pellMagnitudes_1303
  masks := pellMasks_1303
  witnesses := pellWitnesses_1303
  masks_valid := pellMasks_1303_valid
  checked := pellMatching_1303_checked
  large := pellMagnitudes_1303_large

def pellMagnitudes_1319 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1319

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

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

theorem pellMasks_1319_valid : ∀ m ∈ pellMasks_1319, m.Valid 1319 := by
  exact pellLightMasks_valid 1319 PellMatchingLightProduction.pellMasks_1319 PellMatchingLightProduction.pellMasks_1319_valid

theorem pellMatching_1319_checked :
    pellMatchingCheck pellMasks_1319 pellMagnitudes_1319 pellWitnesses_1319 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1319
    PellMatchingLightProduction.pellMagnitudes_1319 PellMatchingLightProduction.pellWitnesses_1319).symm.trans
      PellMatchingLightProduction.pellMatching_1319_checked

theorem pellMagnitudes_1319_large : ∀ x ∈ pellMagnitudes_1319, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1319 PellMatchingLightProduction.pellMagnitudes_1319_large

def pellGraphCertificate_1319 : PellMatchingCertificate 1319 where
  magnitudes := pellMagnitudes_1319
  masks := pellMasks_1319
  witnesses := pellWitnesses_1319
  masks_valid := pellMasks_1319_valid
  checked := pellMatching_1319_checked
  large := pellMagnitudes_1319_large































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































end D1Bound5
end