def Hex.RCF.buildSturmReplay? (f : ZPoly) : Option SturmReplay

Build and verify a multiplication-only generalized Sturm replay.

The compiled builder may use pseudo-remainders and primitive parts, but a candidate crosses the boundary only after the multiplication-only checker accepts it.

Equations

• Hex.RCF.buildSturmReplay? f = match Hex.RCF.buildSturmReplayRaw?✝ f with | none => none | some replay => if Hex.RCF.SturmReplay.check f replay = true then some replay else none

theorem Hex.RCF.check_buildSturmReplay {f : ZPoly} {replay : SturmReplay} (h : buildSturmReplay? f = some replay) : SturmReplay.check f replay = true

Every certificate returned by the builder has passed the kernel-facing Boolean checker.