def Hex.RCF.SturmReplay.Valid (f : ZPoly) (cert : SturmReplay) : Prop

Kernel-facing consequences of an accepted generalized Sturm replay. The existential form keeps this a proposition while exposing the literal list decomposition needed by downstream count proofs.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.RCF.SturmReplay.checkStep_sound {a b c : ZPoly} {step : SturmStep} (h : checkStep a b c step = true) : HexRealRootsMathlib.ZReplayStep a b c

A successful identity check supplies the existential recurrence expected by HexRealRootsMathlib.ZReplay.

theorem Hex.RCF.SturmReplay.checkSteps_sound {a b : ZPoly} {rest : List ZPoly} {steps : List SturmStep} (h : checkSteps a b rest steps = true) : HexRealRootsMathlib.ZReplay a b rest

A successful recurrence walk constructs an abstract integer replay.

theorem Hex.RCF.SturmReplay.check_sound {f : ZPoly} {cert : SturmReplay} (h : check f cert = true) : Valid f cert

Soundness of the executable generalized Sturm replay checker.

theorem Hex.RCF.SturmReplay.isChain_of_check {f : ZPoly} {cert : SturmReplay} (h : check f cert = true) : Sturm.IsSturmChain (HexRealRootsMathlib.toPolyℝ f) (List.map HexRealRootsMathlib.toPolyℝ cert.chain.toList)

An accepted replay is a Sturm chain after casting its literal entries to real polynomials.

theorem Hex.RCF.SturmReplay.squarefree_of_check {f : ZPoly} {cert : SturmReplay} (h : check f cert = true) : Squarefree (HexRealRootsMathlib.toPolyℝ f)

An accepted replay proves that the real cast of its head is squarefree.

theorem Hex.RCF.SturmReplay.count_eq_card_roots {f : ZPoly} {cert : SturmReplay} (h : check f cert = true) (I : DyadicInterval) : cert.count I = ↑(HexRealRootsMathlib.Literal.rootsIn (HexRealRootsMathlib.toPolyℝ f) I).card

The literal variation drop of an accepted replay counts exactly the real roots in the supplied half-open interval. This acts directly on the certificate array, avoiding a list-to-array round trip.

theorem Hex.RCF.SturmReplay.total_eq_card_roots {f : ZPoly} {cert : SturmReplay} (h : check f cert = true) : cert.total = ↑(HexRealRootsMathlib.toPolyℝ f).roots.card

The literal infinite-endpoint variation drop of an accepted replay counts exactly all real roots of its head. This acts directly on the certificate array.