Exact light coverage of indices 0–49

Proved

D1Bound5.Prove2MeTransfer.pellCoverageLightBlock00_20261024

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

diophantine-tuplesnumber-theory

For indices 0 through 49, the original integer parameter list or an explicit nonunit square divisor verifies the field-coverage test. This is the light-data form of the first coverage block.

Preamble

import Mathlib.Tactic
import Definitions.Def_D1Bound5_PellFiniteFieldCoverageLight_Definitions

Formal statement


section
namespace D1Bound5
set_option maxRecDepth 32768
set_option maxHeartbeats 12000000

theorem _root_.D1Bound5.Prove2MeTransfer.pellCoverageLightBlock00_20261024 : ∀ k : Fin 50, PellFieldCoverageLightAt (0+k.val) := by sorry

end D1Bound5
end

Source

D1Bound5/PellFiniteFields.lean, lines 91-110, SHA-256 352c30df17c6d6e5a3b765a23814fee880412e130767d7c10f6bf24c2c1ef96d. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph