Pell Light All Matching Certificates 004

import Init
import Mathlib.Data.List.Defs
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_003
import Definitions.Def_D1Bound5_PellLightMatchingBridge_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField479_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField487_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField503_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField511_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField527_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField599_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField607_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField623_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField631_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField647_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 pellMasks_479_valid : ∀ m ∈ pellMasks_479, m.Valid 479 := by
  exact pellLightMasks_valid 479 PellMatchingLightProduction.pellMasks_479 PellMatchingLightProduction.pellMasks_479_valid

theorem pellMatching_479_checked :
    pellMatchingCheck pellMasks_479 pellMagnitudes_479 pellWitnesses_479 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_479
    PellMatchingLightProduction.pellMagnitudes_479 PellMatchingLightProduction.pellWitnesses_479).symm.trans
      PellMatchingLightProduction.pellMatching_479_checked

theorem pellMagnitudes_479_large : ∀ x ∈ pellMagnitudes_479, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_479 PellMatchingLightProduction.pellMagnitudes_479_large

def pellGraphCertificate_479 : PellMatchingCertificate 479 where
  magnitudes := pellMagnitudes_479
  masks := pellMasks_479
  witnesses := pellWitnesses_479
  masks_valid := pellMasks_479_valid
  checked := pellMatching_479_checked
  large := pellMagnitudes_479_large

def pellMagnitudes_487 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_487

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

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

theorem pellMasks_487_valid : ∀ m ∈ pellMasks_487, m.Valid 487 := by
  exact pellLightMasks_valid 487 PellMatchingLightProduction.pellMasks_487 PellMatchingLightProduction.pellMasks_487_valid

theorem pellMatching_487_checked :
    pellMatchingCheck pellMasks_487 pellMagnitudes_487 pellWitnesses_487 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_487
    PellMatchingLightProduction.pellMagnitudes_487 PellMatchingLightProduction.pellWitnesses_487).symm.trans
      PellMatchingLightProduction.pellMatching_487_checked

theorem pellMagnitudes_487_large : ∀ x ∈ pellMagnitudes_487, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_487 PellMatchingLightProduction.pellMagnitudes_487_large

def pellGraphCertificate_487 : PellMatchingCertificate 487 where
  magnitudes := pellMagnitudes_487
  masks := pellMasks_487
  witnesses := pellWitnesses_487
  masks_valid := pellMasks_487_valid
  checked := pellMatching_487_checked
  large := pellMagnitudes_487_large

def pellMagnitudes_503 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_503

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

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

theorem pellMasks_503_valid : ∀ m ∈ pellMasks_503, m.Valid 503 := by
  exact pellLightMasks_valid 503 PellMatchingLightProduction.pellMasks_503 PellMatchingLightProduction.pellMasks_503_valid

theorem pellMatching_503_checked :
    pellMatchingCheck pellMasks_503 pellMagnitudes_503 pellWitnesses_503 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_503
    PellMatchingLightProduction.pellMagnitudes_503 PellMatchingLightProduction.pellWitnesses_503).symm.trans
      PellMatchingLightProduction.pellMatching_503_checked

theorem pellMagnitudes_503_large : ∀ x ∈ pellMagnitudes_503, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_503 PellMatchingLightProduction.pellMagnitudes_503_large

def pellGraphCertificate_503 : PellMatchingCertificate 503 where
  magnitudes := pellMagnitudes_503
  masks := pellMasks_503
  witnesses := pellWitnesses_503
  masks_valid := pellMasks_503_valid
  checked := pellMatching_503_checked
  large := pellMagnitudes_503_large

def pellMagnitudes_511 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_511

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

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

theorem pellMasks_511_valid : ∀ m ∈ pellMasks_511, m.Valid 511 := by
  exact pellLightMasks_valid 511 PellMatchingLightProduction.pellMasks_511 PellMatchingLightProduction.pellMasks_511_valid

theorem pellMatching_511_checked :
    pellMatchingCheck pellMasks_511 pellMagnitudes_511 pellWitnesses_511 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_511
    PellMatchingLightProduction.pellMagnitudes_511 PellMatchingLightProduction.pellWitnesses_511).symm.trans
      PellMatchingLightProduction.pellMatching_511_checked

theorem pellMagnitudes_511_large : ∀ x ∈ pellMagnitudes_511, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_511 PellMatchingLightProduction.pellMagnitudes_511_large

def pellGraphCertificate_511 : PellMatchingCertificate 511 where
  magnitudes := pellMagnitudes_511
  masks := pellMasks_511
  witnesses := pellWitnesses_511
  masks_valid := pellMasks_511_valid
  checked := pellMatching_511_checked
  large := pellMagnitudes_511_large

def pellMagnitudes_527 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_527

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

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

theorem pellMasks_527_valid : ∀ m ∈ pellMasks_527, m.Valid 527 := by
  exact pellLightMasks_valid 527 PellMatchingLightProduction.pellMasks_527 PellMatchingLightProduction.pellMasks_527_valid

theorem pellMatching_527_checked :
    pellMatchingCheck pellMasks_527 pellMagnitudes_527 pellWitnesses_527 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_527
    PellMatchingLightProduction.pellMagnitudes_527 PellMatchingLightProduction.pellWitnesses_527).symm.trans
      PellMatchingLightProduction.pellMatching_527_checked

theorem pellMagnitudes_527_large : ∀ x ∈ pellMagnitudes_527, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_527 PellMatchingLightProduction.pellMagnitudes_527_large

def pellGraphCertificate_527 : PellMatchingCertificate 527 where
  magnitudes := pellMagnitudes_527
  masks := pellMasks_527
  witnesses := pellWitnesses_527
  masks_valid := pellMasks_527_valid
  checked := pellMatching_527_checked
  large := pellMagnitudes_527_large

def pellMagnitudes_599 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_599

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

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

theorem pellMasks_599_valid : ∀ m ∈ pellMasks_599, m.Valid 599 := by
  exact pellLightMasks_valid 599 PellMatchingLightProduction.pellMasks_599 PellMatchingLightProduction.pellMasks_599_valid

theorem pellMatching_599_checked :
    pellMatchingCheck pellMasks_599 pellMagnitudes_599 pellWitnesses_599 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_599
    PellMatchingLightProduction.pellMagnitudes_599 PellMatchingLightProduction.pellWitnesses_599).symm.trans
      PellMatchingLightProduction.pellMatching_599_checked

theorem pellMagnitudes_599_large : ∀ x ∈ pellMagnitudes_599, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_599 PellMatchingLightProduction.pellMagnitudes_599_large

def pellGraphCertificate_599 : PellMatchingCertificate 599 where
  magnitudes := pellMagnitudes_599
  masks := pellMasks_599
  witnesses := pellWitnesses_599
  masks_valid := pellMasks_599_valid
  checked := pellMatching_599_checked
  large := pellMagnitudes_599_large

def pellMagnitudes_607 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_607

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

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

theorem pellMasks_607_valid : ∀ m ∈ pellMasks_607, m.Valid 607 := by
  exact pellLightMasks_valid 607 PellMatchingLightProduction.pellMasks_607 PellMatchingLightProduction.pellMasks_607_valid

theorem pellMatching_607_checked :
    pellMatchingCheck pellMasks_607 pellMagnitudes_607 pellWitnesses_607 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_607
    PellMatchingLightProduction.pellMagnitudes_607 PellMatchingLightProduction.pellWitnesses_607).symm.trans
      PellMatchingLightProduction.pellMatching_607_checked

theorem pellMagnitudes_607_large : ∀ x ∈ pellMagnitudes_607, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_607 PellMatchingLightProduction.pellMagnitudes_607_large

def pellGraphCertificate_607 : PellMatchingCertificate 607 where
  magnitudes := pellMagnitudes_607
  masks := pellMasks_607
  witnesses := pellWitnesses_607
  masks_valid := pellMasks_607_valid
  checked := pellMatching_607_checked
  large := pellMagnitudes_607_large

def pellMagnitudes_623 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_623

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

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

theorem pellMasks_623_valid : ∀ m ∈ pellMasks_623, m.Valid 623 := by
  exact pellLightMasks_valid 623 PellMatchingLightProduction.pellMasks_623 PellMatchingLightProduction.pellMasks_623_valid

theorem pellMatching_623_checked :
    pellMatchingCheck pellMasks_623 pellMagnitudes_623 pellWitnesses_623 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_623
    PellMatchingLightProduction.pellMagnitudes_623 PellMatchingLightProduction.pellWitnesses_623).symm.trans
      PellMatchingLightProduction.pellMatching_623_checked

theorem pellMagnitudes_623_large : ∀ x ∈ pellMagnitudes_623, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_623 PellMatchingLightProduction.pellMagnitudes_623_large

def pellGraphCertificate_623 : PellMatchingCertificate 623 where
  magnitudes := pellMagnitudes_623
  masks := pellMasks_623
  witnesses := pellWitnesses_623
  masks_valid := pellMasks_623_valid
  checked := pellMatching_623_checked
  large := pellMagnitudes_623_large

def pellMagnitudes_631 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_631

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

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

theorem pellMasks_631_valid : ∀ m ∈ pellMasks_631, m.Valid 631 := by
  exact pellLightMasks_valid 631 PellMatchingLightProduction.pellMasks_631 PellMatchingLightProduction.pellMasks_631_valid

theorem pellMatching_631_checked :
    pellMatchingCheck pellMasks_631 pellMagnitudes_631 pellWitnesses_631 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_631
    PellMatchingLightProduction.pellMagnitudes_631 PellMatchingLightProduction.pellWitnesses_631).symm.trans
      PellMatchingLightProduction.pellMatching_631_checked

theorem pellMagnitudes_631_large : ∀ x ∈ pellMagnitudes_631, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_631 PellMatchingLightProduction.pellMagnitudes_631_large

def pellGraphCertificate_631 : PellMatchingCertificate 631 where
  magnitudes := pellMagnitudes_631
  masks := pellMasks_631
  witnesses := pellWitnesses_631
  masks_valid := pellMasks_631_valid
  checked := pellMatching_631_checked
  large := pellMagnitudes_631_large

def pellMagnitudes_647 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_647

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

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

theorem pellMasks_647_valid : ∀ m ∈ pellMasks_647, m.Valid 647 := by
  exact pellLightMasks_valid 647 PellMatchingLightProduction.pellMasks_647 PellMatchingLightProduction.pellMasks_647_valid































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































end D1Bound5
end