Pair Light Prepared2 — left checked

Proved

D1Bound5.PairLightPrepared2.left_checked

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

diophantine-tuplesnumber-theory

Auxiliary result PairLightPrepared2.left_checked in the proof of the bound five for Diophantine D(1) sets in imaginary quadratic integer rings. The formal statement specifies its hypotheses and conclusion; a mathematical prose description remains to be supplied.

Preamble

import Init
import Mathlib.Algebra.Order.Ring.Abs
import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Complex.Norm
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Int.GCD
import Mathlib.Data.Int.Interval
import Mathlib.Data.Int.Sqrt
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Range
import Mathlib.Data.ZMod.Basic
import Mathlib.LinearAlgebra.Dimension.Free
import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
import Mathlib.NumberTheory.NumberField.Norm
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_Coordinates_Definitions
import Definitions.Def_D1Bound5_PairBipartiteCheck_Definitions
import Definitions.Def_D1Bound5_SmallPairGraphData2_Definitions_002
import Definitions.Def_D1Bound5_SmallPairSieve_0_1_Definitions

Formal statement

section
/- Preserved body from D1Bound5.SmallPairGraphInputs2; original SHA256 05c6eac538f8497cd3a821770526ca8706d00a25abdc81b4c26cfd4d1fb29b57. -/

namespace D1Bound5
set_option maxRecDepth 100000

open QuadInt








namespace PairGraphPrepared2



end PairGraphPrepared2
end D1Bound5

/- Preserved body from D1Bound5.SmallPairGraphArithmetic2; original SHA256 26154516f673902cc1e3bce80054f0c96e08d80a543d1e1f2882f177302acaf7. -/

namespace D1Bound5
set_option maxRecDepth 100000
set_option maxHeartbeats 0







end D1Bound5

/- Preserved body from D1Bound5.SmallPairGraphWitnessData2; original SHA256 f319a0bdaefa48f1a9f3ae5ceb65656c94c041b0fa290e14cab6856d8341c7fb. -/

namespace D1Bound5.PairGraphPrepared2
set_option maxRecDepth 100000









end D1Bound5.PairGraphPrepared2

/- Preserved body from D1Bound5.SmallPairGraphClosure2; original SHA256 6c3d39e00759e54ecfe739fe7c0b0c438ed702899f4932797158545d8d3f914b. -/

namespace D1Bound5
set_option maxRecDepth 100000
set_option maxHeartbeats 0

open PairGraphPrepared2





end D1Bound5

/- Preserved body from D1Bound5.SmallPairRawSelectedData2; original SHA256 bd14d335ba3742940ee6255966b2aa93923682ac39e18375e9a9ee7870d1dc4f. -/

namespace D1Bound5.PairSelectedPrepared2
set_option maxRecDepth 100000









end D1Bound5.PairSelectedPrepared2

/- Preserved body from D1Bound5.SmallPairLightAssembly2; original SHA256 28e25096d2fda97cfe2f853e3f3dc8734674d85d678e091170cdd16eaf988ed7. -/

namespace D1Bound5.PairLightPrepared2
set_option maxRecDepth 100000
set_option maxHeartbeats 0









theorem _root_.D1Bound5.PairLightPrepared2.left_checked :
    pairIndependentBool smallPairSieve_0_1 (pairSplitByMask smallPairLarge_2 PairGraphPrepared2.colors).1 = true := by sorry









end D1Bound5.PairLightPrepared2

/- Preserved body from D1Bound5.SmallPairGraphTriangle2; original SHA256 304600336a461f07462df8aa2968c65908970f7e5cd79d6981f86853f6ac6e7d. -/

namespace D1Bound5
set_option maxRecDepth 100000



end D1Bound5

/- Preserved body from D1Bound5.SmallPairGraphData2; original SHA256 89e5d1cc4246d5ec20132684b3f2d13a6ac263401e770195eef0c09fa478e927. -/
end

Source

D1Bound5/SmallPairGraphData2.lean, lines 2620-2625, SHA-256 be08008a0ad80b33a5853a5240bd17aa588c523ee4ff90f53bde4787f4fb0943. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph