Pell Light All Finite Certificates 002

import Init
import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Group.Int.Units
import Mathlib.Algebra.Polynomial.Monic
import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Algebra.Squarefree.Basic
import Mathlib.Analysis.Complex.Norm
import Mathlib.Data.Finset.Card
import Mathlib.Data.Fintype.EquivFin
import Mathlib.Data.Int.GCD
import Mathlib.Data.Int.Sqrt
import Mathlib.Data.List.Defs
import Mathlib.Data.Rat.Lemmas
import Mathlib.Data.ZMod.Basic
import Mathlib.LinearAlgebra.Dimension.Free
import Mathlib.NumberTheory.DiophantineApproximation.Basic
import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
import Mathlib.NumberTheory.NumberField.Norm
import Mathlib.NumberTheory.Real.Irrational
import Mathlib.RingTheory.Coprime.Lemmas
import Mathlib.RingTheory.Int.Basic
import Mathlib.Tactic
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_PellFiniteCertificate_Definitions
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_004
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_005
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_006
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_007
import Definitions.Def_D1Bound5_PellLightCF_Definitions
import Definitions.Def_D1Bound5_PellLightFiniteAdapter_Definitions
import Definitions.Def_D1Bound5_PellLightPrefixData4_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData5_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData5_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData6_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData6_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData7_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData7_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData8_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData8_Definitions_002
import Definitions.Def_D1Bound5_PellMatchingCheck_Definitions

section
namespace D1Bound5
set_option maxRecDepth 32768
set_option maxHeartbeats 12000000

































































































































def pellFiniteCertificate_607 : PellFiniteCertificate 607 (10^275) :=
  pellFiniteCertificateOfLight 607 (10^275) 24 571 pellGraphCertificate_607 (by
    change pellLightFiniteCheck 607 24 (10^275) 571 PellLightProduction.magnitudes_607 = true
    exact PellLightProduction.checked_607)

def pellFiniteCertificate_615 : PellFiniteCertificate 615 (10^275) :=
  pellFiniteCertificateOfLight 615 (10^275) 24 459 (pellEmptyMatchingCertificate 615) (by
    change pellLightFiniteCheck 615 24 (10^275) 459 PellLightProduction.magnitudes_615 = true
    exact PellLightProduction.checked_615)

def pellFiniteCertificate_623 : PellFiniteCertificate 623 (10^275) :=
  pellFiniteCertificateOfLight 623 (10^275) 24 354 pellGraphCertificate_623 (by
    change pellLightFiniteCheck 623 24 (10^275) 354 PellLightProduction.magnitudes_623 = true
    exact PellLightProduction.checked_623)

def pellFiniteCertificate_631 : PellFiniteCertificate 631 (10^275) :=
  pellFiniteCertificateOfLight 631 (10^275) 25 575 pellGraphCertificate_631 (by
    change pellLightFiniteCheck 631 25 (10^275) 575 PellLightProduction.magnitudes_631 = true
    exact PellLightProduction.checked_631)

def pellFiniteCertificate_647 : PellFiniteCertificate 647 (10^275) :=
  pellFiniteCertificateOfLight 647 (10^275) 25 525 pellGraphCertificate_647 (by
    change pellLightFiniteCheck 647 25 (10^275) 525 PellLightProduction.magnitudes_647 = true
    exact PellLightProduction.checked_647)

def pellFiniteCertificate_655 : PellFiniteCertificate 655 (10^275) :=
  pellFiniteCertificateOfLight 655 (10^275) 25 480 (pellEmptyMatchingCertificate 655) (by
    change pellLightFiniteCheck 655 25 (10^275) 480 PellLightProduction.magnitudes_655 = true
    exact PellLightProduction.checked_655)

def pellFiniteCertificate_663 : PellFiniteCertificate 663 (10^275) :=
  pellFiniteCertificateOfLight 663 (10^275) 25 475 (pellEmptyMatchingCertificate 663) (by
    change pellLightFiniteCheck 663 25 (10^275) 475 PellLightProduction.magnitudes_663 = true
    exact PellLightProduction.checked_663)

def pellFiniteCertificate_671 : PellFiniteCertificate 671 (10^275) :=
  pellFiniteCertificateOfLight 671 (10^275) 25 540 (pellEmptyMatchingCertificate 671) (by
    change pellLightFiniteCheck 671 25 (10^275) 540 PellLightProduction.magnitudes_671 = true
    exact PellLightProduction.checked_671)

def pellFiniteCertificate_679 : PellFiniteCertificate 679 (10^275) :=
  pellFiniteCertificateOfLight 679 (10^275) 26 416 pellGraphCertificate_679 (by
    change pellLightFiniteCheck 679 26 (10^275) 416 PellLightProduction.magnitudes_679 = true
    exact PellLightProduction.checked_679)

def pellFiniteCertificate_687 : PellFiniteCertificate 687 (10^275) :=
  pellFiniteCertificateOfLight 687 (10^275) 26 499 (pellEmptyMatchingCertificate 687) (by
    change pellLightFiniteCheck 687 26 (10^275) 499 PellLightProduction.magnitudes_687 = true
    exact PellLightProduction.checked_687)

def pellFiniteCertificate_695 : PellFiniteCertificate 695 (10^275) :=
  pellFiniteCertificateOfLight 695 (10^275) 26 456 (pellEmptyMatchingCertificate 695) (by
    change pellLightFiniteCheck 695 26 (10^275) 456 PellLightProduction.magnitudes_695 = true
    exact PellLightProduction.checked_695)

def pellFiniteCertificate_703 : PellFiniteCertificate 703 (10^275) :=
  pellFiniteCertificateOfLight 703 (10^275) 26 430 (pellEmptyMatchingCertificate 703) (by
    change pellLightFiniteCheck 703 26 (10^275) 430 PellLightProduction.magnitudes_703 = true
    exact PellLightProduction.checked_703)

def pellFiniteCertificate_719 : PellFiniteCertificate 719 (10^275) :=
  pellFiniteCertificateOfLight 719 (10^275) 26 644 pellGraphCertificate_719 (by
    change pellLightFiniteCheck 719 26 (10^275) 644 PellLightProduction.magnitudes_719 = true
    exact PellLightProduction.checked_719)

def pellFiniteCertificate_727 : PellFiniteCertificate 727 (10^275) :=
  pellFiniteCertificateOfLight 727 (10^275) 26 348 pellGraphCertificate_727 (by
    change pellLightFiniteCheck 727 26 (10^275) 348 PellLightProduction.magnitudes_727 = true
    exact PellLightProduction.checked_727)

def pellFiniteCertificate_743 : PellFiniteCertificate 743 (10^275) :=
  pellFiniteCertificateOfLight 743 (10^275) 27 356 pellGraphCertificate_743 (by
    change pellLightFiniteCheck 743 27 (10^275) 356 PellLightProduction.magnitudes_743 = true
    exact PellLightProduction.checked_743)

def pellFiniteCertificate_751 : PellFiniteCertificate 751 (10^275) :=
  pellFiniteCertificateOfLight 751 (10^275) 27 569 pellGraphCertificate_751 (by
    change pellLightFiniteCheck 751 27 (10^275) 569 PellLightProduction.magnitudes_751 = true
    exact PellLightProduction.checked_751)

def pellFiniteCertificate_759 : PellFiniteCertificate 759 (10^275) :=
  pellFiniteCertificateOfLight 759 (10^275) 27 540 (pellEmptyMatchingCertificate 759) (by
    change pellLightFiniteCheck 759 27 (10^275) 540 PellLightProduction.magnitudes_759 = true
    exact PellLightProduction.checked_759)

def pellFiniteCertificate_767 : PellFiniteCertificate 767 (10^275) :=
  pellFiniteCertificateOfLight 767 (10^275) 27 686 (pellEmptyMatchingCertificate 767) (by
    change pellLightFiniteCheck 767 27 (10^275) 686 PellLightProduction.magnitudes_767 = true
    exact PellLightProduction.checked_767)

def pellFiniteCertificate_791 : PellFiniteCertificate 791 (10^275) :=
  pellFiniteCertificateOfLight 791 (10^275) 28 207 (pellEmptyMatchingCertificate 791) (by
    change pellLightFiniteCheck 791 28 (10^275) 207 PellLightProduction.magnitudes_791 = true
    exact PellLightProduction.checked_791)

def pellFiniteCertificate_799 : PellFiniteCertificate 799 (10^275) :=
  pellFiniteCertificateOfLight 799 (10^275) 28 376 (pellEmptyMatchingCertificate 799) (by
    change pellLightFiniteCheck 799 28 (10^275) 376 PellLightProduction.magnitudes_799 = true
    exact PellLightProduction.checked_799)

def pellFiniteCertificate_807 : PellFiniteCertificate 807 (10^275) :=
  pellFiniteCertificateOfLight 807 (10^275) 28 479 (pellEmptyMatchingCertificate 807) (by
    change pellLightFiniteCheck 807 28 (10^275) 479 PellLightProduction.magnitudes_807 = true
    exact PellLightProduction.checked_807)

def pellFiniteCertificate_815 : PellFiniteCertificate 815 (10^275) :=
  pellFiniteCertificateOfLight 815 (10^275) 28 600 (pellEmptyMatchingCertificate 815) (by
    change pellLightFiniteCheck 815 28 (10^275) 600 PellLightProduction.magnitudes_815 = true
    exact PellLightProduction.checked_815)

def pellFiniteCertificate_823 : PellFiniteCertificate 823 (10^275) :=
  pellFiniteCertificateOfLight 823 (10^275) 28 585 pellGraphCertificate_823 (by
    change pellLightFiniteCheck 823 28 (10^275) 585 PellLightProduction.magnitudes_823 = true
    exact PellLightProduction.checked_823)

def pellFiniteCertificate_831 : PellFiniteCertificate 831 (10^275) :=
  pellFiniteCertificateOfLight 831 (10^275) 28 678 (pellEmptyMatchingCertificate 831) (by
    change pellLightFiniteCheck 831 28 (10^275) 678 PellLightProduction.magnitudes_831 = true
    exact PellLightProduction.checked_831)

def pellFiniteCertificate_839 : PellFiniteCertificate 839 (10^275) :=
  pellFiniteCertificateOfLight 839 (10^275) 28 340 pellGraphCertificate_839 (by
    change pellLightFiniteCheck 839 28 (10^275) 340 PellLightProduction.magnitudes_839 = true
    exact PellLightProduction.checked_839)

def pellFiniteCertificate_863 : PellFiniteCertificate 863 (10^275) :=
  pellFiniteCertificateOfLight 863 (10^275) 29 520 pellGraphCertificate_863 (by
    change pellLightFiniteCheck 863 29 (10^275) 520 PellLightProduction.magnitudes_863 = true
    exact PellLightProduction.checked_863)

def pellFiniteCertificate_871 : PellFiniteCertificate 871 (10^275) :=
  pellFiniteCertificateOfLight 871 (10^275) 29 623 (pellEmptyMatchingCertificate 871) (by
    change pellLightFiniteCheck 871 29 (10^275) 623 PellLightProduction.magnitudes_871 = true
    exact PellLightProduction.checked_871)

def pellFiniteCertificate_879 : PellFiniteCertificate 879 (10^275) :=
  pellFiniteCertificateOfLight 879 (10^275) 29 594 (pellEmptyMatchingCertificate 879) (by
    change pellLightFiniteCheck 879 29 (10^275) 594 PellLightProduction.magnitudes_879 = true
    exact PellLightProduction.checked_879)

def pellFiniteCertificate_887 : PellFiniteCertificate 887 (10^275) :=
  pellFiniteCertificateOfLight 887 (10^275) 29 552 pellGraphCertificate_887 (by
    change pellLightFiniteCheck 887 29 (10^275) 552 PellLightProduction.magnitudes_887 = true
    exact PellLightProduction.checked_887)

def pellFiniteCertificate_895 : PellFiniteCertificate 895 (10^275) :=
  pellFiniteCertificateOfLight 895 (10^275) 29 384 (pellEmptyMatchingCertificate 895) (by
    change pellLightFiniteCheck 895 29 (10^275) 384 PellLightProduction.magnitudes_895 = true
    exact PellLightProduction.checked_895)

def pellFiniteCertificate_903 : PellFiniteCertificate 903 (10^275) :=
  pellFiniteCertificateOfLight 903 (10^275) 30 178 (pellEmptyMatchingCertificate 903) (by
    change pellLightFiniteCheck 903 30 (10^275) 178 PellLightProduction.magnitudes_903 = true
    exact PellLightProduction.checked_903)

def pellFiniteCertificate_911 : PellFiniteCertificate 911 (10^275) :=
  pellFiniteCertificateOfLight 911 (10^275) 30 444 pellGraphCertificate_911 (by
    change pellLightFiniteCheck 911 30 (10^275) 444 PellLightProduction.magnitudes_911 = true
    exact PellLightProduction.checked_911)

def pellFiniteCertificate_919 : PellFiniteCertificate 919 (10^275) :=
  pellFiniteCertificateOfLight 919 (10^275) 30 587 pellGraphCertificate_919 (by
    change pellLightFiniteCheck 919 30 (10^275) 587 PellLightProduction.magnitudes_919 = true
    exact PellLightProduction.checked_919)

def pellFiniteCertificate_935 : PellFiniteCertificate 935 (10^275) :=
  pellFiniteCertificateOfLight 935 (10^275) 30 640 (pellEmptyMatchingCertificate 935) (by
    change pellLightFiniteCheck 935 30 (10^275) 640 PellLightProduction.magnitudes_935 = true
    exact PellLightProduction.checked_935)

def pellFiniteCertificate_943 : PellFiniteCertificate 943 (10^275) :=
  pellFiniteCertificateOfLight 943 (10^275) 30 520 (pellEmptyMatchingCertificate 943) (by
    change pellLightFiniteCheck 943 30 (10^275) 520 PellLightProduction.magnitudes_943 = true
    exact PellLightProduction.checked_943)

def pellFiniteCertificate_951 : PellFiniteCertificate 951 (10^275) :=
  pellFiniteCertificateOfLight 951 (10^275) 30 572 (pellEmptyMatchingCertificate 951) (by
    change pellLightFiniteCheck 951 30 (10^275) 572 PellLightProduction.magnitudes_951 = true
    exact PellLightProduction.checked_951)

def pellFiniteCertificate_959 : PellFiniteCertificate 959 (10^275) :=
  pellFiniteCertificateOfLight 959 (10^275) 30 334 pellGraphCertificate_959 (by
    change pellLightFiniteCheck 959 30 (10^275) 334 PellLightProduction.magnitudes_959 = true
    exact PellLightProduction.checked_959)

def pellFiniteCertificate_967 : PellFiniteCertificate 967 (10^275) :=
  pellFiniteCertificateOfLight 967 (10^275) 31 464 pellGraphCertificate_967 (by
    change pellLightFiniteCheck 967 31 (10^275) 464 PellLightProduction.magnitudes_967 = true
    exact PellLightProduction.checked_967)

def pellFiniteCertificate_983 : PellFiniteCertificate 983 (10^275) :=
  pellFiniteCertificateOfLight 983 (10^275) 31 381 pellGraphCertificate_983 (by
    change pellLightFiniteCheck 983 31 (10^275) 381 PellLightProduction.magnitudes_983 = true
    exact PellLightProduction.checked_983)

def pellFiniteCertificate_991 : PellFiniteCertificate 991 (10^275) :=
  pellFiniteCertificateOfLight 991 (10^275) 31 550 pellGraphCertificate_991 (by
    change pellLightFiniteCheck 991 31 (10^275) 550 PellLightProduction.magnitudes_991 = true
    exact PellLightProduction.checked_991)

def pellFiniteCertificate_1007 : PellFiniteCertificate 1007 (10^275) :=
  pellFiniteCertificateOfLight 1007 (10^275) 31 552 (pellEmptyMatchingCertificate 1007) (by
    change pellLightFiniteCheck 1007 31 (10^275) 552 PellLightProduction.magnitudes_1007 = true
    exact PellLightProduction.checked_1007)

def pellFiniteCertificate_1015 : PellFiniteCertificate 1015 (10^275) :=
  pellFiniteCertificateOfLight 1015 (10^275) 31 376 (pellEmptyMatchingCertificate 1015) (by
    change pellLightFiniteCheck 1015 31 (10^275) 376 PellLightProduction.magnitudes_1015 = true
    exact PellLightProduction.checked_1015)

def pellFiniteCertificate_1023 : PellFiniteCertificate 1023 (10^275) :=
  pellFiniteCertificateOfLight 1023 (10^275) 31 304 (pellEmptyMatchingCertificate 1023) (by
    change pellLightFiniteCheck 1023 31 (10^275) 304 PellLightProduction.magnitudes_1023 = true
    exact PellLightProduction.checked_1023)

def pellFiniteCertificate_1031 : PellFiniteCertificate 1031 (10^275) :=
  pellFiniteCertificateOfLight 1031 (10^275) 32 506 pellGraphCertificate_1031 (by
    change pellLightFiniteCheck 1031 32 (10^275) 506 PellLightProduction.magnitudes_1031 = true
    exact PellLightProduction.checked_1031)

def pellFiniteCertificate_1039 : PellFiniteCertificate 1039 (10^275) :=
  pellFiniteCertificateOfLight 1039 (10^275) 32 569 pellGraphCertificate_1039 (by
    change pellLightFiniteCheck 1039 32 (10^275) 569 PellLightProduction.magnitudes_1039 = true
    exact PellLightProduction.checked_1039)

def pellFiniteCertificate_1047 : PellFiniteCertificate 1047 (10^275) :=
  pellFiniteCertificateOfLight 1047 (10^275) 32 505 (pellEmptyMatchingCertificate 1047) (by
    change pellLightFiniteCheck 1047 32 (10^275) 505 PellLightProduction.magnitudes_1047 = true
    exact PellLightProduction.checked_1047)

def pellFiniteCertificate_1055 : PellFiniteCertificate 1055 (10^275) :=
  pellFiniteCertificateOfLight 1055 (10^275) 32 312 (pellEmptyMatchingCertificate 1055) (by
    change pellLightFiniteCheck 1055 32 (10^275) 312 PellLightProduction.magnitudes_1055 = true
    exact PellLightProduction.checked_1055)

def pellFiniteCertificate_1063 : PellFiniteCertificate 1063 (10^275) :=
  pellFiniteCertificateOfLight 1063 (10^275) 32 563 pellGraphCertificate_1063 (by
    change pellLightFiniteCheck 1063 32 (10^275) 563 PellLightProduction.magnitudes_1063 = true
    exact PellLightProduction.checked_1063)

def pellFiniteCertificate_1079 : PellFiniteCertificate 1079 (10^275) :=
  pellFiniteCertificateOfLight 1079 (10^275) 32 640 (pellEmptyMatchingCertificate 1079) (by
    change pellLightFiniteCheck 1079 32 (10^275) 640 PellLightProduction.magnitudes_1079 = true
    exact PellLightProduction.checked_1079)

def pellFiniteCertificate_1087 : PellFiniteCertificate 1087 (10^275) :=
  pellFiniteCertificateOfLight 1087 (10^275) 32 328 pellGraphCertificate_1087 (by
    change pellLightFiniteCheck 1087 32 (10^275) 328 PellLightProduction.magnitudes_1087 = true
    exact PellLightProduction.checked_1087)

def pellFiniteCertificate_1095 : PellFiniteCertificate 1095 (10^275) :=
  pellFiniteCertificateOfLight 1095 (10^275) 33 192 (pellEmptyMatchingCertificate 1095) (by
    change pellLightFiniteCheck 1095 33 (10^275) 192 PellLightProduction.magnitudes_1095 = true
    exact PellLightProduction.checked_1095)

def pellFiniteCertificate_1103 : PellFiniteCertificate 1103 (10^275) :=
  pellFiniteCertificateOfLight 1103 (10^275) 33 518 pellGraphCertificate_1103 (by
    change pellLightFiniteCheck 1103 33 (10^275) 518 PellLightProduction.magnitudes_1103 = true
    exact PellLightProduction.checked_1103)

def pellFiniteCertificate_1111 : PellFiniteCertificate 1111 (10^275) :=
  pellFiniteCertificateOfLight 1111 (10^275) 33 238 (pellEmptyMatchingCertificate 1111) (by
    change pellLightFiniteCheck 1111 33 (10^275) 238 PellLightProduction.magnitudes_1111 = true
    exact PellLightProduction.checked_1111)

def pellFiniteCertificate_1119 : PellFiniteCertificate 1119 (10^275) :=
  pellFiniteCertificateOfLight 1119 (10^275) 33 492 (pellEmptyMatchingCertificate 1119) (by
    change pellLightFiniteCheck 1119 33 (10^275) 492 PellLightProduction.magnitudes_1119 = true
    exact PellLightProduction.checked_1119)

def pellFiniteCertificate_1135 : PellFiniteCertificate 1135 (10^275) :=
  pellFiniteCertificateOfLight 1135 (10^275) 33 658 (pellEmptyMatchingCertificate 1135) (by
    change pellLightFiniteCheck 1135 33 (10^275) 658 PellLightProduction.magnitudes_1135 = true
    exact PellLightProduction.checked_1135)

def pellFiniteCertificate_1151 : PellFiniteCertificate 1151 (10^275) :=
  pellFiniteCertificateOfLight 1151 (10^275) 33 493 pellGraphCertificate_1151 (by
    change pellLightFiniteCheck 1151 33 (10^275) 493 PellLightProduction.magnitudes_1151 = true
    exact PellLightProduction.checked_1151)

def pellFiniteCertificate_1159 : PellFiniteCertificate 1159 (10^275) :=
  pellFiniteCertificateOfLight 1159 (10^275) 34 460 (pellEmptyMatchingCertificate 1159) (by
    change pellLightFiniteCheck 1159 34 (10^275) 460 PellLightProduction.magnitudes_1159 = true
    exact PellLightProduction.checked_1159)

def pellFiniteCertificate_1167 : PellFiniteCertificate 1167 (10^275) :=
  pellFiniteCertificateOfLight 1167 (10^275) 34 281 (pellEmptyMatchingCertificate 1167) (by
    change pellLightFiniteCheck 1167 34 (10^275) 281 PellLightProduction.magnitudes_1167 = true
    exact PellLightProduction.checked_1167)

def pellFiniteCertificate_1191 : PellFiniteCertificate 1191 (10^275) :=
  pellFiniteCertificateOfLight 1191 (10^275) 34 432 (pellEmptyMatchingCertificate 1191) (by
    change pellLightFiniteCheck 1191 34 (10^275) 432 PellLightProduction.magnitudes_1191 = true
    exact PellLightProduction.checked_1191)

def pellFiniteCertificate_1199 : PellFiniteCertificate 1199 (10^275) :=
  pellFiniteCertificateOfLight 1199 (10^275) 34 549 (pellEmptyMatchingCertificate 1199) (by
    change pellLightFiniteCheck 1199 34 (10^275) 549 PellLightProduction.magnitudes_1199 = true
    exact PellLightProduction.checked_1199)

def pellFiniteCertificate_1207 : PellFiniteCertificate 1207 (10^275) :=
  pellFiniteCertificateOfLight 1207 (10^275) 34 516 pellGraphCertificate_1207 (by
    change pellLightFiniteCheck 1207 34 (10^275) 516 PellLightProduction.magnitudes_1207 = true
    exact PellLightProduction.checked_1207)

def pellFiniteCertificate_1223 : PellFiniteCertificate 1223 (10^275) :=
  pellFiniteCertificateOfLight 1223 (10^275) 34 324 pellGraphCertificate_1223 (by
    change pellLightFiniteCheck 1223 34 (10^275) 324 PellLightProduction.magnitudes_1223 = true
    exact PellLightProduction.checked_1223)

def pellFiniteCertificate_1231 : PellFiniteCertificate 1231 (10^275) :=
  pellFiniteCertificateOfLight 1231 (10^275) 35 489 pellGraphCertificate_1231 (by
    change pellLightFiniteCheck 1231 35 (10^275) 489 PellLightProduction.magnitudes_1231 = true
    exact PellLightProduction.checked_1231)

def pellFiniteCertificate_1239 : PellFiniteCertificate 1239 (10^275) :=
  pellFiniteCertificateOfLight 1239 (10^275) 35 216 (pellEmptyMatchingCertificate 1239) (by
    change pellLightFiniteCheck 1239 35 (10^275) 216 PellLightProduction.magnitudes_1239 = true
    exact PellLightProduction.checked_1239)

















































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































end D1Bound5
end