Documentation

HexRCF.Reify

source
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.

source
theorem Hex.RCF.Atom.toProp_iff_scale {p : ZPoly} {cmp : Cmp} {x lhs rhs scale : ℝ} (hscale : 0 < scale) (heval : (Polynomial.aeval x) (HexPolyZMathlib.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.

source
theorem Hex.RCF.Atom.toProp_iff_natScale {p : ZPoly} {cmp : Cmp} {x lhs rhs : ℝ} {scale : ℕ} (hscale : 0 < scale) (heval : (Polynomial.aeval x) (HexPolyZMathlib.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.

source
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.

source
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.

source
theorem Hex.RCF.Sentence.forallIoc_iff {a b : Dyadic} {a' b' : ℝ} {formula : Formula} {predicate : ℝ → Prop} (ha : HexRealRootsMathlib.Dyadic.toReal a = a') (hb : HexRealRootsMathlib.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.

source
theorem Hex.RCF.Sentence.existsIoc_iff {a b : Dyadic} {a' b' : ℝ} {formula : Formula} {predicate : ℝ → Prop} (ha : HexRealRootsMathlib.Dyadic.toReal a = a') (hb : HexRealRootsMathlib.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.

source
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
Instances For
    source
    def Hex.RCF.Reify.sentenceExpr :
    Sentence → Lean.MetaM Lean.Expr

    Literal reflected sentence.

    Equations
    Instances For
      source
      def Hex.RCF.Reify.certificateExpr :
      Certificate → Lean.MetaM Lean.Expr

      Literal top-level replay certificate.

      Equations
      Instances For
        source
        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.

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

          Reify one supported, singly quantified real sentence.

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