Pair Light Pilot34 — left certificate checked

Proved

D1Bound5.PairLightPilot34.left_certificate_checked

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

diophantine-tuplesnumber-theory

Only the isolated arithmetic computation. Connection to the original class requires the separately checked data equalities and exact bridge.

Preamble

import Init
import Definitions.Def_D1Bound5_PairLightArithmetic_Definitions
import Definitions.Def_D1Bound5_SmallPairLightData34_Definitions_001
import Definitions.Def_D1Bound5_SmallPairLightData34_Definitions_002

Formal statement

section
namespace D1Bound5.PairLightPilot34
set_option maxRecDepth 100000
set_option maxHeartbeats 0


theorem _root_.D1Bound5.PairLightPilot34.left_certificate_checked :
    pairLightSelectedFloorIndependentCertificateBool 1 2 sieve
      leftVertices leftCached leftRows = true := by sorry

end D1Bound5.PairLightPilot34
end

Source

D1Bound5/SmallPairLightLeft34.lean, lines 7-12, SHA-256 734d15677639f0fedfc48da6132ef1e0408a7c506f8c499f9b3f9d1a045be66e. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph