Pell Light All Matching Certificates 003

import Init
import Mathlib.Data.List.Defs
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_002
import Definitions.Def_D1Bound5_PellLightMatchingBridge_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField287_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField311_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField359_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField367_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField383_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField391_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField431_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField439_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField463_Definitions
import Definitions.Def_D1Bound5_PellLightMatchingField479_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 pellWitnesses_287 : List (List (ℕ × ℕ)) :=
  PellMatchingLightProduction.pellWitnesses_287

theorem pellMasks_287_valid : ∀ m ∈ pellMasks_287, m.Valid 287 := by
  exact pellLightMasks_valid 287 PellMatchingLightProduction.pellMasks_287 PellMatchingLightProduction.pellMasks_287_valid

theorem pellMatching_287_checked :
    pellMatchingCheck pellMasks_287 pellMagnitudes_287 pellWitnesses_287 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_287
    PellMatchingLightProduction.pellMagnitudes_287 PellMatchingLightProduction.pellWitnesses_287).symm.trans
      PellMatchingLightProduction.pellMatching_287_checked

theorem pellMagnitudes_287_large : ∀ x ∈ pellMagnitudes_287, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_287 PellMatchingLightProduction.pellMagnitudes_287_large

def pellGraphCertificate_287 : PellMatchingCertificate 287 where
  magnitudes := pellMagnitudes_287
  masks := pellMasks_287
  witnesses := pellWitnesses_287
  masks_valid := pellMasks_287_valid
  checked := pellMatching_287_checked
  large := pellMagnitudes_287_large

def pellMagnitudes_311 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_311

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

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

theorem pellMasks_311_valid : ∀ m ∈ pellMasks_311, m.Valid 311 := by
  exact pellLightMasks_valid 311 PellMatchingLightProduction.pellMasks_311 PellMatchingLightProduction.pellMasks_311_valid

theorem pellMatching_311_checked :
    pellMatchingCheck pellMasks_311 pellMagnitudes_311 pellWitnesses_311 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_311
    PellMatchingLightProduction.pellMagnitudes_311 PellMatchingLightProduction.pellWitnesses_311).symm.trans
      PellMatchingLightProduction.pellMatching_311_checked

theorem pellMagnitudes_311_large : ∀ x ∈ pellMagnitudes_311, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_311 PellMatchingLightProduction.pellMagnitudes_311_large

def pellGraphCertificate_311 : PellMatchingCertificate 311 where
  magnitudes := pellMagnitudes_311
  masks := pellMasks_311
  witnesses := pellWitnesses_311
  masks_valid := pellMasks_311_valid
  checked := pellMatching_311_checked
  large := pellMagnitudes_311_large

def pellMagnitudes_359 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_359

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

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

theorem pellMasks_359_valid : ∀ m ∈ pellMasks_359, m.Valid 359 := by
  exact pellLightMasks_valid 359 PellMatchingLightProduction.pellMasks_359 PellMatchingLightProduction.pellMasks_359_valid

theorem pellMatching_359_checked :
    pellMatchingCheck pellMasks_359 pellMagnitudes_359 pellWitnesses_359 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_359
    PellMatchingLightProduction.pellMagnitudes_359 PellMatchingLightProduction.pellWitnesses_359).symm.trans
      PellMatchingLightProduction.pellMatching_359_checked

theorem pellMagnitudes_359_large : ∀ x ∈ pellMagnitudes_359, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_359 PellMatchingLightProduction.pellMagnitudes_359_large

def pellGraphCertificate_359 : PellMatchingCertificate 359 where
  magnitudes := pellMagnitudes_359
  masks := pellMasks_359
  witnesses := pellWitnesses_359
  masks_valid := pellMasks_359_valid
  checked := pellMatching_359_checked
  large := pellMagnitudes_359_large

def pellMagnitudes_367 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_367

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

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

theorem pellMasks_367_valid : ∀ m ∈ pellMasks_367, m.Valid 367 := by
  exact pellLightMasks_valid 367 PellMatchingLightProduction.pellMasks_367 PellMatchingLightProduction.pellMasks_367_valid

theorem pellMatching_367_checked :
    pellMatchingCheck pellMasks_367 pellMagnitudes_367 pellWitnesses_367 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_367
    PellMatchingLightProduction.pellMagnitudes_367 PellMatchingLightProduction.pellWitnesses_367).symm.trans
      PellMatchingLightProduction.pellMatching_367_checked

theorem pellMagnitudes_367_large : ∀ x ∈ pellMagnitudes_367, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_367 PellMatchingLightProduction.pellMagnitudes_367_large

def pellGraphCertificate_367 : PellMatchingCertificate 367 where
  magnitudes := pellMagnitudes_367
  masks := pellMasks_367
  witnesses := pellWitnesses_367
  masks_valid := pellMasks_367_valid
  checked := pellMatching_367_checked
  large := pellMagnitudes_367_large

def pellMagnitudes_383 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_383

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

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

theorem pellMasks_383_valid : ∀ m ∈ pellMasks_383, m.Valid 383 := by
  exact pellLightMasks_valid 383 PellMatchingLightProduction.pellMasks_383 PellMatchingLightProduction.pellMasks_383_valid

theorem pellMatching_383_checked :
    pellMatchingCheck pellMasks_383 pellMagnitudes_383 pellWitnesses_383 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_383
    PellMatchingLightProduction.pellMagnitudes_383 PellMatchingLightProduction.pellWitnesses_383).symm.trans
      PellMatchingLightProduction.pellMatching_383_checked

theorem pellMagnitudes_383_large : ∀ x ∈ pellMagnitudes_383, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_383 PellMatchingLightProduction.pellMagnitudes_383_large

def pellGraphCertificate_383 : PellMatchingCertificate 383 where
  magnitudes := pellMagnitudes_383
  masks := pellMasks_383
  witnesses := pellWitnesses_383
  masks_valid := pellMasks_383_valid
  checked := pellMatching_383_checked
  large := pellMagnitudes_383_large

def pellMagnitudes_391 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_391

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

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

theorem pellMasks_391_valid : ∀ m ∈ pellMasks_391, m.Valid 391 := by
  exact pellLightMasks_valid 391 PellMatchingLightProduction.pellMasks_391 PellMatchingLightProduction.pellMasks_391_valid

theorem pellMatching_391_checked :
    pellMatchingCheck pellMasks_391 pellMagnitudes_391 pellWitnesses_391 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_391
    PellMatchingLightProduction.pellMagnitudes_391 PellMatchingLightProduction.pellWitnesses_391).symm.trans
      PellMatchingLightProduction.pellMatching_391_checked

theorem pellMagnitudes_391_large : ∀ x ∈ pellMagnitudes_391, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_391 PellMatchingLightProduction.pellMagnitudes_391_large

def pellGraphCertificate_391 : PellMatchingCertificate 391 where
  magnitudes := pellMagnitudes_391
  masks := pellMasks_391
  witnesses := pellWitnesses_391
  masks_valid := pellMasks_391_valid
  checked := pellMatching_391_checked
  large := pellMagnitudes_391_large

def pellMagnitudes_431 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_431

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

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

theorem pellMasks_431_valid : ∀ m ∈ pellMasks_431, m.Valid 431 := by
  exact pellLightMasks_valid 431 PellMatchingLightProduction.pellMasks_431 PellMatchingLightProduction.pellMasks_431_valid

theorem pellMatching_431_checked :
    pellMatchingCheck pellMasks_431 pellMagnitudes_431 pellWitnesses_431 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_431
    PellMatchingLightProduction.pellMagnitudes_431 PellMatchingLightProduction.pellWitnesses_431).symm.trans
      PellMatchingLightProduction.pellMatching_431_checked

theorem pellMagnitudes_431_large : ∀ x ∈ pellMagnitudes_431, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_431 PellMatchingLightProduction.pellMagnitudes_431_large

def pellGraphCertificate_431 : PellMatchingCertificate 431 where
  magnitudes := pellMagnitudes_431
  masks := pellMasks_431
  witnesses := pellWitnesses_431
  masks_valid := pellMasks_431_valid
  checked := pellMatching_431_checked
  large := pellMagnitudes_431_large

def pellMagnitudes_439 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_439

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

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

theorem pellMasks_439_valid : ∀ m ∈ pellMasks_439, m.Valid 439 := by
  exact pellLightMasks_valid 439 PellMatchingLightProduction.pellMasks_439 PellMatchingLightProduction.pellMasks_439_valid

theorem pellMatching_439_checked :
    pellMatchingCheck pellMasks_439 pellMagnitudes_439 pellWitnesses_439 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_439
    PellMatchingLightProduction.pellMagnitudes_439 PellMatchingLightProduction.pellWitnesses_439).symm.trans
      PellMatchingLightProduction.pellMatching_439_checked

theorem pellMagnitudes_439_large : ∀ x ∈ pellMagnitudes_439, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_439 PellMatchingLightProduction.pellMagnitudes_439_large

def pellGraphCertificate_439 : PellMatchingCertificate 439 where
  magnitudes := pellMagnitudes_439
  masks := pellMasks_439
  witnesses := pellWitnesses_439
  masks_valid := pellMasks_439_valid
  checked := pellMatching_439_checked
  large := pellMagnitudes_439_large

def pellMagnitudes_463 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_463

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

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

theorem pellMasks_463_valid : ∀ m ∈ pellMasks_463, m.Valid 463 := by
  exact pellLightMasks_valid 463 PellMatchingLightProduction.pellMasks_463 PellMatchingLightProduction.pellMasks_463_valid

theorem pellMatching_463_checked :
    pellMatchingCheck pellMasks_463 pellMagnitudes_463 pellWitnesses_463 = true := by
  exact (pellLightMatchingCheck_eq PellMatchingLightProduction.pellMasks_463
    PellMatchingLightProduction.pellMagnitudes_463 PellMatchingLightProduction.pellWitnesses_463).symm.trans
      PellMatchingLightProduction.pellMatching_463_checked

theorem pellMagnitudes_463_large : ∀ x ∈ pellMagnitudes_463, 2 ≤ x := by
  exact pellLightMagnitudes_large PellMatchingLightProduction.pellMagnitudes_463 PellMatchingLightProduction.pellMagnitudes_463_large

def pellGraphCertificate_463 : PellMatchingCertificate 463 where
  magnitudes := pellMagnitudes_463
  masks := pellMasks_463
  witnesses := pellWitnesses_463
  masks_valid := pellMasks_463_valid
  checked := pellMatching_463_checked
  large := pellMagnitudes_463_large

def pellMagnitudes_479 : List ℤ :=
  PellMatchingLightProduction.pellMagnitudes_479

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

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































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































end D1Bound5
end