Pell Light All Finite Certificates 001

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_001
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_002
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_003
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_004
import Definitions.Def_D1Bound5_PellLightCF_Definitions
import Definitions.Def_D1Bound5_PellLightFiniteAdapter_Definitions
import Definitions.Def_D1Bound5_PellLightPrefixData1_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData1_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData2_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData2_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData3_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData3_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData4_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData4_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixPilot_Definitions
import Definitions.Def_D1Bound5_PellMatchingCheck_Definitions

section
namespace D1Bound5
set_option maxRecDepth 32768
set_option maxHeartbeats 12000000

def pellFiniteCertificate_4519 : PellFiniteCertificate 4519 (10^275) :=
  pellFiniteCertificateOfLight 4519 (10^275) 67 540 pellGraphCertificate_4519 (by
    change pellLightFiniteCheck 4519 67 (10^275) 540 PellLightProduction.magnitudes_4519 = true
    exact PellLightProduction.checked_4519)

def pellFiniteCertificate_7 : PellFiniteCertificate 7 (10^275) :=
  pellFiniteCertificateOfLight 7 (10^275) 2 915 pellGraphCertificate_7 (by
    change pellLightFiniteCheck 7 2 (10^275) 915 PellLightProduction.magnitudes_7 = true
    exact PellLightProduction.checked_7)

def pellFiniteCertificate_15 : PellFiniteCertificate 15 (10^275) :=
  pellFiniteCertificateOfLight 15 (10^275) 3 614 (pellEmptyMatchingCertificate 15) (by
    change pellLightFiniteCheck 15 3 (10^275) 614 PellLightProduction.magnitudes_15 = true
    exact PellLightProduction.checked_15)

def pellFiniteCertificate_23 : PellFiniteCertificate 23 (10^275) :=
  pellFiniteCertificateOfLight 23 (10^275) 4 654 pellGraphCertificate_23 (by
    change pellLightFiniteCheck 23 4 (10^275) 654 PellLightProduction.magnitudes_23 = true
    exact PellLightProduction.checked_23)

def pellFiniteCertificate_31 : PellFiniteCertificate 31 (10^275) :=
  pellFiniteCertificateOfLight 31 (10^275) 5 632 pellGraphCertificate_31 (by
    change pellLightFiniteCheck 31 5 (10^275) 632 PellLightProduction.magnitudes_31 = true
    exact PellLightProduction.checked_31)

def pellFiniteCertificate_39 : PellFiniteCertificate 39 (10^275) :=
  pellFiniteCertificateOfLight 39 (10^275) 6 324 (pellEmptyMatchingCertificate 39) (by
    change pellLightFiniteCheck 39 6 (10^275) 324 PellLightProduction.magnitudes_39 = true
    exact PellLightProduction.checked_39)

def pellFiniteCertificate_47 : PellFiniteCertificate 47 (10^275) :=
  pellFiniteCertificateOfLight 47 (10^275) 6 554 pellGraphCertificate_47 (by
    change pellLightFiniteCheck 47 6 (10^275) 554 PellLightProduction.magnitudes_47 = true
    exact PellLightProduction.checked_47)

def pellFiniteCertificate_55 : PellFiniteCertificate 55 (10^275) :=
  pellFiniteCertificateOfLight 55 (10^275) 7 488 (pellEmptyMatchingCertificate 55) (by
    change pellLightFiniteCheck 55 7 (10^275) 488 PellLightProduction.magnitudes_55 = true
    exact PellLightProduction.checked_55)

def pellFiniteCertificate_71 : PellFiniteCertificate 71 (10^275) :=
  pellFiniteCertificateOfLight 71 (10^275) 8 572 pellGraphCertificate_71 (by
    change pellLightFiniteCheck 71 8 (10^275) 572 PellLightProduction.magnitudes_71 = true
    exact PellLightProduction.checked_71)

def pellFiniteCertificate_79 : PellFiniteCertificate 79 (10^275) :=
  pellFiniteCertificateOfLight 79 (10^275) 8 498 pellGraphCertificate_79 (by
    change pellLightFiniteCheck 79 8 (10^275) 498 PellLightProduction.magnitudes_79 = true
    exact PellLightProduction.checked_79)

def pellFiniteCertificate_87 : PellFiniteCertificate 87 (10^275) :=
  pellFiniteCertificateOfLight 87 (10^275) 9 314 (pellEmptyMatchingCertificate 87) (by
    change pellLightFiniteCheck 87 9 (10^275) 314 PellLightProduction.magnitudes_87 = true
    exact PellLightProduction.checked_87)

def pellFiniteCertificate_95 : PellFiniteCertificate 95 (10^275) :=
  pellFiniteCertificateOfLight 95 (10^275) 9 580 (pellEmptyMatchingCertificate 95) (by
    change pellLightFiniteCheck 95 9 (10^275) 580 PellLightProduction.magnitudes_95 = true
    exact PellLightProduction.checked_95)

def pellFiniteCertificate_103 : PellFiniteCertificate 103 (10^275) :=
  pellFiniteCertificateOfLight 103 (10^275) 10 582 pellGraphCertificate_103 (by
    change pellLightFiniteCheck 103 10 (10^275) 582 PellLightProduction.magnitudes_103 = true
    exact PellLightProduction.checked_103)

def pellFiniteCertificate_111 : PellFiniteCertificate 111 (10^275) :=
  pellFiniteCertificateOfLight 111 (10^275) 10 594 (pellEmptyMatchingCertificate 111) (by
    change pellLightFiniteCheck 111 10 (10^275) 594 PellLightProduction.magnitudes_111 = true
    exact PellLightProduction.checked_111)

def pellFiniteCertificate_119 : PellFiniteCertificate 119 (10^275) :=
  pellFiniteCertificateOfLight 119 (10^275) 10 462 pellGraphCertificate_119 (by
    change pellLightFiniteCheck 119 10 (10^275) 462 PellLightProduction.magnitudes_119 = true
    exact PellLightProduction.checked_119)

def pellFiniteCertificate_127 : PellFiniteCertificate 127 (10^275) :=
  pellFiniteCertificateOfLight 127 (10^275) 11 473 pellGraphCertificate_127 (by
    change pellLightFiniteCheck 127 11 (10^275) 473 PellLightProduction.magnitudes_127 = true
    exact PellLightProduction.checked_127)

def pellFiniteCertificate_143 : PellFiniteCertificate 143 (10^275) :=
  pellFiniteCertificateOfLight 143 (10^275) 11 398 (pellEmptyMatchingCertificate 143) (by
    change pellLightFiniteCheck 143 11 (10^275) 398 PellLightProduction.magnitudes_143 = true
    exact PellLightProduction.checked_143)

def pellFiniteCertificate_151 : PellFiniteCertificate 151 (10^275) :=
  pellFiniteCertificateOfLight 151 (10^275) 12 577 pellGraphCertificate_151 (by
    change pellLightFiniteCheck 151 12 (10^275) 577 PellLightProduction.magnitudes_151 = true
    exact PellLightProduction.checked_151)

def pellFiniteCertificate_159 : PellFiniteCertificate 159 (10^275) :=
  pellFiniteCertificateOfLight 159 (10^275) 12 802 (pellEmptyMatchingCertificate 159) (by
    change pellLightFiniteCheck 159 12 (10^275) 802 PellLightProduction.magnitudes_159 = true
    exact PellLightProduction.checked_159)

def pellFiniteCertificate_167 : PellFiniteCertificate 167 (10^275) :=
  pellFiniteCertificateOfLight 167 (10^275) 12 434 pellGraphCertificate_167 (by
    change pellLightFiniteCheck 167 12 (10^275) 434 PellLightProduction.magnitudes_167 = true
    exact PellLightProduction.checked_167)

def pellFiniteCertificate_183 : PellFiniteCertificate 183 (10^275) :=
  pellFiniteCertificateOfLight 183 (10^275) 13 552 (pellEmptyMatchingCertificate 183) (by
    change pellLightFiniteCheck 183 13 (10^275) 552 PellLightProduction.magnitudes_183 = true
    exact PellLightProduction.checked_183)

def pellFiniteCertificate_191 : PellFiniteCertificate 191 (10^275) :=
  pellFiniteCertificateOfLight 191 (10^275) 13 606 pellGraphCertificate_191 (by
    change pellLightFiniteCheck 191 13 (10^275) 606 PellLightProduction.magnitudes_191 = true
    exact PellLightProduction.checked_191)

def pellFiniteCertificate_199 : PellFiniteCertificate 199 (10^275) :=
  pellFiniteCertificateOfLight 199 (10^275) 14 521 pellGraphCertificate_199 (by
    change pellLightFiniteCheck 199 14 (10^275) 521 PellLightProduction.magnitudes_199 = true
    exact PellLightProduction.checked_199)

def pellFiniteCertificate_215 : PellFiniteCertificate 215 (10^275) :=
  pellFiniteCertificateOfLight 215 (10^275) 14 564 (pellEmptyMatchingCertificate 215) (by
    change pellLightFiniteCheck 215 14 (10^275) 564 PellLightProduction.magnitudes_215 = true
    exact PellLightProduction.checked_215)

def pellFiniteCertificate_223 : PellFiniteCertificate 223 (10^275) :=
  pellFiniteCertificateOfLight 223 (10^275) 14 414 pellGraphCertificate_223 (by
    change pellLightFiniteCheck 223 14 (10^275) 414 PellLightProduction.magnitudes_223 = true
    exact PellLightProduction.checked_223)

def pellFiniteCertificate_231 : PellFiniteCertificate 231 (10^275) :=
  pellFiniteCertificateOfLight 231 (10^275) 15 252 (pellEmptyMatchingCertificate 231) (by
    change pellLightFiniteCheck 231 15 (10^275) 252 PellLightProduction.magnitudes_231 = true
    exact PellLightProduction.checked_231)

def pellFiniteCertificate_239 : PellFiniteCertificate 239 (10^275) :=
  pellFiniteCertificateOfLight 239 (10^275) 15 464 pellGraphCertificate_239 (by
    change pellLightFiniteCheck 239 15 (10^275) 464 PellLightProduction.magnitudes_239 = true
    exact PellLightProduction.checked_239)

def pellFiniteCertificate_247 : PellFiniteCertificate 247 (10^275) :=
  pellFiniteCertificateOfLight 247 (10^275) 15 629 (pellEmptyMatchingCertificate 247) (by
    change pellLightFiniteCheck 247 15 (10^275) 629 PellLightProduction.magnitudes_247 = true
    exact PellLightProduction.checked_247)

def pellFiniteCertificate_255 : PellFiniteCertificate 255 (10^275) :=
  pellFiniteCertificateOfLight 255 (10^275) 15 364 (pellEmptyMatchingCertificate 255) (by
    change pellLightFiniteCheck 255 15 (10^275) 364 PellLightProduction.magnitudes_255 = true
    exact PellLightProduction.checked_255)

def pellFiniteCertificate_263 : PellFiniteCertificate 263 (10^275) :=
  pellFiniteCertificateOfLight 263 (10^275) 16 606 pellGraphCertificate_263 (by
    change pellLightFiniteCheck 263 16 (10^275) 606 PellLightProduction.magnitudes_263 = true
    exact PellLightProduction.checked_263)

def pellFiniteCertificate_271 : PellFiniteCertificate 271 (10^275) :=
  pellFiniteCertificateOfLight 271 (10^275) 16 578 pellGraphCertificate_271 (by
    change pellLightFiniteCheck 271 16 (10^275) 578 PellLightProduction.magnitudes_271 = true
    exact PellLightProduction.checked_271)

def pellFiniteCertificate_287 : PellFiniteCertificate 287 (10^275) :=
  pellFiniteCertificateOfLight 287 (10^275) 16 398 pellGraphCertificate_287 (by
    change pellLightFiniteCheck 287 16 (10^275) 398 PellLightProduction.magnitudes_287 = true
    exact PellLightProduction.checked_287)

def pellFiniteCertificate_295 : PellFiniteCertificate 295 (10^275) :=
  pellFiniteCertificateOfLight 295 (10^275) 17 498 (pellEmptyMatchingCertificate 295) (by
    change pellLightFiniteCheck 295 17 (10^275) 498 PellLightProduction.magnitudes_295 = true
    exact PellLightProduction.checked_295)

def pellFiniteCertificate_303 : PellFiniteCertificate 303 (10^275) :=
  pellFiniteCertificateOfLight 303 (10^275) 17 444 (pellEmptyMatchingCertificate 303) (by
    change pellLightFiniteCheck 303 17 (10^275) 444 PellLightProduction.magnitudes_303 = true
    exact PellLightProduction.checked_303)

def pellFiniteCertificate_311 : PellFiniteCertificate 311 (10^275) :=
  pellFiniteCertificateOfLight 311 (10^275) 17 584 pellGraphCertificate_311 (by
    change pellLightFiniteCheck 311 17 (10^275) 584 PellLightProduction.magnitudes_311 = true
    exact PellLightProduction.checked_311)

def pellFiniteCertificate_319 : PellFiniteCertificate 319 (10^275) :=
  pellFiniteCertificateOfLight 319 (10^275) 17 518 (pellEmptyMatchingCertificate 319) (by
    change pellLightFiniteCheck 319 17 (10^275) 518 PellLightProduction.magnitudes_319 = true
    exact PellLightProduction.checked_319)

def pellFiniteCertificate_327 : PellFiniteCertificate 327 (10^275) :=
  pellFiniteCertificateOfLight 327 (10^275) 18 208 (pellEmptyMatchingCertificate 327) (by
    change pellLightFiniteCheck 327 18 (10^275) 208 PellLightProduction.magnitudes_327 = true
    exact PellLightProduction.checked_327)

def pellFiniteCertificate_335 : PellFiniteCertificate 335 (10^275) :=
  pellFiniteCertificateOfLight 335 (10^275) 18 356 (pellEmptyMatchingCertificate 335) (by
    change pellLightFiniteCheck 335 18 (10^275) 356 PellLightProduction.magnitudes_335 = true
    exact PellLightProduction.checked_335)

def pellFiniteCertificate_359 : PellFiniteCertificate 359 (10^275) :=
  pellFiniteCertificateOfLight 359 (10^275) 18 384 pellGraphCertificate_359 (by
    change pellLightFiniteCheck 359 18 (10^275) 384 PellLightProduction.magnitudes_359 = true
    exact PellLightProduction.checked_359)

def pellFiniteCertificate_367 : PellFiniteCertificate 367 (10^275) :=
  pellFiniteCertificateOfLight 367 (10^275) 19 520 pellGraphCertificate_367 (by
    change pellLightFiniteCheck 367 19 (10^275) 520 PellLightProduction.magnitudes_367 = true
    exact PellLightProduction.checked_367)

def pellFiniteCertificate_383 : PellFiniteCertificate 383 (10^275) :=
  pellFiniteCertificateOfLight 383 (10^275) 19 480 pellGraphCertificate_383 (by
    change pellLightFiniteCheck 383 19 (10^275) 480 PellLightProduction.magnitudes_383 = true
    exact PellLightProduction.checked_383)

def pellFiniteCertificate_391 : PellFiniteCertificate 391 (10^275) :=
  pellFiniteCertificateOfLight 391 (10^275) 19 613 pellGraphCertificate_391 (by
    change pellLightFiniteCheck 391 19 (10^275) 613 PellLightProduction.magnitudes_391 = true
    exact PellLightProduction.checked_391)

def pellFiniteCertificate_399 : PellFiniteCertificate 399 (10^275) :=
  pellFiniteCertificateOfLight 399 (10^275) 19 342 (pellEmptyMatchingCertificate 399) (by
    change pellLightFiniteCheck 399 19 (10^275) 342 PellLightProduction.magnitudes_399 = true
    exact PellLightProduction.checked_399)

def pellFiniteCertificate_407 : PellFiniteCertificate 407 (10^275) :=
  pellFiniteCertificateOfLight 407 (10^275) 20 443 (pellEmptyMatchingCertificate 407) (by
    change pellLightFiniteCheck 407 20 (10^275) 443 PellLightProduction.magnitudes_407 = true
    exact PellLightProduction.checked_407)

def pellFiniteCertificate_415 : PellFiniteCertificate 415 (10^275) :=
  pellFiniteCertificateOfLight 415 (10^275) 20 580 (pellEmptyMatchingCertificate 415) (by
    change pellLightFiniteCheck 415 20 (10^275) 580 PellLightProduction.magnitudes_415 = true
    exact PellLightProduction.checked_415)

def pellFiniteCertificate_431 : PellFiniteCertificate 431 (10^275) :=
  pellFiniteCertificateOfLight 431 (10^275) 20 518 pellGraphCertificate_431 (by
    change pellLightFiniteCheck 431 20 (10^275) 518 PellLightProduction.magnitudes_431 = true
    exact PellLightProduction.checked_431)

def pellFiniteCertificate_439 : PellFiniteCertificate 439 (10^275) :=
  pellFiniteCertificateOfLight 439 (10^275) 20 372 pellGraphCertificate_439 (by
    change pellLightFiniteCheck 439 20 (10^275) 372 PellLightProduction.magnitudes_439 = true
    exact PellLightProduction.checked_439)

def pellFiniteCertificate_447 : PellFiniteCertificate 447 (10^275) :=
  pellFiniteCertificateOfLight 447 (10^275) 21 222 (pellEmptyMatchingCertificate 447) (by
    change pellLightFiniteCheck 447 21 (10^275) 222 PellLightProduction.magnitudes_447 = true
    exact PellLightProduction.checked_447)

def pellFiniteCertificate_455 : PellFiniteCertificate 455 (10^275) :=
  pellFiniteCertificateOfLight 455 (10^275) 21 260 (pellEmptyMatchingCertificate 455) (by
    change pellLightFiniteCheck 455 21 (10^275) 260 PellLightProduction.magnitudes_455 = true
    exact PellLightProduction.checked_455)

def pellFiniteCertificate_463 : PellFiniteCertificate 463 (10^275) :=
  pellFiniteCertificateOfLight 463 (10^275) 21 597 pellGraphCertificate_463 (by
    change pellLightFiniteCheck 463 21 (10^275) 597 PellLightProduction.magnitudes_463 = true
    exact PellLightProduction.checked_463)

def pellFiniteCertificate_471 : PellFiniteCertificate 471 (10^275) :=
  pellFiniteCertificateOfLight 471 (10^275) 21 534 (pellEmptyMatchingCertificate 471) (by
    change pellLightFiniteCheck 471 21 (10^275) 534 PellLightProduction.magnitudes_471 = true
    exact PellLightProduction.checked_471)

def pellFiniteCertificate_479 : PellFiniteCertificate 479 (10^275) :=
  pellFiniteCertificateOfLight 479 (10^275) 21 486 pellGraphCertificate_479 (by
    change pellLightFiniteCheck 479 21 (10^275) 486 PellLightProduction.magnitudes_479 = true
    exact PellLightProduction.checked_479)

def pellFiniteCertificate_487 : PellFiniteCertificate 487 (10^275) :=
  pellFiniteCertificateOfLight 487 (10^275) 22 549 pellGraphCertificate_487 (by
    change pellLightFiniteCheck 487 22 (10^275) 549 PellLightProduction.magnitudes_487 = true
    exact PellLightProduction.checked_487)

def pellFiniteCertificate_503 : PellFiniteCertificate 503 (10^275) :=
  pellFiniteCertificateOfLight 503 (10^275) 22 468 pellGraphCertificate_503 (by
    change pellLightFiniteCheck 503 22 (10^275) 468 PellLightProduction.magnitudes_503 = true
    exact PellLightProduction.checked_503)

def pellFiniteCertificate_511 : PellFiniteCertificate 511 (10^275) :=
  pellFiniteCertificateOfLight 511 (10^275) 22 553 pellGraphCertificate_511 (by
    change pellLightFiniteCheck 511 22 (10^275) 553 PellLightProduction.magnitudes_511 = true
    exact PellLightProduction.checked_511)

def pellFiniteCertificate_519 : PellFiniteCertificate 519 (10^275) :=
  pellFiniteCertificateOfLight 519 (10^275) 22 661 (pellEmptyMatchingCertificate 519) (by
    change pellLightFiniteCheck 519 22 (10^275) 661 PellLightProduction.magnitudes_519 = true
    exact PellLightProduction.checked_519)

def pellFiniteCertificate_527 : PellFiniteCertificate 527 (10^275) :=
  pellFiniteCertificateOfLight 527 (10^275) 22 364 pellGraphCertificate_527 (by
    change pellLightFiniteCheck 527 22 (10^275) 364 PellLightProduction.magnitudes_527 = true
    exact PellLightProduction.checked_527)

def pellFiniteCertificate_535 : PellFiniteCertificate 535 (10^275) :=
  pellFiniteCertificateOfLight 535 (10^275) 23 505 (pellEmptyMatchingCertificate 535) (by
    change pellLightFiniteCheck 535 23 (10^275) 505 PellLightProduction.magnitudes_535 = true
    exact PellLightProduction.checked_535)

def pellFiniteCertificate_543 : PellFiniteCertificate 543 (10^275) :=
  pellFiniteCertificateOfLight 543 (10^275) 23 449 (pellEmptyMatchingCertificate 543) (by
    change pellLightFiniteCheck 543 23 (10^275) 449 PellLightProduction.magnitudes_543 = true
    exact PellLightProduction.checked_543)

def pellFiniteCertificate_551 : PellFiniteCertificate 551 (10^275) :=
  pellFiniteCertificateOfLight 551 (10^275) 23 390 (pellEmptyMatchingCertificate 551) (by
    change pellLightFiniteCheck 551 23 (10^275) 390 PellLightProduction.magnitudes_551 = true
    exact PellLightProduction.checked_551)

def pellFiniteCertificate_559 : PellFiniteCertificate 559 (10^275) :=
  pellFiniteCertificateOfLight 559 (10^275) 23 610 (pellEmptyMatchingCertificate 559) (by
    change pellLightFiniteCheck 559 23 (10^275) 610 PellLightProduction.magnitudes_559 = true
    exact PellLightProduction.checked_559)

def pellFiniteCertificate_583 : PellFiniteCertificate 583 (10^275) :=
  pellFiniteCertificateOfLight 583 (10^275) 24 380 (pellEmptyMatchingCertificate 583) (by
    change pellLightFiniteCheck 583 24 (10^275) 380 PellLightProduction.magnitudes_583 = true
    exact PellLightProduction.checked_583)

def pellFiniteCertificate_591 : PellFiniteCertificate 591 (10^275) :=
  pellFiniteCertificateOfLight 591 (10^275) 24 498 (pellEmptyMatchingCertificate 591) (by
    change pellLightFiniteCheck 591 24 (10^275) 498 PellLightProduction.magnitudes_591 = true
    exact PellLightProduction.checked_591)

def pellFiniteCertificate_599 : PellFiniteCertificate 599 (10^275) :=
  pellFiniteCertificateOfLight 599 (10^275) 24 560 pellGraphCertificate_599 (by
    change pellLightFiniteCheck 599 24 (10^275) 560 PellLightProduction.magnitudes_599 = true
    exact PellLightProduction.checked_599)

















































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































end D1Bound5
end