Pell certificate existence, records 193–256

import Mathlib.Tactic
import Definitions.Def_D1Bound5_PellFiniteCertificate_Definitions

section
namespace D1Bound5
set_option maxRecDepth 32768
set_option maxHeartbeats 12000000

theorem _root_.D1Bound5.Prove2MeTransfer.pellCertificateMembership03_20261024 (d : ℤ) (hd : d ∈ ([1871,1879,1887,1895,1903,1919,1927,1943,1951,1959,1967,1983,1991,1999,2015,2031,2039,2047,2055,2063,2071,2087,2095,2103,2111,2119,2127,2135,2143,2159,2167,2183,2191,2199,2207,2215,2231,2239,2247,2255,2263,2271,2279,2287,2311,2319,2327,2335,2343,2351,2359,2383,2391,2399,2407,2415,2423,2431,2447,2455,2463,2471,2479,2487] : List ℤ)) : Nonempty (PellFiniteCertificate d (10^275)) := by sorry

end D1Bound5
end