A certificate has one of four shapes: the interval is empty; every polynomial in the sentence is constant; the polynomial that governs the sign changes has no real root in the domain; or, in the general case, a list of the pieces into which its real roots cut the domain, with the sign of every polynomial on each piece.
The four disjoint replay branches.
Constructors
Hex.RCF.Certificate.emptyIoc : Hex.RCF.Certificate
Equal or reversed bounded endpoints.
Hex.RCF.Certificate.constants : Hex.RCF.Certificate
A formula containing no nonconstant atom polynomial.
Hex.RCF.Certificate.noRoots (data : Hex.RCF.DecompCert) : Hex.RCF.Certificate
A checked carrier with no real roots.
Hex.RCF.Certificate.cells (data : Hex.RCF.CellsCert) : Hex.RCF.Certificate
A checked carrier with at least one real root.
Unlike the other libraries in this manual, HexRCF imports Mathlib: the
tactic works on ℝ, and its soundness theorem is a statement about real
numbers. The search, the certificate checker and Hex.RCF.decide do not
need Mathlib. They are collected in the module HexRCF.DecisionCheck, which
a build-time check keeps free of Mathlib imports, so the executable part can
be run and tested on its own.
Certificate construction runs as compiled elaboration code. That search is
not trusted. The tactic embeds its sentence and a literal
Hex.RCF.Certificate, reduces the public Boolean checker
Hex.RCF.Certificate.check to true in the kernel, and applies the
soundness theorem Hex.RCF.check_sound. Lean's kernel also checks the
proof that the sentence as data is equivalent to the source goal.
The public soundness boundary can be used independently of the tactic:
open Hex.RCF
example (s : Sentence) (cert : Certificate)
(h : Certificate.check s cert = true) : s.toProp :=
check_sound s cert h
example (s : Sentence)
(h : Hex.RCF.decide s = some true) : s.toProp :=
decide_sound s h
Hex.RCF.Certificate.replay? distinguishes malformed evidence (none), a checked
false verdict (some false), and a checked true verdict (some true).
Hex.RCF.Certificate.check accepts only the last case. The convenience function
Hex.RCF.decide returns some true only after this checker accepts the
certificate. Advanced clients can use Hex.RCF.build? to retain the
certificate and its diagnostic or proof-producing verdict. A successfully
checked false sentence produces some false. Neither Hex.RCF.check_sound nor the
tactic turns some false into a proof of a negation.
A none from Hex.RCF.decide means the compiled path did not produce a
checker-accepted certificate. It does not mean that the sentence is false.
The kernel replays polynomial identities, signs, root counts, endpoint
comparisons, and the Boolean structure of the sentence, all on the concrete
numbers in the certificate. It does not repeat root isolation, polynomial gcd
computation, or interval refinement. The emitted
proof uses ordinary kernel reduction and does not use native_decide:
theorem rcf_square_nonnegative : ∀ x : ℝ, x ^ 2 ≥ 0 := ⊢ ∀ (x : ℝ), x ^ 2 ≥ 0
All goals completed! 🐙
#print axioms rcf_square_nonnegative