Pell Light All Matching Certificates 005

import Init
import Mathlib.Data.List.Defs
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_004
import Definitions.Def_D1Bound5_PellLightMatchingBridge_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField647_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField679_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField719_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField727_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField743_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField751_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField823_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField839_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField863_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField887_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 pellMatching_647_checked :
    pellMatchingCheck pellMasks_647 pellMagnitudes_647 pellWitnesses_647 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_647
    PellMatchingLightProduction.pellMagnitudes_647 PellMatchingLightProduction.pellWitnesses_647).symm.trans
      PellMatchingLightProduction.pellMatching_647_checked

theorem pellMagnitudes_647_large : ∀ x ∈ pellMagnitudes_647, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_647 PellMatchingLightProduction.pellMagnitudes_647_large

def pellGraphCertificate_647 : PellMatchingCertificate 647 where
  magnitudes := pellMagnitudes_647
  masks := pellMasks_647
  witnesses := pellWitnesses_647
  masks_valid := pellMasks_647_valid
  checked := pellMatching_647_checked
  large := pellMagnitudes_647_large

def pellMagnitudes_679 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_679

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

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

theorem pellMasks_679_valid : ∀ m ∈ pellMasks_679, m.Valid 679 := by
  exact pellLightMasks_valid 679 PellMatchingLightProduction.pellMasks_679 PellMatchingLightProduction.pellMasks_679_valid

theorem pellMatching_679_checked :
    pellMatchingCheck pellMasks_679 pellMagnitudes_679 pellWitnesses_679 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_679
    PellMatchingLightProduction.pellMagnitudes_679 PellMatchingLightProduction.pellWitnesses_679).symm.trans
      PellMatchingLightProduction.pellMatching_679_checked

theorem pellMagnitudes_679_large : ∀ x ∈ pellMagnitudes_679, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_679 PellMatchingLightProduction.pellMagnitudes_679_large

def pellGraphCertificate_679 : PellMatchingCertificate 679 where
  magnitudes := pellMagnitudes_679
  masks := pellMasks_679
  witnesses := pellWitnesses_679
  masks_valid := pellMasks_679_valid
  checked := pellMatching_679_checked
  large := pellMagnitudes_679_large

def pellMagnitudes_719 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_719

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

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

theorem pellMasks_719_valid : ∀ m ∈ pellMasks_719, m.Valid 719 := by
  exact pellLightMasks_valid 719 PellMatchingLightProduction.pellMasks_719 PellMatchingLightProduction.pellMasks_719_valid

theorem pellMatching_719_checked :
    pellMatchingCheck pellMasks_719 pellMagnitudes_719 pellWitnesses_719 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_719
    PellMatchingLightProduction.pellMagnitudes_719 PellMatchingLightProduction.pellWitnesses_719).symm.trans
      PellMatchingLightProduction.pellMatching_719_checked

theorem pellMagnitudes_719_large : ∀ x ∈ pellMagnitudes_719, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_719 PellMatchingLightProduction.pellMagnitudes_719_large

def pellGraphCertificate_719 : PellMatchingCertificate 719 where
  magnitudes := pellMagnitudes_719
  masks := pellMasks_719
  witnesses := pellWitnesses_719
  masks_valid := pellMasks_719_valid
  checked := pellMatching_719_checked
  large := pellMagnitudes_719_large

def pellMagnitudes_727 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_727

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

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

theorem pellMasks_727_valid : ∀ m ∈ pellMasks_727, m.Valid 727 := by
  exact pellLightMasks_valid 727 PellMatchingLightProduction.pellMasks_727 PellMatchingLightProduction.pellMasks_727_valid

theorem pellMatching_727_checked :
    pellMatchingCheck pellMasks_727 pellMagnitudes_727 pellWitnesses_727 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_727
    PellMatchingLightProduction.pellMagnitudes_727 PellMatchingLightProduction.pellWitnesses_727).symm.trans
      PellMatchingLightProduction.pellMatching_727_checked

theorem pellMagnitudes_727_large : ∀ x ∈ pellMagnitudes_727, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_727 PellMatchingLightProduction.pellMagnitudes_727_large

def pellGraphCertificate_727 : PellMatchingCertificate 727 where
  magnitudes := pellMagnitudes_727
  masks := pellMasks_727
  witnesses := pellWitnesses_727
  masks_valid := pellMasks_727_valid
  checked := pellMatching_727_checked
  large := pellMagnitudes_727_large

def pellMagnitudes_743 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_743

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

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

theorem pellMasks_743_valid : ∀ m ∈ pellMasks_743, m.Valid 743 := by
  exact pellLightMasks_valid 743 PellMatchingLightProduction.pellMasks_743 PellMatchingLightProduction.pellMasks_743_valid

theorem pellMatching_743_checked :
    pellMatchingCheck pellMasks_743 pellMagnitudes_743 pellWitnesses_743 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_743
    PellMatchingLightProduction.pellMagnitudes_743 PellMatchingLightProduction.pellWitnesses_743).symm.trans
      PellMatchingLightProduction.pellMatching_743_checked

theorem pellMagnitudes_743_large : ∀ x ∈ pellMagnitudes_743, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_743 PellMatchingLightProduction.pellMagnitudes_743_large

def pellGraphCertificate_743 : PellMatchingCertificate 743 where
  magnitudes := pellMagnitudes_743
  masks := pellMasks_743
  witnesses := pellWitnesses_743
  masks_valid := pellMasks_743_valid
  checked := pellMatching_743_checked
  large := pellMagnitudes_743_large

def pellMagnitudes_751 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_751

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

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

theorem pellMasks_751_valid : ∀ m ∈ pellMasks_751, m.Valid 751 := by
  exact pellLightMasks_valid 751 PellMatchingLightProduction.pellMasks_751 PellMatchingLightProduction.pellMasks_751_valid

theorem pellMatching_751_checked :
    pellMatchingCheck pellMasks_751 pellMagnitudes_751 pellWitnesses_751 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_751
    PellMatchingLightProduction.pellMagnitudes_751 PellMatchingLightProduction.pellWitnesses_751).symm.trans
      PellMatchingLightProduction.pellMatching_751_checked

theorem pellMagnitudes_751_large : ∀ x ∈ pellMagnitudes_751, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_751 PellMatchingLightProduction.pellMagnitudes_751_large

def pellGraphCertificate_751 : PellMatchingCertificate 751 where
  magnitudes := pellMagnitudes_751
  masks := pellMasks_751
  witnesses := pellWitnesses_751
  masks_valid := pellMasks_751_valid
  checked := pellMatching_751_checked
  large := pellMagnitudes_751_large

def pellMagnitudes_823 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_823

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

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

theorem pellMasks_823_valid : ∀ m ∈ pellMasks_823, m.Valid 823 := by
  exact pellLightMasks_valid 823 PellMatchingLightProduction.pellMasks_823 PellMatchingLightProduction.pellMasks_823_valid

theorem pellMatching_823_checked :
    pellMatchingCheck pellMasks_823 pellMagnitudes_823 pellWitnesses_823 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_823
    PellMatchingLightProduction.pellMagnitudes_823 PellMatchingLightProduction.pellWitnesses_823).symm.trans
      PellMatchingLightProduction.pellMatching_823_checked

theorem pellMagnitudes_823_large : ∀ x ∈ pellMagnitudes_823, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_823 PellMatchingLightProduction.pellMagnitudes_823_large

def pellGraphCertificate_823 : PellMatchingCertificate 823 where
  magnitudes := pellMagnitudes_823
  masks := pellMasks_823
  witnesses := pellWitnesses_823
  masks_valid := pellMasks_823_valid
  checked := pellMatching_823_checked
  large := pellMagnitudes_823_large

def pellMagnitudes_839 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_839

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

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

theorem pellMasks_839_valid : ∀ m ∈ pellMasks_839, m.Valid 839 := by
  exact pellLightMasks_valid 839 PellMatchingLightProduction.pellMasks_839 PellMatchingLightProduction.pellMasks_839_valid

theorem pellMatching_839_checked :
    pellMatchingCheck pellMasks_839 pellMagnitudes_839 pellWitnesses_839 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_839
    PellMatchingLightProduction.pellMagnitudes_839 PellMatchingLightProduction.pellWitnesses_839).symm.trans
      PellMatchingLightProduction.pellMatching_839_checked

theorem pellMagnitudes_839_large : ∀ x ∈ pellMagnitudes_839, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_839 PellMatchingLightProduction.pellMagnitudes_839_large

def pellGraphCertificate_839 : PellMatchingCertificate 839 where
  magnitudes := pellMagnitudes_839
  masks := pellMasks_839
  witnesses := pellWitnesses_839
  masks_valid := pellMasks_839_valid
  checked := pellMatching_839_checked
  large := pellMagnitudes_839_large

def pellMagnitudes_863 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_863

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

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

theorem pellMasks_863_valid : ∀ m ∈ pellMasks_863, m.Valid 863 := by
  exact pellLightMasks_valid 863 PellMatchingLightProduction.pellMasks_863 PellMatchingLightProduction.pellMasks_863_valid

theorem pellMatching_863_checked :
    pellMatchingCheck pellMasks_863 pellMagnitudes_863 pellWitnesses_863 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_863
    PellMatchingLightProduction.pellMagnitudes_863 PellMatchingLightProduction.pellWitnesses_863).symm.trans
      PellMatchingLightProduction.pellMatching_863_checked

theorem pellMagnitudes_863_large : ∀ x ∈ pellMagnitudes_863, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_863 PellMatchingLightProduction.pellMagnitudes_863_large

def pellGraphCertificate_863 : PellMatchingCertificate 863 where
  magnitudes := pellMagnitudes_863
  masks := pellMasks_863
  witnesses := pellWitnesses_863
  masks_valid := pellMasks_863_valid
  checked := pellMatching_863_checked
  large := pellMagnitudes_863_large

def pellMagnitudes_887 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_887

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

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

theorem pellMasks_887_valid : ∀ m ∈ pellMasks_887, m.Valid 887 := by
  exact pellLightMasks_valid 887 PellMatchingLightProduction.pellMasks_887 PellMatchingLightProduction.pellMasks_887_valid

theorem pellMatching_887_checked :
    pellMatchingCheck pellMasks_887 pellMagnitudes_887 pellWitnesses_887 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_887
    PellMatchingLightProduction.pellMagnitudes_887 PellMatchingLightProduction.pellWitnesses_887).symm.trans
      PellMatchingLightProduction.pellMatching_887_checked































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































end D1Bound5
end