Pell Light All Matching Certificates 006

import Init
import Mathlib.Data.List.Defs
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_005
import Definitions.Def_D1Bound5_PellLightMatchingBridge_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingData4_Definitions_001
import Definitions.Def_D1Bound5_PellLightMatchingData4_Definitions_002
import Definitions.Def_D1Bound5_PellLightMatchingData4_Definitions_003
import Definitions.Def_D1Bound5_PellLightMatchingField887_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField911_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField919_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField959_Definitions
import Definitions.Def_D1Bound5_PellLightMatching_Definitions
import Definitions.Def_D1Bound5_PellMatchingCheck_Definitions

section
namespace D1Bound5
set_option maxRecDepth 32768
set_option maxHeartbeats 12000000

































































































































































































































































































































































































































































































































































































































































theorem pellMagnitudes_887_large : ∀ x ∈ pellMagnitudes_887, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_887 PellMatchingLightProduction.pellMagnitudes_887_large

def pellGraphCertificate_887 : PellMatchingCertificate 887 where
  magnitudes := pellMagnitudes_887
  masks := pellMasks_887
  witnesses := pellWitnesses_887
  masks_valid := pellMasks_887_valid
  checked := pellMatching_887_checked
  large := pellMagnitudes_887_large

def pellMagnitudes_911 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_911

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

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

theorem pellMasks_911_valid : ∀ m ∈ pellMasks_911, m.Valid 911 := by
  exact pellLightMasks_valid 911 PellMatchingLightProduction.pellMasks_911 PellMatchingLightProduction.pellMasks_911_valid

theorem pellMatching_911_checked :
    pellMatchingCheck pellMasks_911 pellMagnitudes_911 pellWitnesses_911 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_911
    PellMatchingLightProduction.pellMagnitudes_911 PellMatchingLightProduction.pellWitnesses_911).symm.trans
      PellMatchingLightProduction.pellMatching_911_checked

theorem pellMagnitudes_911_large : ∀ x ∈ pellMagnitudes_911, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_911 PellMatchingLightProduction.pellMagnitudes_911_large

def pellGraphCertificate_911 : PellMatchingCertificate 911 where
  magnitudes := pellMagnitudes_911
  masks := pellMasks_911
  witnesses := pellWitnesses_911
  masks_valid := pellMasks_911_valid
  checked := pellMatching_911_checked
  large := pellMagnitudes_911_large

def pellMagnitudes_919 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_919

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

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

theorem pellMasks_919_valid : ∀ m ∈ pellMasks_919, m.Valid 919 := by
  exact pellLightMasks_valid 919 PellMatchingLightProduction.pellMasks_919 PellMatchingLightProduction.pellMasks_919_valid

theorem pellMatching_919_checked :
    pellMatchingCheck pellMasks_919 pellMagnitudes_919 pellWitnesses_919 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_919
    PellMatchingLightProduction.pellMagnitudes_919 PellMatchingLightProduction.pellWitnesses_919).symm.trans
      PellMatchingLightProduction.pellMatching_919_checked

theorem pellMagnitudes_919_large : ∀ x ∈ pellMagnitudes_919, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_919 PellMatchingLightProduction.pellMagnitudes_919_large

def pellGraphCertificate_919 : PellMatchingCertificate 919 where
  magnitudes := pellMagnitudes_919
  masks := pellMasks_919
  witnesses := pellWitnesses_919
  masks_valid := pellMasks_919_valid
  checked := pellMatching_919_checked
  large := pellMagnitudes_919_large

def pellMagnitudes_959 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_959

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

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

theorem pellMasks_959_valid : ∀ m ∈ pellMasks_959, m.Valid 959 := by
  exact pellLightMasks_valid 959 PellMatchingLightProduction.pellMasks_959 PellMatchingLightProduction.pellMasks_959_valid

theorem pellMatching_959_checked :
    pellMatchingCheck pellMasks_959 pellMagnitudes_959 pellWitnesses_959 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_959
    PellMatchingLightProduction.pellMagnitudes_959 PellMatchingLightProduction.pellWitnesses_959).symm.trans
      PellMatchingLightProduction.pellMatching_959_checked

theorem pellMagnitudes_959_large : ∀ x ∈ pellMagnitudes_959, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_959 PellMatchingLightProduction.pellMagnitudes_959_large

def pellGraphCertificate_959 : PellMatchingCertificate 959 where
  magnitudes := pellMagnitudes_959
  masks := pellMasks_959
  witnesses := pellWitnesses_959
  masks_valid := pellMasks_959_valid
  checked := pellMatching_959_checked
  large := pellMagnitudes_959_large

def pellMagnitudes_967 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_967

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

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

theorem pellMasks_967_valid : ∀ m ∈ pellMasks_967, m.Valid 967 := by
  exact pellLightMasks_valid 967 PellMatchingLightProduction.pellMasks_967 PellMatchingLightProduction.pellMasks_967_valid

theorem pellMatching_967_checked :
    pellMatchingCheck pellMasks_967 pellMagnitudes_967 pellWitnesses_967 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_967
    PellMatchingLightProduction.pellMagnitudes_967 PellMatchingLightProduction.pellWitnesses_967).symm.trans
      PellMatchingLightProduction.pellMatching_967_checked

theorem pellMagnitudes_967_large : ∀ x ∈ pellMagnitudes_967, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_967 PellMatchingLightProduction.pellMagnitudes_967_large

def pellGraphCertificate_967 : PellMatchingCertificate 967 where
  magnitudes := pellMagnitudes_967
  masks := pellMasks_967
  witnesses := pellWitnesses_967
  masks_valid := pellMasks_967_valid
  checked := pellMatching_967_checked
  large := pellMagnitudes_967_large

def pellMagnitudes_983 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_983

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

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

theorem pellMasks_983_valid : ∀ m ∈ pellMasks_983, m.Valid 983 := by
  exact pellLightMasks_valid 983 PellMatchingLightProduction.pellMasks_983 PellMatchingLightProduction.pellMasks_983_valid

theorem pellMatching_983_checked :
    pellMatchingCheck pellMasks_983 pellMagnitudes_983 pellWitnesses_983 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_983
    PellMatchingLightProduction.pellMagnitudes_983 PellMatchingLightProduction.pellWitnesses_983).symm.trans
      PellMatchingLightProduction.pellMatching_983_checked

theorem pellMagnitudes_983_large : ∀ x ∈ pellMagnitudes_983, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_983 PellMatchingLightProduction.pellMagnitudes_983_large

def pellGraphCertificate_983 : PellMatchingCertificate 983 where
  magnitudes := pellMagnitudes_983
  masks := pellMasks_983
  witnesses := pellWitnesses_983
  masks_valid := pellMasks_983_valid
  checked := pellMatching_983_checked
  large := pellMagnitudes_983_large

def pellMagnitudes_991 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_991

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

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

theorem pellMasks_991_valid : ∀ m ∈ pellMasks_991, m.Valid 991 := by
  exact pellLightMasks_valid 991 PellMatchingLightProduction.pellMasks_991 PellMatchingLightProduction.pellMasks_991_valid

theorem pellMatching_991_checked :
    pellMatchingCheck pellMasks_991 pellMagnitudes_991 pellWitnesses_991 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_991
    PellMatchingLightProduction.pellMagnitudes_991 PellMatchingLightProduction.pellWitnesses_991).symm.trans
      PellMatchingLightProduction.pellMatching_991_checked

theorem pellMagnitudes_991_large : ∀ x ∈ pellMagnitudes_991, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_991 PellMatchingLightProduction.pellMagnitudes_991_large

def pellGraphCertificate_991 : PellMatchingCertificate 991 where
  magnitudes := pellMagnitudes_991
  masks := pellMasks_991
  witnesses := pellWitnesses_991
  masks_valid := pellMasks_991_valid
  checked := pellMatching_991_checked
  large := pellMagnitudes_991_large

def pellMagnitudes_1031 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1031

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

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

theorem pellMasks_1031_valid : ∀ m ∈ pellMasks_1031, m.Valid 1031 := by
  exact pellLightMasks_valid 1031 PellMatchingLightProduction.pellMasks_1031 PellMatchingLightProduction.pellMasks_1031_valid

theorem pellMatching_1031_checked :
    pellMatchingCheck pellMasks_1031 pellMagnitudes_1031 pellWitnesses_1031 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1031
    PellMatchingLightProduction.pellMagnitudes_1031 PellMatchingLightProduction.pellWitnesses_1031).symm.trans
      PellMatchingLightProduction.pellMatching_1031_checked

theorem pellMagnitudes_1031_large : ∀ x ∈ pellMagnitudes_1031, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1031 PellMatchingLightProduction.pellMagnitudes_1031_large

def pellGraphCertificate_1031 : PellMatchingCertificate 1031 where
  magnitudes := pellMagnitudes_1031
  masks := pellMasks_1031
  witnesses := pellWitnesses_1031
  masks_valid := pellMasks_1031_valid
  checked := pellMatching_1031_checked
  large := pellMagnitudes_1031_large

def pellMagnitudes_1039 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1039

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

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

theorem pellMasks_1039_valid : ∀ m ∈ pellMasks_1039, m.Valid 1039 := by
  exact pellLightMasks_valid 1039 PellMatchingLightProduction.pellMasks_1039 PellMatchingLightProduction.pellMasks_1039_valid

theorem pellMatching_1039_checked :
    pellMatchingCheck pellMasks_1039 pellMagnitudes_1039 pellWitnesses_1039 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1039
    PellMatchingLightProduction.pellMagnitudes_1039 PellMatchingLightProduction.pellWitnesses_1039).symm.trans
      PellMatchingLightProduction.pellMatching_1039_checked

theorem pellMagnitudes_1039_large : ∀ x ∈ pellMagnitudes_1039, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1039 PellMatchingLightProduction.pellMagnitudes_1039_large

def pellGraphCertificate_1039 : PellMatchingCertificate 1039 where
  magnitudes := pellMagnitudes_1039
  masks := pellMasks_1039
  witnesses := pellWitnesses_1039
  masks_valid := pellMasks_1039_valid
  checked := pellMatching_1039_checked
  large := pellMagnitudes_1039_large

def pellMagnitudes_1063 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_1063

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

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

theorem pellMasks_1063_valid : ∀ m ∈ pellMasks_1063, m.Valid 1063 := by
  exact pellLightMasks_valid 1063 PellMatchingLightProduction.pellMasks_1063 PellMatchingLightProduction.pellMasks_1063_valid

theorem pellMatching_1063_checked :
    pellMatchingCheck pellMasks_1063 pellMagnitudes_1063 pellWitnesses_1063 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_1063
    PellMatchingLightProduction.pellMagnitudes_1063 PellMatchingLightProduction.pellWitnesses_1063).symm.trans
      PellMatchingLightProduction.pellMatching_1063_checked

theorem pellMagnitudes_1063_large : ∀ x ∈ pellMagnitudes_1063, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_1063 PellMatchingLightProduction.pellMagnitudes_1063_large































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































end D1Bound5
end