Prove2Me

Pair Light Right Pilot34 — right certificate checked

Proved
D1Bound5.PairLightRightPilot34.right_certificate_checked

by tp · Oct 23, 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_SmallPairLightRightData34_Definitions_001
import Definitions.Def_D1Bound5_SmallPairLightRightData34_Definitions_002
Formal statement
section
namespace D1Bound5.PairLightRightPilot34
set_option maxRecDepth 100000
set_option maxHeartbeats 0


theorem _root_.D1Bound5.PairLightRightPilot34.right_certificate_checked :
    pairLightSelectedFloorIndependentCertificateBool 1 2 sieve
      rightVertices rightCached rightRows = true := by sorry

end D1Bound5.PairLightRightPilot34
end
Source
D1Bound5/SmallPairLightRight34.lean, lines 7-12, SHA-256 13228b59b3cf1b1c112fe577f3dcda6d8c3607137915c305f5c3472bca5a8bae. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph