Pair Light Prepared38 — right checked

Proved

D1Bound5.PairLightPrepared38.right_checked

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

diophantine-tuplesnumber-theory

Auxiliary result PairLightPrepared38.right_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_SmallPairGraphData38_Definitions_003
import Definitions.Def_D1Bound5_SmallPairGraphData38_Definitions_004
import Definitions.Def_D1Bound5_SmallPairSieve_1_2_Definitions

Formal statement

section
/- Preserved body from D1Bound5.SmallPairGraphInputs38; original SHA256 e84905f2c584eaec762f49ff95cacb67eda33b4f26e2c70c9b7b8b2cce33bac3. -/

namespace D1Bound5
set_option maxRecDepth 100000

open QuadInt








namespace PairGraphPrepared38



end PairGraphPrepared38
end D1Bound5

/- Preserved body from D1Bound5.SmallPairGraphArithmetic38; original SHA256 dd8dbfa6abf4d50ab024f61aee47d820a823b926c36e406836f87c60656daee7. -/

namespace D1Bound5
set_option maxRecDepth 100000
set_option maxHeartbeats 0







end D1Bound5

/- Preserved body from D1Bound5.SmallPairGraphWitnessData38; original SHA256 c6164df96db4aa1be0a86091c70be1a406e41f83d72c88d46eabb3e7189c3052. -/

namespace D1Bound5.PairGraphPrepared38
set_option maxRecDepth 100000









end D1Bound5.PairGraphPrepared38

/- Preserved body from D1Bound5.SmallPairGraphClosure38; original SHA256 b10bc5b53ff5864b17af0b52e70793fe0d0cc33ca5726ae8e59895847f319d29. -/

namespace D1Bound5
set_option maxRecDepth 100000
set_option maxHeartbeats 0

open PairGraphPrepared38





end D1Bound5

/- Preserved body from D1Bound5.SmallPairRawSelectedData38; original SHA256 bc91510fcbc172095a6e7f20939407122422a55cd73446afa31e0b04776daec7. -/

namespace D1Bound5.PairSelectedPrepared38
set_option maxRecDepth 100000









end D1Bound5.PairSelectedPrepared38

/- Preserved body from D1Bound5.SmallPairLightAssembly38; original SHA256 0a6d4a5a2f8cf5b522f0c22f64572b8fe8962d975aa36145b357f51474e4371c. -/

namespace D1Bound5.PairLightPrepared38
set_option maxRecDepth 100000
set_option maxHeartbeats 0

















theorem _root_.D1Bound5.PairLightPrepared38.right_checked :
    pairIndependentBool smallPairSieve_1_2 (pairSplitByMask smallPairLarge_38 PairGraphPrepared38.colors).2 = true := by sorry

end D1Bound5.PairLightPrepared38

/- Preserved body from D1Bound5.SmallPairGraphTriangle38; original SHA256 cb5933e1c0e765de3430434a98639be128637fe79d2d295f12b7f83e963f8872. -/

namespace D1Bound5
set_option maxRecDepth 100000



end D1Bound5

/- Preserved body from D1Bound5.SmallPairGraphData38; original SHA256 83f2c3bd68777968da247a58362b3e2051ce156b248c76a29c29eb55c1278ea0. -/
end

Source

D1Bound5/SmallPairGraphData38.lean, lines 3520-3525, SHA-256 a997843325b5adcd34463654eb0279c8f8b4f0865ed325a847802b71b2ad9df2. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph