Exact Pell data slice 8bc6e5fa5d389d1fe74b

Definition

D1Bound5_Prove2MeTransfer_pellSlice_8bc6e5fa5d389d1fe74b

by tp · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

Exact consecutive entries 128–133 of pellWitnesses_7. The original list is the ordered concatenation of these slices.

Definition code

import Init

namespace D1Bound5.Prove2MeTransfer
set_option maxRecDepth 100000
set_option maxHeartbeats 0

def pellSlice_8bc6e5fa5d389d1fe74b : List (List (Nat × Nat)) :=
[
  [(1,0),(1,0),(1,4),(1,0),(1,0),(1,5),(1,0),(1,0),(1,3),(1,0),(1,0),(1,4),(1,0),(1,0),(1,5),(1,0),(1,0),(1,5),(1,0),(1,0),(1,4),(1,0),(1,0),(1,5),(1,0),(1,0),(1,8),(1,0),(1,0),(1,3),(1,0),(1,0),(1,5),(1,0),(1,0),(1,12),(1,0),(1,0),(1,4),(1,0),(1,0),(1,10),(1,0),(1,0),(1,9),(1,0),(1,0),(1,4),(1,0),(1,0),(1,3),(1,0),(1,0),(1,8),(1,0),(1,0),(1,4),(1,0),(1,0),(1,5),(1,0),(1,0),(1,5),(1,0),(1,0),(1,4),(1,0),(1,0),(1,8),(1,0),(1,0),(1,3),(1,0),(1,0),(1,4),(1,0),(1,0),(1,17),(1,0),(1,0),(1,9),(1,0),(1,0),(1,4),(1,0),(1,0),(1,10),(1,0),(1,0),(1,5),(1,0),(1,0),(1,3),(1,0),(1,0),(1,8),(1,0),(1,0),(1,5),(1,0),(1,0)],
  [(1,3),(1,0),(1,2),(1,2),(1,0),(1,6),(1,5),(1,0),(1,2),(1,2),(1,0),(1,3),(1,5),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,5),(1,3),(1,0),(1,2),(1,2),(1,0),(1,4),(1,10),(1,0),(1,2),(1,2),(1,0),(1,3),(1,4),(1,0),(1,2),(1,2),(1,0),(1,11),(1,3),(1,0),(1,2),(1,2),(1,0),(1,4),(1,5),(1,0),(1,2),(1,2),(1,0),(1,3),(1,4),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,4),(1,3),(1,0),(1,2),(1,2),(1,0),(1,5),(1,4),(1,0),(1,2),(1,2),(1,0),(1,3),(1,6),(1,0),(1,2),(1,2),(1,0),(1,4),(1,3),(1,0),(1,2),(1,2),(1,0),(1,9),(1,4),(1,0),(1,2),(1,2),(1,0),(1,3),(1,5),(1,0),(1,2),(1,2)],
  [(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,4),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,7),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,6),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,4),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2)],
  [(1,0),(1,0),(1,3),(1,0),(1,0),(1,3),(1,0),(1,0),(1,3),(1,0),(1,0),(1,4),(1,0),(1,0),(1,4),(1,0),(1,0),(1,5),(1,0),(1,0),(1,4),(1,0),(1,0),(1,3),(1,0),(1,0),(1,3),(1,0),(1,0),(1,3),(1,0),(1,0),(1,4),(1,0),(1,0),(1,6),(1,0),(1,0),(1,4),(1,0),(1,0),(1,4),(1,0),(1,0),(1,3),(1,0),(1,0),(1,3),(1,0),(1,0),(1,3),(1,0),(1,0),(1,5),(1,0),(1,0),(1,4),(1,0),(1,0),(1,4),(1,0),(1,0),(1,5),(1,0),(1,0),(1,3),(1,0),(1,0),(1,3),(1,0),(1,0),(1,3),(1,0),(1,0),(1,4),(1,0),(1,0),(1,4),(1,0),(1,0),(1,6),(1,0),(1,0),(1,4),(1,0),(1,0),(1,3),(1,0),(1,0),(1,3),(1,0),(1,0),(1,3),(1,0),(1,0),(1,4),(1,0),(1,0)],
  [(1,4),(1,0),(1,2),(1,2),(1,0),(1,4),(1,5),(1,0),(1,2),(1,2),(1,0),(1,3),(1,5),(1,0),(1,2),(1,2),(1,0),(1,5),(1,3),(1,0),(1,2),(1,2),(1,0),(1,4),(1,8),(1,0),(1,2),(1,2),(1,0),(1,7),(1,7),(1,0),(1,2),(1,2),(1,0),(1,5),(1,4),(1,0),(1,2),(1,2),(1,0),(1,4),(1,6),(1,0),(1,2),(1,2),(1,0),(1,6),(1,5),(1,0),(1,2),(1,2),(1,0),(1,3),(1,4),(1,0),(1,2),(1,2),(1,0),(1,4),(1,3),(1,0),(1,2),(1,2),(1,0),(1,5),(1,7),(1,0),(1,2),(1,2),(1,0),(1,11),(1,4),(1,0),(1,2),(1,2),(1,0),(1,4),(1,5),(1,0),(1,2),(1,2),(1,0),(1,6),(1,7),(1,0),(1,2),(1,2),(1,0),(1,8),(1,4),(1,0),(1,2),(1,2),(1,0),(1,3),(1,5)],
  [(1,0),(1,2),(1,2),(1,0),(1,3),(1,4),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,5),(1,3),(1,0),(1,2),(1,2),(1,0),(1,11),(1,10),(1,0),(1,2),(1,2),(1,0),(1,4),(1,8),(1,0),(1,2),(1,2),(1,0),(1,6),(1,4),(1,0),(1,2),(1,2),(1,0),(1,3),(1,5),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3),(1,0),(1,2),(1,2),(1,0),(1,5),(1,3),(1,0),(1,2),(1,2),(1,0),(1,4),(1,6),(1,0),(1,2),(1,2),(1,0),(1,6),(1,4),(1,0),(1,2),(1,2),(1,0),(1,6),(1,6),(1,0),(1,2),(1,2),(1,0),(1,3),(1,5),(1,0),(1,2),(1,2),(1,0),(1,3),(1,3)]
]

end D1Bound5.Prove2MeTransfer

Source

D1Bound5/PellLightMatchingField7.lean, lines 7-8, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82; D1Bound5/PellLightMatchingField7.lean, lines 10-11, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82; D1Bound5/PellLightMatchingField7.lean, lines 13-14, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82; D1Bound5/PellLightMatchingField7.lean, lines 16-18, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82; D1Bound5/PellLightMatchingField7.lean, lines 20-22, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82; D1Bound5/PellLightMatchingField7.lean, lines 24-26, SHA-256 cb2b47876127a30e241273d61a4c1a7056c0b462398797ee7f4519b7c4f90d82. Project: https://github.com/tomislav-math/d1-bound5-lean. Exact entries 128-133 of pellWitnesses_7; original literal SHA-256 581029e34b801bc55a56d20c3817498f0ce63aef9679c94437bf3d1c27aa63a4.

View graph