Pell certificate existence, records 769–832

import Mathlib.Tactic
import Definitions.Def_D1Bound5_PellFiniteCertificate_Definitions

section
namespace D1Bound5
set_option maxRecDepth 32768
set_option maxHeartbeats 12000000

theorem _root_.D1Bound5.Prove2MeTransfer.pellCertificateMembership12_20261024 (d : ℤ) (hd : d ∈ ([7543,7559,7567,7583,7591,7599,7607,7615,7631,7639,7647,7655,7663,7671,7679,7687,7703,7711,7719,7727,7735,7743,7751,7759,7783,7799,7807,7815,7823,7831,7847,7855,7863,7871,7879,7887,7895,7903,7919,7927,7951,7959,7967,7991,7999,8007,8015,8023,8031,8039,8047,8063,8071,8079,8087,8095,8103,8111,8119,8135,8143,8151,8159,8167] : List ℤ)) : Nonempty (PellFiniteCertificate d (10^275)) := by sorry

end D1Bound5
end