theorem Hex.RCF.Cmp.scale_sub_iff (cmp : Cmp) {lhs rhs scale : ℝ} (hscale : 0 < scale) : cmp.toProp (scale * (lhs - rhs)) 0 ↔ cmp.toProp lhs rhs

Transport any supported comparison across subtraction and multiplication by a positive scalar.

theorem Hex.RCF.Atom.toProp_iff_scale {p : ZPoly} {cmp : Cmp} {x lhs rhs scale : ℝ} (hscale : 0 < scale) (heval : (Polynomial.aeval x) (HexPolyZTheory.toPolynomial p) = scale * (lhs - rhs)) : { p := p, cmp := cmp }.toProp x ↔ cmp.toProp lhs rhs

A kernel-checked scaled evaluation identity validates one reified atom.

theorem Hex.RCF.Atom.toProp_iff_natScale {p : ZPoly} {cmp : Cmp} {x lhs rhs : ℝ} {scale : ℕ} (hscale : 0 < scale) (heval : (Polynomial.aeval x) (HexPolyZTheory.toPolynomial p) = ↑scale * (lhs - rhs)) : { p := p, cmp := cmp }.toProp x ↔ cmp.toProp lhs rhs

Natural denominator clearing is a convenient literal specialization for the meta reifier.

theorem Hex.RCF.Sentence.forallReal_iff {formula : Formula} {predicate : ℝ → Prop} (h : ∀ (x : ℝ), formula.toProp x ↔ predicate x) : (forallReal formula).toProp ↔ ∀ (x : ℝ), predicate x

Transport a reflected universal sentence along its formula equivalence.

theorem Hex.RCF.Sentence.existsReal_iff {formula : Formula} {predicate : ℝ → Prop} (h : ∀ (x : ℝ), formula.toProp x ↔ predicate x) : (existsReal formula).toProp ↔ ∃ (x : ℝ), predicate x

Transport a reflected existential sentence along its formula equivalence.

theorem Hex.RCF.Sentence.forallIoc_iff {a b : Dyadic} {a' b' : ℝ} {formula : Formula} {predicate : ℝ → Prop} (ha : HexRealRootsTheory.Dyadic.toReal a = a') (hb : HexRealRootsTheory.Dyadic.toReal b = b') (h : ∀ (x : ℝ), formula.toProp x ↔ predicate x) : (forallIoc a b formula).toProp ↔ ∀ x ∈ Set.Ioc a' b', predicate x

Transport a reflected bounded universal sentence and its dyadic endpoints.

theorem Hex.RCF.Sentence.existsIoc_iff {a b : Dyadic} {a' b' : ℝ} {formula : Formula} {predicate : ℝ → Prop} (ha : HexRealRootsTheory.Dyadic.toReal a = a') (hb : HexRealRootsTheory.Dyadic.toReal b = b') (h : ∀ (x : ℝ), formula.toProp x ↔ predicate x) : (existsIoc a b formula).toProp ↔ ∃ x ∈ Set.Ioc a' b', predicate x

Transport a reflected bounded existential sentence and its dyadic endpoints.

def Hex.RCF.rcfRing : Lean.ParserDescr

Close evaluation identities for literal ZPoly coefficients and accepted ring syntax. The parser remains untrusted: unsupported or misparsed syntax merely makes this proof fail during elaboration.

Equations

• Hex.RCF.rcfRing = Lean.ParserDescr.node `Hex.RCF.rcfRing 1024 (Lean.ParserDescr.nonReservedSymbol "rcf_ring" false)

structure Hex.RCF.Reify.ClosedCoefficient : Type

A coefficient expression and an ordinary proof that it equals a closed real value. This is syntax authentication, not a sign or domain decision.

• value : Lean.Expr

  A real expression with no free variables or metavariables.

• proof : Lean.Expr

  Equality of the original expression with value.

def Hex.RCF.Reify.closeCoefficient? (source : Lean.Expr) : Lean.MetaM (Option ClosedCoefficient)

Close a real coefficient using only explicit local equalities to closed values. Every free symbol needs its own direct witness. Substitution preserves all arithmetic syntax, including original divisors and zero multiplication.

Equations

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

structure Hex.RCF.Reify.UnsupportedCoefficient : Type

Rational recognition stopped at closed coefficient syntax. This is the only reification outcome that permits an optional coefficient handler.

• expr : Lean.Expr

  The source coefficient that rational normalization did not recognize.

• closed : ClosedCoefficient

  The checked closed value, including explicit local-equality witnesses.

def Hex.RCF.Reify.UnsupportedCoefficient.message (reason : UnsupportedCoefficient) : Lean.MessageData

Preserve the rational frontend's diagnostic when no handler accepts.

Equations

• reason.message = Lean.toMessageData "rcf: symbolic or non-rational coefficient" ++ Lean.toMessageData (Lean.indentExpr reason.expr)

def Hex.RCF.Reify.recognizeCoefficient (e : Lean.Expr) : ExceptT UnsupportedCoefficient Lean.MetaM ℚ

Probe one scalar through the rational frontend's typed recognition boundary. Unsupported closed syntax is a result; runtime/resource exceptions propagate. The probe preserves caller metavariable state.

Equations

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

def Hex.RCF.Reify.sentenceExpr : Sentence → Lean.MetaM Lean.Expr

Literal reflected sentence.

Equations

• One or more equations did not get rendered due to their size.
• Hex.RCF.Reify.sentenceExpr (Hex.RCF.Sentence.forallReal formula) = do let __do_lift ← Hex.RCF.Reify.formulaExpr✝ formula Lean.Meta.mkAppM `Hex.RCF.Sentence.forallReal #[__do_lift]
• Hex.RCF.Reify.sentenceExpr (Hex.RCF.Sentence.existsReal formula) = do let __do_lift ← Hex.RCF.Reify.formulaExpr✝ formula Lean.Meta.mkAppM `Hex.RCF.Sentence.existsReal #[__do_lift]

def Hex.RCF.Reify.certificateExpr : Certificate → Lean.MetaM Lean.Expr

Literal top-level replay certificate.

Equations

• One or more equations did not get rendered due to their size.
• Hex.RCF.Reify.certificateExpr Hex.RCF.Certificate.emptyIoc = pure (Lean.mkConst `Hex.RCF.Certificate.emptyIoc)
• Hex.RCF.Reify.certificateExpr Hex.RCF.Certificate.constants = pure (Lean.mkConst `Hex.RCF.Certificate.constants)

structure Hex.RCF.Reify.SentenceResult : Type

Runtime and literal forms of a reflected sentence, together with its checked equivalence to the source goal.

• sentence : Sentence

  The reflected sentence used by compiled certificate construction.

• expr : Lean.Expr

  The literal expression representing sentence in the generated proof.

• proof : Lean.Expr

  A proof that sentence is equivalent to the source goal.

def Hex.RCF.Reify.recognizeSentence (source : Lean.Expr) : ExceptT UnsupportedCoefficient Lean.MetaM SentenceResult

Reify one singly quantified real sentence, distinguishing unsupported closed coefficients from terminal syntax, proof and resource errors.

Equations

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

def Hex.RCF.Reify.reifySentence (source : Lean.Expr) : Lean.MetaM SentenceResult

Reify a rational sentence, reporting unsupported coefficients as diagnostics for callers that do not participate in optional handler dispatch.

Equations

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