Pell Light All Finite Certificates 003

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_007
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_008
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_009
import Definitions.Def_D1Bound5_PellLightAllMatchingCertificates_Definitions_010
import Definitions.Def_D1Bound5_PellLightCF_Definitions
import Definitions.Def_D1Bound5_PellLightFiniteAdapter_Definitions
import Definitions.Def_D1Bound5_PellLightPrefixData10_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData10_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData11_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData11_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData12_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData12_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData8_Definitions_002
import Definitions.Def_D1Bound5_PellLightPrefixData9_Definitions_001
import Definitions.Def_D1Bound5_PellLightPrefixData9_Definitions_002
import Definitions.Def_D1Bound5_PellMatchingCheck_Definitions

section
namespace D1Bound5
set_option maxRecDepth 32768
set_option maxHeartbeats 12000000

































































































































































































































































def pellFiniteCertificate_1247 : PellFiniteCertificate 1247 (10^275) :=
  pellFiniteCertificateOfLight 1247 (10^275) 35 350 (pellEmptyMatchingCertificate 1247) (by
    change pellLightFiniteCheck 1247 35 (10^275) 350 PellLightProduction.magnitudes_1247 = true
    exact PellLightProduction.checked_1247)

def pellFiniteCertificate_1255 : PellFiniteCertificate 1255 (10^275) :=
  pellFiniteCertificateOfLight 1255 (10^275) 35 478 (pellEmptyMatchingCertificate 1255) (by
    change pellLightFiniteCheck 1255 35 (10^275) 478 PellLightProduction.magnitudes_1255 = true
    exact PellLightProduction.checked_1255)

def pellFiniteCertificate_1263 : PellFiniteCertificate 1263 (10^275) :=
  pellFiniteCertificateOfLight 1263 (10^275) 35 503 (pellEmptyMatchingCertificate 1263) (by
    change pellLightFiniteCheck 1263 35 (10^275) 503 PellLightProduction.magnitudes_1263 = true
    exact PellLightProduction.checked_1263)

def pellFiniteCertificate_1271 : PellFiniteCertificate 1271 (10^275) :=
  pellFiniteCertificateOfLight 1271 (10^275) 35 570 (pellEmptyMatchingCertificate 1271) (by
    change pellLightFiniteCheck 1271 35 (10^275) 570 PellLightProduction.magnitudes_1271 = true
    exact PellLightProduction.checked_1271)

def pellFiniteCertificate_1279 : PellFiniteCertificate 1279 (10^275) :=
  pellFiniteCertificateOfLight 1279 (10^275) 35 594 pellGraphCertificate_1279 (by
    change pellLightFiniteCheck 1279 35 (10^275) 594 PellLightProduction.magnitudes_1279 = true
    exact PellLightProduction.checked_1279)

def pellFiniteCertificate_1295 : PellFiniteCertificate 1295 (10^275) :=
  pellFiniteCertificateOfLight 1295 (10^275) 35 296 (pellEmptyMatchingCertificate 1295) (by
    change pellLightFiniteCheck 1295 35 (10^275) 296 PellLightProduction.magnitudes_1295 = true
    exact PellLightProduction.checked_1295)

def pellFiniteCertificate_1303 : PellFiniteCertificate 1303 (10^275) :=
  pellFiniteCertificateOfLight 1303 (10^275) 36 553 pellGraphCertificate_1303 (by
    change pellLightFiniteCheck 1303 36 (10^275) 553 PellLightProduction.magnitudes_1303 = true
    exact PellLightProduction.checked_1303)

def pellFiniteCertificate_1311 : PellFiniteCertificate 1311 (10^275) :=
  pellFiniteCertificateOfLight 1311 (10^275) 36 490 (pellEmptyMatchingCertificate 1311) (by
    change pellLightFiniteCheck 1311 36 (10^275) 490 PellLightProduction.magnitudes_1311 = true
    exact PellLightProduction.checked_1311)

def pellFiniteCertificate_1319 : PellFiniteCertificate 1319 (10^275) :=
  pellFiniteCertificateOfLight 1319 (10^275) 36 466 pellGraphCertificate_1319 (by
    change pellLightFiniteCheck 1319 36 (10^275) 466 PellLightProduction.magnitudes_1319 = true
    exact PellLightProduction.checked_1319)

def pellFiniteCertificate_1327 : PellFiniteCertificate 1327 (10^275) :=
  pellFiniteCertificateOfLight 1327 (10^275) 36 428 pellGraphCertificate_1327 (by
    change pellLightFiniteCheck 1327 36 (10^275) 428 PellLightProduction.magnitudes_1327 = true
    exact PellLightProduction.checked_1327)

def pellFiniteCertificate_1335 : PellFiniteCertificate 1335 (10^275) :=
  pellFiniteCertificateOfLight 1335 (10^275) 36 443 (pellEmptyMatchingCertificate 1335) (by
    change pellLightFiniteCheck 1335 36 (10^275) 443 PellLightProduction.magnitudes_1335 = true
    exact PellLightProduction.checked_1335)

def pellFiniteCertificate_1343 : PellFiniteCertificate 1343 (10^275) :=
  pellFiniteCertificateOfLight 1343 (10^275) 36 558 pellGraphCertificate_1343 (by
    change pellLightFiniteCheck 1343 36 (10^275) 558 PellLightProduction.magnitudes_1343 = true
    exact PellLightProduction.checked_1343)

def pellFiniteCertificate_1351 : PellFiniteCertificate 1351 (10^275) :=
  pellFiniteCertificateOfLight 1351 (10^275) 36 402 (pellEmptyMatchingCertificate 1351) (by
    change pellLightFiniteCheck 1351 36 (10^275) 402 PellLightProduction.magnitudes_1351 = true
    exact PellLightProduction.checked_1351)

def pellFiniteCertificate_1367 : PellFiniteCertificate 1367 (10^275) :=
  pellFiniteCertificateOfLight 1367 (10^275) 36 320 pellGraphCertificate_1367 (by
    change pellLightFiniteCheck 1367 36 (10^275) 320 PellLightProduction.magnitudes_1367 = true
    exact PellLightProduction.checked_1367)

def pellFiniteCertificate_1383 : PellFiniteCertificate 1383 (10^275) :=
  pellFiniteCertificateOfLight 1383 (10^275) 37 429 (pellEmptyMatchingCertificate 1383) (by
    change pellLightFiniteCheck 1383 37 (10^275) 429 PellLightProduction.magnitudes_1383 = true
    exact PellLightProduction.checked_1383)

def pellFiniteCertificate_1391 : PellFiniteCertificate 1391 (10^275) :=
  pellFiniteCertificateOfLight 1391 (10^275) 37 606 (pellEmptyMatchingCertificate 1391) (by
    change pellLightFiniteCheck 1391 37 (10^275) 606 PellLightProduction.magnitudes_1391 = true
    exact PellLightProduction.checked_1391)

def pellFiniteCertificate_1399 : PellFiniteCertificate 1399 (10^275) :=
  pellFiniteCertificateOfLight 1399 (10^275) 37 476 pellGraphCertificate_1399 (by
    change pellLightFiniteCheck 1399 37 (10^275) 476 PellLightProduction.magnitudes_1399 = true
    exact PellLightProduction.checked_1399)

def pellFiniteCertificate_1407 : PellFiniteCertificate 1407 (10^275) :=
  pellFiniteCertificateOfLight 1407 (10^275) 37 426 (pellEmptyMatchingCertificate 1407) (by
    change pellLightFiniteCheck 1407 37 (10^275) 426 PellLightProduction.magnitudes_1407 = true
    exact PellLightProduction.checked_1407)

def pellFiniteCertificate_1415 : PellFiniteCertificate 1415 (10^275) :=
  pellFiniteCertificateOfLight 1415 (10^275) 37 720 (pellEmptyMatchingCertificate 1415) (by
    change pellLightFiniteCheck 1415 37 (10^275) 720 PellLightProduction.magnitudes_1415 = true
    exact PellLightProduction.checked_1415)

def pellFiniteCertificate_1423 : PellFiniteCertificate 1423 (10^275) :=
  pellFiniteCertificateOfLight 1423 (10^275) 37 503 pellGraphCertificate_1423 (by
    change pellLightFiniteCheck 1423 37 (10^275) 503 PellLightProduction.magnitudes_1423 = true
    exact PellLightProduction.checked_1423)

def pellFiniteCertificate_1439 : PellFiniteCertificate 1439 (10^275) :=
  pellFiniteCertificateOfLight 1439 (10^275) 37 507 pellGraphCertificate_1439 (by
    change pellLightFiniteCheck 1439 37 (10^275) 507 PellLightProduction.magnitudes_1439 = true
    exact PellLightProduction.checked_1439)

def pellFiniteCertificate_1447 : PellFiniteCertificate 1447 (10^275) :=
  pellFiniteCertificateOfLight 1447 (10^275) 38 506 pellGraphCertificate_1447 (by
    change pellLightFiniteCheck 1447 38 (10^275) 506 PellLightProduction.magnitudes_1447 = true
    exact PellLightProduction.checked_1447)

def pellFiniteCertificate_1455 : PellFiniteCertificate 1455 (10^275) :=
  pellFiniteCertificateOfLight 1455 (10^275) 38 353 (pellEmptyMatchingCertificate 1455) (by
    change pellLightFiniteCheck 1455 38 (10^275) 353 PellLightProduction.magnitudes_1455 = true
    exact PellLightProduction.checked_1455)

def pellFiniteCertificate_1463 : PellFiniteCertificate 1463 (10^275) :=
  pellFiniteCertificateOfLight 1463 (10^275) 38 220 (pellEmptyMatchingCertificate 1463) (by
    change pellLightFiniteCheck 1463 38 (10^275) 220 PellLightProduction.magnitudes_1463 = true
    exact PellLightProduction.checked_1463)

def pellFiniteCertificate_1471 : PellFiniteCertificate 1471 (10^275) :=
  pellFiniteCertificateOfLight 1471 (10^275) 38 553 pellGraphCertificate_1471 (by
    change pellLightFiniteCheck 1471 38 (10^275) 553 PellLightProduction.magnitudes_1471 = true
    exact PellLightProduction.checked_1471)

def pellFiniteCertificate_1479 : PellFiniteCertificate 1479 (10^275) :=
  pellFiniteCertificateOfLight 1479 (10^275) 38 632 (pellEmptyMatchingCertificate 1479) (by
    change pellLightFiniteCheck 1479 38 (10^275) 632 PellLightProduction.magnitudes_1479 = true
    exact PellLightProduction.checked_1479)

def pellFiniteCertificate_1487 : PellFiniteCertificate 1487 (10^275) :=
  pellFiniteCertificateOfLight 1487 (10^275) 38 608 pellGraphCertificate_1487 (by
    change pellLightFiniteCheck 1487 38 (10^275) 608 PellLightProduction.magnitudes_1487 = true
    exact PellLightProduction.checked_1487)

def pellFiniteCertificate_1495 : PellFiniteCertificate 1495 (10^275) :=
  pellFiniteCertificateOfLight 1495 (10^275) 38 464 (pellEmptyMatchingCertificate 1495) (by
    change pellLightFiniteCheck 1495 38 (10^275) 464 PellLightProduction.magnitudes_1495 = true
    exact PellLightProduction.checked_1495)

def pellFiniteCertificate_1511 : PellFiniteCertificate 1511 (10^275) :=
  pellFiniteCertificateOfLight 1511 (10^275) 38 584 pellGraphCertificate_1511 (by
    change pellLightFiniteCheck 1511 38 (10^275) 584 PellLightProduction.magnitudes_1511 = true
    exact PellLightProduction.checked_1511)

def pellFiniteCertificate_1527 : PellFiniteCertificate 1527 (10^275) :=
  pellFiniteCertificateOfLight 1527 (10^275) 39 182 (pellEmptyMatchingCertificate 1527) (by
    change pellLightFiniteCheck 1527 39 (10^275) 182 PellLightProduction.magnitudes_1527 = true
    exact PellLightProduction.checked_1527)

def pellFiniteCertificate_1535 : PellFiniteCertificate 1535 (10^275) :=
  pellFiniteCertificateOfLight 1535 (10^275) 39 511 (pellEmptyMatchingCertificate 1535) (by
    change pellLightFiniteCheck 1535 39 (10^275) 511 PellLightProduction.magnitudes_1535 = true
    exact PellLightProduction.checked_1535)

def pellFiniteCertificate_1543 : PellFiniteCertificate 1543 (10^275) :=
  pellFiniteCertificateOfLight 1543 (10^275) 39 568 pellGraphCertificate_1543 (by
    change pellLightFiniteCheck 1543 39 (10^275) 568 PellLightProduction.magnitudes_1543 = true
    exact PellLightProduction.checked_1543)

def pellFiniteCertificate_1551 : PellFiniteCertificate 1551 (10^275) :=
  pellFiniteCertificateOfLight 1551 (10^275) 39 754 (pellEmptyMatchingCertificate 1551) (by
    change pellLightFiniteCheck 1551 39 (10^275) 754 PellLightProduction.magnitudes_1551 = true
    exact PellLightProduction.checked_1551)

def pellFiniteCertificate_1559 : PellFiniteCertificate 1559 (10^275) :=
  pellFiniteCertificateOfLight 1559 (10^275) 39 491 pellGraphCertificate_1559 (by
    change pellLightFiniteCheck 1559 39 (10^275) 491 PellLightProduction.magnitudes_1559 = true
    exact PellLightProduction.checked_1559)

def pellFiniteCertificate_1567 : PellFiniteCertificate 1567 (10^275) :=
  pellFiniteCertificateOfLight 1567 (10^275) 39 490 pellGraphCertificate_1567 (by
    change pellLightFiniteCheck 1567 39 (10^275) 490 PellLightProduction.magnitudes_1567 = true
    exact PellLightProduction.checked_1567)

def pellFiniteCertificate_1583 : PellFiniteCertificate 1583 (10^275) :=
  pellFiniteCertificateOfLight 1583 (10^275) 39 615 pellGraphCertificate_1583 (by
    change pellLightFiniteCheck 1583 39 (10^275) 615 PellLightProduction.magnitudes_1583 = true
    exact PellLightProduction.checked_1583)

def pellFiniteCertificate_1591 : PellFiniteCertificate 1591 (10^275) :=
  pellFiniteCertificateOfLight 1591 (10^275) 39 539 (pellEmptyMatchingCertificate 1591) (by
    change pellLightFiniteCheck 1591 39 (10^275) 539 PellLightProduction.magnitudes_1591 = true
    exact PellLightProduction.checked_1591)

def pellFiniteCertificate_1599 : PellFiniteCertificate 1599 (10^275) :=
  pellFiniteCertificateOfLight 1599 (10^275) 39 288 (pellEmptyMatchingCertificate 1599) (by
    change pellLightFiniteCheck 1599 39 (10^275) 288 PellLightProduction.magnitudes_1599 = true
    exact PellLightProduction.checked_1599)

def pellFiniteCertificate_1607 : PellFiniteCertificate 1607 (10^275) :=
  pellFiniteCertificateOfLight 1607 (10^275) 40 532 pellGraphCertificate_1607 (by
    change pellLightFiniteCheck 1607 40 (10^275) 532 PellLightProduction.magnitudes_1607 = true
    exact PellLightProduction.checked_1607)

def pellFiniteCertificate_1615 : PellFiniteCertificate 1615 (10^275) :=
  pellFiniteCertificateOfLight 1615 (10^275) 40 401 (pellEmptyMatchingCertificate 1615) (by
    change pellLightFiniteCheck 1615 40 (10^275) 401 PellLightProduction.magnitudes_1615 = true
    exact PellLightProduction.checked_1615)

def pellFiniteCertificate_1623 : PellFiniteCertificate 1623 (10^275) :=
  pellFiniteCertificateOfLight 1623 (10^275) 40 327 (pellEmptyMatchingCertificate 1623) (by
    change pellLightFiniteCheck 1623 40 (10^275) 327 PellLightProduction.magnitudes_1623 = true
    exact PellLightProduction.checked_1623)

def pellFiniteCertificate_1631 : PellFiniteCertificate 1631 (10^275) :=
  pellFiniteCertificateOfLight 1631 (10^275) 40 560 (pellEmptyMatchingCertificate 1631) (by
    change pellLightFiniteCheck 1631 40 (10^275) 560 PellLightProduction.magnitudes_1631 = true
    exact PellLightProduction.checked_1631)

def pellFiniteCertificate_1639 : PellFiniteCertificate 1639 (10^275) :=
  pellFiniteCertificateOfLight 1639 (10^275) 40 426 (pellEmptyMatchingCertificate 1639) (by
    change pellLightFiniteCheck 1639 40 (10^275) 426 PellLightProduction.magnitudes_1639 = true
    exact PellLightProduction.checked_1639)

def pellFiniteCertificate_1655 : PellFiniteCertificate 1655 (10^275) :=
  pellFiniteCertificateOfLight 1655 (10^275) 40 378 (pellEmptyMatchingCertificate 1655) (by
    change pellLightFiniteCheck 1655 40 (10^275) 378 PellLightProduction.magnitudes_1655 = true
    exact PellLightProduction.checked_1655)

def pellFiniteCertificate_1663 : PellFiniteCertificate 1663 (10^275) :=
  pellFiniteCertificateOfLight 1663 (10^275) 40 558 pellGraphCertificate_1663 (by
    change pellLightFiniteCheck 1663 40 (10^275) 558 PellLightProduction.magnitudes_1663 = true
    exact PellLightProduction.checked_1663)

def pellFiniteCertificate_1671 : PellFiniteCertificate 1671 (10^275) :=
  pellFiniteCertificateOfLight 1671 (10^275) 40 377 (pellEmptyMatchingCertificate 1671) (by
    change pellLightFiniteCheck 1671 40 (10^275) 377 PellLightProduction.magnitudes_1671 = true
    exact PellLightProduction.checked_1671)

def pellFiniteCertificate_1679 : PellFiniteCertificate 1679 (10^275) :=
  pellFiniteCertificateOfLight 1679 (10^275) 40 312 pellGraphCertificate_1679 (by
    change pellLightFiniteCheck 1679 40 (10^275) 312 PellLightProduction.magnitudes_1679 = true
    exact PellLightProduction.checked_1679)

def pellFiniteCertificate_1687 : PellFiniteCertificate 1687 (10^275) :=
  pellFiniteCertificateOfLight 1687 (10^275) 41 397 pellGraphCertificate_1687 (by
    change pellLightFiniteCheck 1687 41 (10^275) 397 PellLightProduction.magnitudes_1687 = true
    exact PellLightProduction.checked_1687)

def pellFiniteCertificate_1695 : PellFiniteCertificate 1695 (10^275) :=
  pellFiniteCertificateOfLight 1695 (10^275) 41 480 (pellEmptyMatchingCertificate 1695) (by
    change pellLightFiniteCheck 1695 41 (10^275) 480 PellLightProduction.magnitudes_1695 = true
    exact PellLightProduction.checked_1695)

def pellFiniteCertificate_1703 : PellFiniteCertificate 1703 (10^275) :=
  pellFiniteCertificateOfLight 1703 (10^275) 41 499 (pellEmptyMatchingCertificate 1703) (by
    change pellLightFiniteCheck 1703 41 (10^275) 499 PellLightProduction.magnitudes_1703 = true
    exact PellLightProduction.checked_1703)

def pellFiniteCertificate_1711 : PellFiniteCertificate 1711 (10^275) :=
  pellFiniteCertificateOfLight 1711 (10^275) 41 492 (pellEmptyMatchingCertificate 1711) (by
    change pellLightFiniteCheck 1711 41 (10^275) 492 PellLightProduction.magnitudes_1711 = true
    exact PellLightProduction.checked_1711)

def pellFiniteCertificate_1727 : PellFiniteCertificate 1727 (10^275) :=
  pellFiniteCertificateOfLight 1727 (10^275) 41 583 (pellEmptyMatchingCertificate 1727) (by
    change pellLightFiniteCheck 1727 41 (10^275) 583 PellLightProduction.magnitudes_1727 = true
    exact PellLightProduction.checked_1727)

def pellFiniteCertificate_1735 : PellFiniteCertificate 1735 (10^275) :=
  pellFiniteCertificateOfLight 1735 (10^275) 41 578 (pellEmptyMatchingCertificate 1735) (by
    change pellLightFiniteCheck 1735 41 (10^275) 578 PellLightProduction.magnitudes_1735 = true
    exact PellLightProduction.checked_1735)

def pellFiniteCertificate_1743 : PellFiniteCertificate 1743 (10^275) :=
  pellFiniteCertificateOfLight 1743 (10^275) 41 436 (pellEmptyMatchingCertificate 1743) (by
    change pellLightFiniteCheck 1743 41 (10^275) 436 PellLightProduction.magnitudes_1743 = true
    exact PellLightProduction.checked_1743)

def pellFiniteCertificate_1751 : PellFiniteCertificate 1751 (10^275) :=
  pellFiniteCertificateOfLight 1751 (10^275) 41 454 (pellEmptyMatchingCertificate 1751) (by
    change pellLightFiniteCheck 1751 41 (10^275) 454 PellLightProduction.magnitudes_1751 = true
    exact PellLightProduction.checked_1751)

def pellFiniteCertificate_1759 : PellFiniteCertificate 1759 (10^275) :=
  pellFiniteCertificateOfLight 1759 (10^275) 41 571 pellGraphCertificate_1759 (by
    change pellLightFiniteCheck 1759 41 (10^275) 571 PellLightProduction.magnitudes_1759 = true
    exact PellLightProduction.checked_1759)

def pellFiniteCertificate_1767 : PellFiniteCertificate 1767 (10^275) :=
  pellFiniteCertificateOfLight 1767 (10^275) 42 163 (pellEmptyMatchingCertificate 1767) (by
    change pellLightFiniteCheck 1767 42 (10^275) 163 PellLightProduction.magnitudes_1767 = true
    exact PellLightProduction.checked_1767)

def pellFiniteCertificate_1783 : PellFiniteCertificate 1783 (10^275) :=
  pellFiniteCertificateOfLight 1783 (10^275) 42 554 pellGraphCertificate_1783 (by
    change pellLightFiniteCheck 1783 42 (10^275) 554 PellLightProduction.magnitudes_1783 = true
    exact PellLightProduction.checked_1783)

def pellFiniteCertificate_1799 : PellFiniteCertificate 1799 (10^275) :=
  pellFiniteCertificateOfLight 1799 (10^275) 42 486 pellGraphCertificate_1799 (by
    change pellLightFiniteCheck 1799 42 (10^275) 486 PellLightProduction.magnitudes_1799 = true
    exact PellLightProduction.checked_1799)

def pellFiniteCertificate_1807 : PellFiniteCertificate 1807 (10^275) :=
  pellFiniteCertificateOfLight 1807 (10^275) 42 532 (pellEmptyMatchingCertificate 1807) (by
    change pellLightFiniteCheck 1807 42 (10^275) 532 PellLightProduction.magnitudes_1807 = true
    exact PellLightProduction.checked_1807)

def pellFiniteCertificate_1823 : PellFiniteCertificate 1823 (10^275) :=
  pellFiniteCertificateOfLight 1823 (10^275) 42 644 pellGraphCertificate_1823 (by
    change pellLightFiniteCheck 1823 42 (10^275) 644 PellLightProduction.magnitudes_1823 = true
    exact PellLightProduction.checked_1823)

def pellFiniteCertificate_1831 : PellFiniteCertificate 1831 (10^275) :=
  pellFiniteCertificateOfLight 1831 (10^275) 42 583 pellGraphCertificate_1831 (by
    change pellLightFiniteCheck 1831 42 (10^275) 583 PellLightProduction.magnitudes_1831 = true
    exact PellLightProduction.checked_1831)

def pellFiniteCertificate_1839 : PellFiniteCertificate 1839 (10^275) :=
  pellFiniteCertificateOfLight 1839 (10^275) 42 497 (pellEmptyMatchingCertificate 1839) (by
    change pellLightFiniteCheck 1839 42 (10^275) 497 PellLightProduction.magnitudes_1839 = true
    exact PellLightProduction.checked_1839)

def pellFiniteCertificate_1847 : PellFiniteCertificate 1847 (10^275) :=
  pellFiniteCertificateOfLight 1847 (10^275) 42 308 pellGraphCertificate_1847 (by
    change pellLightFiniteCheck 1847 42 (10^275) 308 PellLightProduction.magnitudes_1847 = true
    exact PellLightProduction.checked_1847)

















































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































































end D1Bound5
end