hex

39.6. HexOrderedFn: real constants and infinitesimals🔗

39.6.1. Ordered rational-function extensions🔗

HexOrderedFn orders exact rational functions in a new indeterminate. The indeterminate can represent a positive infinitesimal, or a real constant with caller-supplied rational approximations. Arithmetic uses the canonical fractions from HexRationalFn; normalization and equality remain exact. The computational library is Mathlib-free. Import HexOrderedFnTheory for the interpretation and order proofs.

The two constructions answer different questions. An infinitesimal is positive and smaller than every positive predecessor coefficient. A real constant is interpreted in ℝ: containment proofs justify its finite sign checks, while narrowing bounds and relative transcendence justify a total ordered field. At each real extension, relative transcendence means that no nonzero polynomial over the entire predecessor field vanishes at the new constant.

39.6.2. Positive infinitesimals🔗

For a nonzero fraction P/Q, the infinitesimal sign is the product of the signs of the lowest nonzero coefficients of P and Q. The denominator coefficient matters even though the denominator is monic. Zero is detected from the canonical numerator without calling the predecessor sign.

🔗def
Hex.OrderedFn.Infinitesimal.sign.{u} {K : Type u} [Lean.Grind.Field K]
  [DecidableEq K] (baseSign : K → ℤ) (f : Hex.RationalFn K) : ℤ
Hex.OrderedFn.Infinitesimal.sign.{u}
  {K : Type u} [Lean.Grind.Field K]
  [DecidableEq K] (baseSign : K → ℤ)
  (f : Hex.RationalFn K) : ℤ

Sign at a positive infinitesimal, using the predecessor field's total sign. Both coefficients matter: a monic denominator can have a negative lowest coefficient.

🔗def
Hex.OrderedFn.Infinitesimal.compare.{u} {K : Type u}
  [Lean.Grind.Field K] [DecidableEq K] (baseSign : K → ℤ)
  (f g : Hex.RationalFn K) : Ordering
Hex.OrderedFn.Infinitesimal.compare.{u}
  {K : Type u} [Lean.Grind.Field K]
  [DecidableEq K] (baseSign : K → ℤ)
  (f g : Hex.RationalFn K) : Ordering

Compare canonical fractions by the sign of their difference.

Opening the infinitesimal scope enables comparisons on RationalFn K. The snippets here use import HexOrderedFnTheory. For computation alone, use import HexOrderedFn and omit the local Mathlib dictionary selection. Here the denominator ε-1 and its inverse are both negative:

open Hex Hex.OrderedFn namespace OrderedFnInfinitesimals open scoped Hex.OrderedFn.Infinitesimal attribute [local instance 2000] Field.toGrindField def epsilon : RationalFn Rat := RationalFn.X #guard 0 < epsilon #guard epsilon < RationalFn.C (1/100 : Rat) #guard Infinitesimal.sign orderSign (1 / (epsilon - 1)) = -1 #guard Infinitesimal.compare orderSign epsilon (RationalFn.C (1 : Rat)) = .lt end OrderedFnInfinitesimals

The explicit sign and compare functions accept a predecessor sign function. The companion proves the order laws when that function agrees with the predecessor's order. The scope is opt-in; while it is open, RationalFn K uses the infinitesimal order on the available ordered coefficient field. Registered real extensions use a separate wrapper.

With the companion import, that same scope also installs its proved LinearOrder, IsStrictOrderedRing and core Lean.Grind.OrderedRing instances. These make ordinary ordered-field lemmas available on the executable carrier.

The examples select Field.toGrindField locally before forming their carriers. This keeps the coefficient arithmetic dictionary consistent with the companion's Mathlib field. When transporting fractions formed with the core rational dictionary, use HexRationalFnTheory.ratField_eq by an explicit rewrite or equality transport to the companion dictionary; the two rational dictionaries do not unify definitionally. The existing LiouvilleCoreTests fixture demonstrates this transport. The generic HexRationalFnTheory.coreField_eq identifies the field induced on a rational-function carrier with its original core field.

39.6.3. Successive infinitesimals🔗

At a second level, coefficients are themselves rational functions in the first infinitesimal. The new indeterminate δ is smaller than every positive element of the preceding field, including every natural power of ε:

namespace OrderedFnSuccessive open scoped Hex.OrderedFn.Infinitesimal attribute [local instance 2000] Field.toGrindField abbrev First := RationalFn Rat abbrev Second := RationalFn First def epsilon : First := RationalFn.X def delta : Second := RationalFn.X #guard 0 < delta #guard delta < RationalFn.C (epsilon ^ 3) example (n : ℕ) : delta < RationalFn.C (epsilon ^ n) := Infinitesimal.X_lt_pow n example (n : ℤ) : (n : First) < epsilon⁻¹ := Infinitesimal.intCast_lt_inv_X n end OrderedFnSuccessive

RationalFn.C embeds a predecessor value; RationalFn.X introduces the current level's indeterminate. These two operations distinguish ε from δ even though both are written as X in their own fields.

39.6.4. Exact bounds and finite signs🔗

Hex.OrderedFn.Oracle.Bounds stores rational lower and upper endpoints with a proof that they are ordered. It does not itself assert containment of a real value. Addition and four-endpoint multiplication compute exact enclosures; Bounds.div? requires the denominator bound to exclude zero.

🔗def
Hex.OrderedFn.Oracle.Bounds.sign? (a : Hex.OrderedFn.Oracle.Bounds) :
  Option ℤ
Hex.OrderedFn.Oracle.Bounds.sign?
  (a : Hex.OrderedFn.Oracle.Bounds) :
  Option ℤ

Only strictly separated bounds yield a nonzero sign.

🔗def
Hex.OrderedFn.Oracle.Bounds.exactSign?
  (a : Hex.OrderedFn.Oracle.Bounds) : Option ℤ
Hex.OrderedFn.Oracle.Bounds.exactSign?
  (a : Hex.OrderedFn.Oracle.Bounds) :
  Option ℤ

Finite evaluation can additionally certify zero from an exact singleton.

Hex.OrderedFn.Oracle.Approximation contains two procedures: one bounds a predecessor coefficient, and one bounds the new constant. Each receives a requested rational width. Approximation.ofConstant starts over rational coefficients using exact singleton bounds.

🔗def
Hex.OrderedFn.Real.enclose.{u} {K : Type u} [Lean.Grind.Field K]
  [DecidableEq K] (a : Hex.OrderedFn.Oracle.Approximation K)
  (p : Hex.DensePoly K) (δ : ℚ) : Hex.OrderedFn.Oracle.Bounds
Hex.OrderedFn.Real.enclose.{u}
  {K : Type u} [Lean.Grind.Field K]
  [DecidableEq K]
  (a :
    Hex.OrderedFn.Oracle.Approximation K)
  (p : Hex.DensePoly K) (δ : ℚ) :
  Hex.OrderedFn.Oracle.Bounds

Exact Horner bounds, refining every coefficient and the argument together.

🔗def
Hex.OrderedFn.Real.sign?.{u} {K : Type u} [Lean.Grind.Field K]
  [DecidableEq K] (a : Hex.OrderedFn.Oracle.Approximation K)
  (f : Hex.RationalFn K) (fuel : ℕ) : Option ℤ
Hex.OrderedFn.Real.sign?.{u} {K : Type u}
  [Lean.Grind.Field K] [DecidableEq K]
  (a :
    Hex.OrderedFn.Oracle.Approximation K)
  (f : Hex.RationalFn K) (fuel : ℕ) :
  Option ℤ

Optional finite evaluation. Fuel counts trials, beginning at precision zero; this function is never a coefficient field operation.

Consider a constant known to lie between 7/5 and 3/2. Those bounds separate X-1 and X-2 from zero, but leave X²-2 unresolved. A finite query can use the same bounds at every trial:

namespace OrderedFnFinite attribute [local instance 2000] Field.toGrindField open Oracle def source : Approximation Rat := .ofConstant (fun _ => ⟨7/5, 3/2, x✝:ℚ⊢ 7 / 5 ≤ 3 / 2 All goals completed! 🐙⟩) def linear (q : Rat) : RationalFn Rat := RationalFn.ofPoly (#p[-q, 1]) #guard Real.sign? source (linear 1) 1 = some 1 #guard Real.sign? source (linear 2) 1 = some (-1) #guard Real.sign? source (RationalFn.ofPoly (#p[-2, 0, 1])) 4 = none theorem source_correct : ApproximationCorrect (Rat.castHom ℝ) (_root_.Real.sqrt 2) source := SemanticTests.sqrt_correct example : (1 : Int) = sgn (Real.eval (Rat.castHom ℝ) (_root_.Real.sqrt 2) (linear 1)) := (Real.sign?_sound source_correct _ 1 (⊢ Real.sign? source (linear 1) 1 = some 1 All goals completed! 🐙)).1 end OrderedFnFinite

The computation needs only endpoint data; its mathematical conclusion needs a containment proof for this provider, subject and embedding. Here source_correct reuses the companion test's proof for Real.sqrt 2. That algebraic subject is suitable for finite checks, but cannot supply a transcendental registration. Fuel exhaustion returns none; this includes a denominator that remains unseparated from zero. A zero-containing interval does not prove a zero value; an exact singleton zero can do so.

🔗theorem
Hex.OrderedFn.Real.sign?_sound.{u} {K : Type u} [Field K]
  [DecidableEq K] {ι : K →+* ℝ} {τ : ℝ}
  {a : Hex.OrderedFn.Oracle.Approximation K}
  (ha : Hex.OrderedFn.Oracle.ApproximationCorrect ι τ a)
  (f : Hex.RationalFn K) (fuel : ℕ) {s : ℤ}
  (hs : Hex.OrderedFn.Real.sign? a f fuel = some s) :
  s = Hex.OrderedFn.Oracle.sgn (Hex.OrderedFn.Real.eval ι τ f) ∧
    Polynomial.eval₂ ι τ (HexPolyTheory.toPolynomial f.den) ≠ 0
Hex.OrderedFn.Real.sign?_sound.{u}
  {K : Type u} [Field K] [DecidableEq K]
  {ι : K →+* ℝ} {τ : ℝ}
  {a :
    Hex.OrderedFn.Oracle.Approximation K}
  (ha :
    Hex.OrderedFn.Oracle.ApproximationCorrect
      ι τ a)
  (f : Hex.RationalFn K) (fuel : ℕ)
  {s : ℤ}
  (hs :
    Hex.OrderedFn.Real.sign? a f fuel =
      some s) :
  s =
      Hex.OrderedFn.Oracle.sgn
        (Hex.OrderedFn.Real.eval ι τ f) ∧
    Polynomial.eval₂ ι τ
        (HexPolyTheory.toPolynomial
          f.den) ≠
      0

A successful finite sign query agrees with real evaluation and certifies nonvanishing of the canonical denominator, using containment for this provider.

The theorem also proves that the normalized denominator evaluates to a nonzero value. A source expression may have additional divisor conditions that normalization removed. For example, formal cancellation makes (X-2)/(X-2) equal to one, but at the real subject 2 the original division is 0/0. Expression consumers must retain the original divisor hypotheses when interpreting that cancellation.

39.6.5. Registered real extensions🔗

Hex.OrderedFn.Real.Registration fixes the provider together with termination proofs for every sign and approximation query. The companion's Hex.OrderedFn.Real.Valid supplies sufficient semantic hypotheses: containment, requested-width guarantees, and transcendence relative to the chosen predecessor embedding. Its registration constructor derives the termination proofs for the actual refinement search.

To extend an already ordered predecessor field, also require the chosen embedding ι to be strictly monotone. Valid does not include that condition: it justifies the real interpretation's order, which can differ from a previously chosen order on the predecessor. Extension.C_lt uses StrictMono ι to prove agreement on embedded coefficients.

Over the rationals, Rat.cast_strictMono supplies this condition. At a successive real level, Extension.eval_strictMono supplies it under the local LinearOrder built from that theorem's same witness tuple.

🔗theorem
Hex.OrderedFn.Real.Extension.C_lt.{u} {K : Type u} [Field K]
  [DecidableEq K] {ι : K →+* ℝ} {τ : ℝ}
  {r : Hex.OrderedFn.Real.Registration K} [LinearOrder K]
  (ha : Hex.OrderedFn.Oracle.ApproximationCorrect ι τ r.source)
  (ht : Hex.OrderedFn.Real.RelativeTranscendence ι τ)
  (hι : StrictMono ⇑ι) (c d : K) :
  Hex.OrderedFn.Real.Extension.C c < Hex.OrderedFn.Real.Extension.C d ↔
    c < d
Hex.OrderedFn.Real.Extension.C_lt.{u}
  {K : Type u} [Field K] [DecidableEq K]
  {ι : K →+* ℝ} {τ : ℝ}
  {r : Hex.OrderedFn.Real.Registration K}
  [LinearOrder K]
  (ha :
    Hex.OrderedFn.Oracle.ApproximationCorrect
      ι τ r.source)
  (ht :
    Hex.OrderedFn.Real.RelativeTranscendence
      ι τ)
  (hι : StrictMono ⇑ι) (c d : K) :
  Hex.OrderedFn.Real.Extension.C c <
      Hex.OrderedFn.Real.Extension.C d ↔
    c < d

An order-preserving predecessor embedding preserves coefficient order.

🔗def
Hex.OrderedFn.Real.registration.{u} {K : Type u} [Field K]
  [DecidableEq K] {a : Hex.OrderedFn.Oracle.Approximation K}
  (h : Hex.OrderedFn.Real.Valid a) : Hex.OrderedFn.Real.Registration K
Hex.OrderedFn.Real.registration.{u}
  {K : Type u} [Field K] [DecidableEq K]
  {a :
    Hex.OrderedFn.Oracle.Approximation K}
  (h : Hex.OrderedFn.Real.Valid a) :
  Hex.OrderedFn.Real.Registration K

Register a provider with structurally erased semantic evidence.

registration_source identifies the fixed provider without unfolding registration. Valid.orderValid supplies the order hypothesis for the registration produced from that same validity proof. It lets callers install the registered order without extracting the existential semantic witnesses. OrderValid.strictOrderedRing and OrderValid.orderedRing supply its Mathlib and native ordered-ring laws:

namespace RegisteredOrder open Oracle variable {K : Type} [Field K] variable [DecidableEq K] variable {a : Approximation K} example (h : Real.Valid a) : LinearOrder (Real.Extension (Real.registration h)) := Real.Extension.linearOrder h.orderValid example (h : Real.Valid a) (f : Real.Extension (Real.registration h)) : let := Real.Extension.linearOrder h.orderValid 0 ≤ f * f := K:Typeinst✝¹:Field Kinst✝:DecidableEq Ka:Approximation Kh:Real.Valid af:Real.Extension (Real.registration h)⊢ let this := Real.Extension.linearOrder ⋯; 0 ≤ f * f K:Typeinst✝¹:Field Kinst✝:DecidableEq Ka:Approximation Kh:Real.Valid af:Real.Extension (Real.registration h)this:LinearOrder (Real.Extension (Real.registration h)) := Real.Extension.linearOrder ⋯⊢ let this := Real.Extension.linearOrder ⋯; 0 ≤ f * f K:Typeinst✝¹:Field Kinst✝:DecidableEq Ka:Approximation Kh:Real.Valid af:Real.Extension (Real.registration h)this✝:LinearOrder (Real.Extension (Real.registration h)) := Real.Extension.linearOrder ⋯this:have this := Real.Extension.linearOrder ⋯; IsStrictOrderedRing (Real.Extension (Real.registration h)) := ···⊢ let this := Real.Extension.linearOrder ⋯; 0 ≤ f * f K:Typeinst✝¹:Field Kinst✝:DecidableEq Ka:Approximation Kh:Real.Valid af:Real.Extension (Real.registration h)this✝¹:LinearOrder (Real.Extension (Real.registration h)) := Real.Extension.linearOrder ⋯this✝:have this := Real.Extension.linearOrder ⋯; IsStrictOrderedRing (Real.Extension (Real.registration h)) := ···this:let this := Real.Extension.linearOrder ⋯; Lean.Grind.OrderedRing (Real.Extension (Real.registration h)) := ···⊢ let this := Real.Extension.linearOrder ⋯; 0 ≤ f * f All goals completed! 🐙 end RegisteredOrder

Hex.OrderedFn.Real.Extension wraps a canonical fraction with this fixed registration. Extension.C embeds a predecessor coefficient and Extension.X represents the registered real constant. The wrapper keeps its real order when used as the coefficient field for an infinitesimal.

🔗def
Hex.OrderedFn.Real.Extension.sign.{u} {K : Type u} [Lean.Grind.Field K]
  [DecidableEq K] {r : Hex.OrderedFn.Real.Registration K}
  (f : Hex.OrderedFn.Real.Extension r) : ℤ
Hex.OrderedFn.Real.Extension.sign.{u}
  {K : Type u} [Lean.Grind.Field K]
  [DecidableEq K]
  {r : Hex.OrderedFn.Real.Registration K}
  (f : Hex.OrderedFn.Real.Extension r) : ℤ

Total sign using this registration's fixed source.

🔗def
Hex.OrderedFn.Real.Extension.approx.{u} {K : Type u}
  [Lean.Grind.Field K] [DecidableEq K]
  {r : Hex.OrderedFn.Real.Registration K}
  (f : Hex.OrderedFn.Real.Extension r) (δ : ℚ) :
  Hex.OrderedFn.Oracle.Bounds
Hex.OrderedFn.Real.Extension.approx.{u}
  {K : Type u} [Lean.Grind.Field K]
  [DecidableEq K]
  {r : Hex.OrderedFn.Real.Registration K}
  (f : Hex.OrderedFn.Real.Extension r)
  (δ : ℚ) : Hex.OrderedFn.Oracle.Bounds

Refine a quotient enclosure to the requested width.

For a nonzero formal fraction, sign refinement narrows bounds for both numerator and denominator until each has a strict sign. Formal zero returns immediately. The termination proofs erase from compiled execution; they do not impose a fuel limit. Positive approximation requests return bounds of at most the requested width. Nonpositive requests instead ask for width one, while still preserving containment.

Each trial computes fresh coefficient and constant bounds at precision 2^(-n). At a further real level, coefficient approximations themselves run refinement searches; their cost depends on the caller's providers.

A further real registration uses Extension.approximation to obtain bounds for its predecessor coefficients. Each new real constant needs relative transcendence over that entire predecessor field. Separate transcendence of two constants over the rationals does not establish this condition. The fixture's LiouvilleTests.second_valid proves validity under explicit hypotheses on its new constant and provider; secondRegistration constructs the corresponding registration. For a fixed relatively transcendental subject, containment proofs for both providers and the same embedding suffice to preserve order through Extension.transport_lt.

39.6.6. The Mathlib correspondence🔗

The infinitesimal embedding maps canonical fractions into the lexicographically ordered Hahn field with integer exponents. Its leading coefficient order agrees with the executable scan. The public theorems Infinitesimal.X_pos and X_lt_C establish positivity and the comparison with every positive predecessor coefficient; X_lt_pow supplies the successive-level law used above. Infinitesimal.towerEmbed and towerEmbed_lt embed the two-level field into its iterated Hahn model and preserve and reflect order.

🔗def
Hex.OrderedFn.Infinitesimal.embed.{u} {K : Type u} [Field K]
  [DecidableEq K] : Hex.RationalFn K →+* Lex (HahnSeries ℤ K)
Hex.OrderedFn.Infinitesimal.embed.{u}
  {K : Type u} [Field K] [DecidableEq K] :
  Hex.RationalFn K →+*
    Lex (HahnSeries ℤ K)

Interpret canonical fractions as lexicographically ordered Laurent series.

🔗theorem
Hex.OrderedFn.Infinitesimal.sign_orderSign.{u} {K : Type u} [Field K]
  [DecidableEq K] [LinearOrder K] [IsStrictOrderedRing K]
  (f : Hex.RationalFn K) :
  Hex.OrderedFn.Infinitesimal.sign Hex.OrderedFn.orderSign f =
    ↑(SignType.sign (Hex.OrderedFn.Infinitesimal.embed f))
Hex.OrderedFn.Infinitesimal.sign_orderSign.{u}
  {K : Type u} [Field K] [DecidableEq K]
  [LinearOrder K] [IsStrictOrderedRing K]
  (f : Hex.RationalFn K) :
  Hex.OrderedFn.Infinitesimal.sign
      Hex.OrderedFn.orderSign f =
    ↑(SignType.sign
        (Hex.OrderedFn.Infinitesimal.embed
          f))

The infinitesimal sign agrees with the sign in the Hahn field.

🔗theorem
Hex.OrderedFn.Infinitesimal.embed_lt.{u} {K : Type u} [Field K]
  [DecidableEq K] [LinearOrder K] [IsStrictOrderedRing K]
  (f g : Hex.RationalFn K) :
  f < g ↔
    Hex.OrderedFn.Infinitesimal.embed f <
      Hex.OrderedFn.Infinitesimal.embed g
Hex.OrderedFn.Infinitesimal.embed_lt.{u}
  {K : Type u} [Field K] [DecidableEq K]
  [LinearOrder K] [IsStrictOrderedRing K]
  (f g : Hex.RationalFn K) :
  f < g ↔
    Hex.OrderedFn.Infinitesimal.embed f <
      Hex.OrderedFn.Infinitesimal.embed g

Strict comparison is the pullback of the ordered Hahn model.

🔗theorem
Hex.OrderedFn.Infinitesimal.mapHom_sign.{u, v} {K : Type u} [Field K]
  [DecidableEq K] [LinearOrder K] {L : Type v} [Field L] [DecidableEq L]
  [LinearOrder L] (f : K →+* L) (ordered : StrictMono ⇑f)
  (q : Hex.RationalFn K) :
  Hex.OrderedFn.Infinitesimal.sign Hex.OrderedFn.orderSign
      ((HexRationalFnTheory.mapHom f) q) =
    Hex.OrderedFn.Infinitesimal.sign Hex.OrderedFn.orderSign q
Hex.OrderedFn.Infinitesimal.mapHom_sign.{u,
    v}
  {K : Type u} [Field K] [DecidableEq K]
  [LinearOrder K] {L : Type v} [Field L]
  [DecidableEq L] [LinearOrder L]
  (f : K →+* L) (ordered : StrictMono ⇑f)
  (q : Hex.RationalFn K) :
  Hex.OrderedFn.Infinitesimal.sign
      Hex.OrderedFn.orderSign
      ((HexRationalFnTheory.mapHom f) q) =
    Hex.OrderedFn.Infinitesimal.sign
      Hex.OrderedFn.orderSign q

Coefficient-field embeddings preserve the selected infinitesimal sign.

Coefficient transport preserves signs and order under an ordered field embedding. The Hahn model is not real closed: an integer-exponent series cannot provide a square root of its exponent-one monomial. Algebraic adjunctions belong to the real-closure contract, whose full tower implementation and acceptance are separate obligations.

For a registered real extension, Extension.evalHom maps fractions into ℝ and is injective under relative transcendence. Containment proves that the executable sign and order agree with this interpretation. The companion supplies Mathlib field and order laws for the same computational arithmetic.

🔗theorem
Hex.OrderedFn.Real.Extension.sign_eq.{u} {K : Type u} [Field K]
  [DecidableEq K] {ι : K →+* ℝ} {τ : ℝ}
  {r : Hex.OrderedFn.Real.Registration K}
  (ha : Hex.OrderedFn.Oracle.ApproximationCorrect ι τ r.source)
  (ht : Hex.OrderedFn.Real.RelativeTranscendence ι τ)
  (f : Hex.OrderedFn.Real.Extension r) :
  f.sign =
    Hex.OrderedFn.Oracle.sgn
      ((Hex.OrderedFn.Real.Extension.evalHom ht) f)
Hex.OrderedFn.Real.Extension.sign_eq.{u}
  {K : Type u} [Field K] [DecidableEq K]
  {ι : K →+* ℝ} {τ : ℝ}
  {r : Hex.OrderedFn.Real.Registration K}
  (ha :
    Hex.OrderedFn.Oracle.ApproximationCorrect
      ι τ r.source)
  (ht :
    Hex.OrderedFn.Real.RelativeTranscendence
      ι τ)
  (f : Hex.OrderedFn.Real.Extension r) :
  f.sign =
    Hex.OrderedFn.Oracle.sgn
      ((Hex.OrderedFn.Real.Extension.evalHom
          ht)
        f)

The registered total sign agrees with the real embedding, under containment for its fixed provider and transcendence over the predecessor field.

🔗theorem
Hex.OrderedFn.Real.Extension.approx_contains.{u} {K : Type u} [Field K]
  [DecidableEq K] {ι : K →+* ℝ} {τ : ℝ}
  {r : Hex.OrderedFn.Real.Registration K}
  (ha : Hex.OrderedFn.Oracle.ApproximationCorrect ι τ r.source)
  (ht : Hex.OrderedFn.Real.RelativeTranscendence ι τ)
  (f : Hex.OrderedFn.Real.Extension r) (δ : ℚ) :
  Hex.OrderedFn.Oracle.Contains (f.approx δ)
    ((Hex.OrderedFn.Real.Extension.evalHom ht) f)
Hex.OrderedFn.Real.Extension.approx_contains.{u}
  {K : Type u} [Field K] [DecidableEq K]
  {ι : K →+* ℝ} {τ : ℝ}
  {r : Hex.OrderedFn.Real.Registration K}
  (ha :
    Hex.OrderedFn.Oracle.ApproximationCorrect
      ι τ r.source)
  (ht :
    Hex.OrderedFn.Real.RelativeTranscendence
      ι τ)
  (f : Hex.OrderedFn.Real.Extension r)
  (δ : ℚ) :
  Hex.OrderedFn.Oracle.Contains
    (f.approx δ)
    ((Hex.OrderedFn.Real.Extension.evalHom
        ht)
      f)

Approximation containment is separate from the core requested-width theorem.

A successful finite trial can also prove the total sign using Extension.sign_of_attempt. This lets the kernel check a supplied finite success without reducing the unbounded search or its termination proof.

The existing test-local Liouville provider illustrates a complete real registration: rational partial sums and tail bounds have proved containment and requested width, and liouvilleNumber 2 has proved transcendence. The fixture defines positive = X-5/4, negative = X-2 and their quotient. Its preparedPositive stores a literal normalized fraction that the kernel can reduce. A finite successful trial proves that prepared value's total sign from containment. Its equality with the arithmetic-built positive is formal and independent of the chosen real subject. The fixture proves that identity using positive_eq through injective real evaluation under transcendence; this is one proof route, rather than an extra hypothesis of the finite-success sign theorem.

For an already registered carrier, Extension.OrderValid requires containment and relative transcendence; it does not request the width guarantee again. Install the real order structures as local instances:

namespace OrderedFnLiouville attribute [local instance 2000] Field.toGrindField open Hex.OrderedFn.Real open Hex.OrderedFn.LiouvilleTests example : Extension.sign preparedPositive = 1 := Extension.sign_of_attempt source_correct _ (n := 2) (⊢ attempt registered.source preparedPositive.val 2 = some 1 All goals completed! 🐙) local instance : LinearOrder E := Extension.linearOrder ⟨Rat.castHom ℝ, liouvilleNumber 2, source_correct, transcendence⟩ local instance : IsStrictOrderedRing E := Extension.strictOrderedRing source_correct transcendence local instance : Lean.Grind.OrderedRing E := Extension.orderedRing source_correct transcendence example : (0 : E) < positive := (Extension.sign_pos_iff source_correct transcendence positive).mp positive_sign example : Extension.sign quotient = -1 := quotient_sign end OrderedFnLiouville

This fixture is imported explicitly from HexOrderedFnTheory.LiouvilleTests; it is not a bundled analytic provider in the ordinary library umbrella. The library supplies no providers for π or e. The companion's compiled hexorderedfn_liouville_test exercises the total search, approximation and a subsequent infinitesimal extension.

The real-closure specification prescribes order-preserving predecessor embeddings and stages in the order real constants, infinitesimals, then algebraic extensions. A positive infinitesimal over the rationals has no order-preserving real embedding. A later real registration could choose a different real interpretation of the formal rational functions, but its order would not extend that infinitesimal order. It therefore cannot serve as a subsequent stage with the prescribed order preservation. The existing Hex.RealClosure.BaseContext constructors already separate the real prefix from subsequent infinitesimals. See the selected-root RCF examples for delivered consumers. General tower-building and ordinary-real realization remain separate obligations.