39.9.1. Extending an ordered coefficient context🔗

HexRealClosure computes roots and builds finite algebraic towers over an ordered coefficient context. A root carries its selected embedding; a value carries the immutable context in which its arithmetic is valid. The library combines the polynomial kernels, Sturm queries, sign determination and ordered rational-function extensions.

Import HexRealClosure for the Mathlib-free computational API. The HexRealClosureTheory umbrella supplies the base-model proofs; the tower root and collection theorems below additionally require HexRealClosureTheory.TowerRoots and HexRealClosureTheory.RootCollection. The installed-catalog laws use HexRealClosureTheory.ReconciledCatalog; constructed-history gathering uses HexRealClosureTheory.ConstructedCatalog. The finite inverse laws use HexRealClosureTheory.SuppliedInverse. Those semantic modules belong to the HexQuerySemantics Lake target under adapters/ in the development tree. They build in hex-dev, but are not therefore available from a published companion. Both libraries are unreleased; Tau Ceti belongs only to their Mathlib proof layer.

The API describes finite constructed extensions. It does not identify raw polynomial quotients with fields, compute multivariate quantifier elimination, or install an ordinary-real interpretation of a positive infinitesimal. General finite ordinary-real realization and the full end-to-end family contract have separate proof requirements.

39.9.2. Real prefixes, infinitesimals and selected roots🔗

A base starts with rational coefficients, may extend them with registered real constants, and may then adjoin successive positive infinitesimals. A real constant has a caller-supplied rational bound provider. Its progress witnesses refer to the exact source formed from that provider and the predecessor's bounds. Semantic validity requires containment, narrowing widths and relative transcendence over the entire predecessor field. No bundled provider for π or e is supplied.

Hex.RealClosure.BaseContext.RealContext.constant
  {registry : Hex.RealClosure.BaseContext.Registry} {K : Type}
  [Lean.Grind.Field K] [DecidableEq K]
  {approx : K → ℚ → Hex.OrderedFn.Oracle.Bounds} {sign : K → ℤ}
  (parent :
    Hex.RealClosure.BaseContext.RealContext registry K approx sign)
  (key : Hex.RealClosure.BaseContext.ConstantKey)
  (present : (registry key).isSome = true)
  (sp :
    ∀ (f : Hex.RationalFn K),
      Acc
        (Hex.OrderedFn.Next
          (Hex.OrderedFn.Real.attempt (parent.source key present) f))
        0)
  (ap :
    ∀ (f : Hex.RationalFn K) (δ : ℚ),
      Acc
        (Hex.OrderedFn.Next
          (Hex.OrderedFn.Real.approxAttempt (parent.source key present)
            f (Hex.OrderedFn.Real.requestWidth δ)))
        0) :
  Hex.RealClosure.BaseContext.RealContext registry (Hex.RationalFn K)
    (fun f δ =>
      Hex.OrderedFn.Real.approx (parent.source key present) f δ ⋯)
    fun f => Hex.OrderedFn.Real.sign (parent.source key present) f ⋯
Hex.RealClosure.BaseContext.RealContext.constant
  {registry :
    Hex.RealClosure.BaseContext.Registry}
  {K : Type} [Lean.Grind.Field K]
  [DecidableEq K]
  {approx :
    K → ℚ → Hex.OrderedFn.Oracle.Bounds}
  {sign : K → ℤ}
  (parent :
    Hex.RealClosure.BaseContext.RealContext
      registry K approx sign)
  (key :
    Hex.RealClosure.BaseContext.ConstantKey)
  (present : (registry key).isSome = true)
  (sp :
    ∀ (f : Hex.RationalFn K),
      Acc
        (Hex.OrderedFn.Next
          (Hex.OrderedFn.Real.attempt
            (parent.source key present)
            f))
        0)
  (ap :
    ∀ (f : Hex.RationalFn K) (δ : ℚ),
      Acc
        (Hex.OrderedFn.Next
          (Hex.OrderedFn.Real.approxAttempt
            (parent.source key present) f
            (Hex.OrderedFn.Real.requestWidth
              δ)))
        0) :
  Hex.RealClosure.BaseContext.RealContext
    registry (Hex.RationalFn K)
    (fun f δ =>
      Hex.OrderedFn.Real.approx
        (parent.source key present) f δ ⋯)
    fun f =>
    Hex.OrderedFn.Real.sign
      (parent.source key present) f ⋯

The real prefix ends before the first infinitesimal. The base chain has no constructor adding a real constant after an infinitesimal. Algebraic extensions then use validated selected-root descriptors over their actual predecessor contexts.

A Tower.Context hides its concrete native coefficient carrier behind Hex.RealClosure.Tower.Context.Value. Use its total sign, compare and equal operations. Representation equality is not the criterion for mathematical equality of arbitrary selected-root values. The semantic companion interprets the supplied operations in an ordered field and reflects zero; it does not require injectivity of every stored representative.

39.9.3. Complete roots and original multiplicities🔗

The generic root API takes a coefficient sign function and a literal context. Under the companion's coefficient-model laws, it returns the all-roots case exactly for zero, and a finite list otherwise. A nonzero constant and a root-free polynomial give an empty finite list.

Hex.RealClosure.Roots.roots.{u, v} {E : Type u} {Ctx : Type v} [Zero E]
  [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [NatCast E] [Neg E]
  [Inv E] [Div E] [DecidableEq Ctx] (sign : E → ℤ) (context : Ctx)
  (p : Hex.DensePoly E) : Hex.RealClosure.Roots.Output sign context
Hex.RealClosure.Roots.roots.{u, v}
  {E : Type u} {Ctx : Type v} [Zero E]
  [DecidableEq E] [One E] [Add E] [Sub E]
  [Mul E] [NatCast E] [Neg E] [Inv E]
  [Div E] [DecidableEq Ctx] (sign : E → ℤ)
  (context : Ctx) (p : Hex.DensePoly E) :
  Hex.RealClosure.Roots.Output sign
    context

Zero extraction and Yun decomposition recover multiplicities from the original polynomial, before sorting roots across factors. Entries retain positive multiplicity labels. Squarefree decomposition is an internal step: a repeated-root input is valid here, unlike a raw Sturm query head.

The following small example reuses the cases checked by the owner's root-factor suite. The polynomial X²(X-1)³ has two distinct roots with multiplicities two and three:

The diagnostic operation Hex.RealClosure.Roots.roots? exposes internal producer errors for arbitrary coefficient operations. The ordinary operation has a diagnostic panic fallback of .all, inherited by the tower and rational wrappers. Outside the coefficient-model laws, this fallback must not be taken as proof that the input was zero. Use roots? to retain explicit errors. The companion proves that the actual construction succeeds under its interpretation laws; an example's successful output cannot discharge that general obligation.

39.9.4. Native root contexts and coefficient embeddings🔗

Hex.RealClosure.Tower.Context.roots
  {registry : Hex.RealClosure.BaseContext.Registry}
  (parent : Hex.RealClosure.Tower.Context registry)
  (p : Hex.DensePoly parent.Value) :
  Hex.RealClosure.Tower.RootSet parent
Hex.RealClosure.Tower.Context.roots
  {registry :
    Hex.RealClosure.BaseContext.Registry}
  (parent :
    Hex.RealClosure.Tower.Context
      registry)
  (p : Hex.DensePoly parent.Value) :
  Hex.RealClosure.Tower.RootSet parent

A native root is either a predecessor coefficient point or a selected root in the child actually returned by adjoining its descriptor. Each entry keeps the original multiplicity. A point stays in the parent; a selected root stores the descriptor, child context and selected generator.

Use Hex.RealClosure.Tower.Root.context and Hex.RealClosure.Tower.Root.value together. To enter that context, map predecessor coefficients with Hex.RealClosure.Tower.Root.embed. Hex.RealClosure.Tower.Root.embedPoly maps a polynomial's coefficients, and Hex.RealClosure.Tower.Root.signAt evaluates it at the stored root. Root.compare compares roots of the shared input context while keeping their different child ownership explicit. Its diagnostic panic fallback is .eq; use Hex.RealClosure.Tower.Root.compare? to retain errors. The companion's model laws exclude this fallback.

Hex.RealClosure.Tower.Context.adjoin
  {registry : Hex.RealClosure.BaseContext.Registry}
  (context : Hex.RealClosure.Tower.Context registry)
  (descriptor :
    Hex.SignDet.Descriptor context.Value Hex.RealClosure.Tower.Signature
      context.sign context.signature) :
  Hex.RealClosure.Tower.Extension context descriptor
Hex.RealClosure.Tower.Context.adjoin
  {registry :
    Hex.RealClosure.BaseContext.Registry}
  (context :
    Hex.RealClosure.Tower.Context
      registry)
  (descriptor :
    Hex.SignDet.Descriptor context.Value
      Hex.RealClosure.Tower.Signature
      context.sign context.signature) :
  Hex.RealClosure.Tower.Extension context
    descriptor

The low-level selected algebraic carrier represents a polynomial's value at one root. Its defining polynomial may be reducible. The carrier stores zero canonically, and every other element carries a checked nonzero sign. The companion derives zero reflection from the predecessor laws with Hex.RealClosure.Algebraic.Element.denote_eq_zero, so a ≠ 0 implies a nonzero value. Nonzero values can still have several stored representatives. The quotient by the whole defining polynomial need not be a field, so xgcd inversion modulo that polynomial is insufficient. Inversion uses selected-root tests and the appropriate cofactor. The semantic proofs justify the actual operation rather than granting a field instance to raw representatives.

Clean monic definitions allow stored remainder reduction. Non-monic or unclean definitions retain their raw policy; scaled pseudo-remainders must not be substituted for value-preserving remainders. This policy changes representation and costs, while the companion proves value preservation for the transformations that actually apply.

39.9.5. Checking a supplied inverse🔗

A retained inverse can certify two different things. An Inverse record binds the output's original polynomial to the native algorithm's actual candidate. Its Inverse.native theorem identifies the packed output with the native inverse. A Inverse.Equation record instead checks that a supplied output is an inverse at the selected root. It retains the operand and checked signs of the operand and the residual operand · output - 1. Those signs must be the operand's nonzero cached sign and zero. This permits an inverse with a different polynomial representation.

Hex.RealClosure.Algebraic.Packing.Inverse.Equation.make?.{u, v}
  {E : Type u} {Ctx : Type v} [Zero E] [DecidableEq E] [One E] [Add E]
  [Neg E] [Sub E] [Mul E] [Inv E] [Div E] [NatCast E] [DecidableEq Ctx]
  {coeffSign : E → ℤ} {parent : Ctx}
  {context : Hex.RealClosure.Algebraic.Context E Ctx coeffSign parent}
  (argument : Hex.RealClosure.Algebraic.Element context)
  (entry : Hex.RealClosure.Algebraic.Packing context)
  (signs :
    Hex.SignDet.SelectedSigns context.root
      [argument.polynomial,
        argument.polynomial * entry.value.polynomial - 1]) :
  Option (Hex.RealClosure.Algebraic.Packing.Inverse.Equation entry)
Hex.RealClosure.Algebraic.Packing.Inverse.Equation.make?.{u,
    v}
  {E : Type u} {Ctx : Type v} [Zero E]
  [DecidableEq E] [One E] [Add E] [Neg E]
  [Sub E] [Mul E] [Inv E] [Div E]
  [NatCast E] [DecidableEq Ctx]
  {coeffSign : E → ℤ} {parent : Ctx}
  {context :
    Hex.RealClosure.Algebraic.Context E
      Ctx coeffSign parent}
  (argument :
    Hex.RealClosure.Algebraic.Element
      context)
  (entry :
    Hex.RealClosure.Algebraic.Packing
      context)
  (signs :
    Hex.SignDet.SelectedSigns context.root
      [argument.polynomial,
        argument.polynomial *
            entry.value.polynomial -
          1]) :
  Option
    (Hex.RealClosure.Algebraic.Packing.Inverse.Equation
      entry)

Use Inverse.Equation.readMemo? to obtain that record from an already checked sign graph. The reader binds the operand, supplied output and selected root through the exact query slice; it does not produce new sign evidence or compute an inverse candidate. Inverse.Equation.make?_self proves rechecking a retained record succeeds. An existing native inverse record can be converted with Inverse.toEquation, retaining its operand and literal replay evidence.

The existing InverseFact dictionaries and Element.replayInverse and Element.replayQuotient operations require the native record. A supplied equation proves a value equation at the selected root, not equality of stored Element representatives, and cannot replace that record in these operations.

The supplied-equation semantics have two useful interfaces. Inverse.Equation.denote_inv proves the inverse law under a lawful predecessor interpretation into an ordered real-closed field. For a reader justified only on reached coefficients, Inverse.Equation.eval_inv instead uses zero and unit preservation, the reached product and subtraction relations, and the two observed signs at a chosen point.

Inverse.Equation.atPoint places the output and operand at the descriptor's shared finite selected point in an ordered real-closed field. Its premises are zero and unit preservation, reached descriptor data and Inverse.Equation.Data. The latter supplies the original packing's replay and subtraction relation, the inverse equation's replay, and the reached product and subtraction relations. The conclusion gives the original packing equation, the inverse law and both cached signs at that same point. The stronger native record's finite data converts with Inverse.Data.toEquation. These interfaces require the caller to supply their semantic premises; assembling them recursively through a whole tower remains a separate task. Canonical zero uses Element.inv_zero and does not need a nonzero inverse record. Source-expression divisor guards remain an obligation of the expression consumer.

The existing InversePackingTests runs both readers on monic and non-monic reducible defining polynomials. It checks acceptance of a supplied alternate inverse and rejection of a bad inverse, changed operand, wrong root domain, out-of-range memo index and zero operand. These finite controls complement the general conditional laws; they do not construct their semantic premises for an arbitrary tower.

39.9.6. Enlargement and live transport🔗

Adding an infinitesimal below an existing algebraic suffix requires rebuilding that suffix over the extended base. A descriptor, polynomial or value from the old context does not automatically acquire the new binding.

Hex.RealClosure.Tower.Context.enlargeWithParameter?
  {registry : Hex.RealClosure.BaseContext.Registry}
  (source : Hex.RealClosure.Tower.Context registry) :
  Option (Hex.RealClosure.Tower.Enlargement source)
Hex.RealClosure.Tower.Context.enlargeWithParameter?
  {registry :
    Hex.RealClosure.BaseContext.Registry}
  (source :
    Hex.RealClosure.Tower.Context
      registry) :
  Option
    (Hex.RealClosure.Tower.Enlargement
      source)

The result contains the actual conversion and its new parameter. Use the returned conversion for old values; compose conversions explicitly for later extensions. Its cached parameter uses the same reconstructed suffix and does not trigger another reconstruction.

Consumers gathering several live values must include every required owner, coefficient and root dependency. Preserving one selected value is weaker than all-live preservation. The merged enlargement and transport theorems have explicit source/target models and dependency premises; they do not by themselves construct all arithmetic facts needed for an arbitrary accepted serialized tower.

39.9.7. Gathering owners into one context🔗

A Hex.RealClosure.Tower.Live.Request records the live operands and root descriptors that must move together. Gathering retains each requested owner's ancestry. Use Hex.RealClosure.Tower.Live.Request.gatherReconciled? with an explicit packed base: it gathers those owners, transports the requested operands and revalidates the descriptors in one returned context. The result retains both the original request and the checked conversions. Its Hex.RealClosure.Tower.Live.Request.gatherReconciled?_shared law identifies the actual successful owner gather used by the live collection.

This route permits different orders of registered provider keys. It preserves the existing ordered conversion when one is available; otherwise it uses the checked provider reconciliation. Key coverage and infinitesimal depth are checked on both paths. The reordering fallback and catalog selection also check key distinctness; on the ordered path, distinctness follows from the target's realization. A matching key list alone does not supply the providers' semantic laws.

For automatic base selection, use Hex.RealClosure.Tower.Live.Request.gatherReconciledFrom? with a Hex.RealClosure.BaseContext.Catalog of installed real prefixes. This is the base-provider catalog, distinct from the tower-handle catalog used to read stored values. The operation selects the first key-compatible prefix in catalog order: the rational prefix comes first, then installed prefixes from newest to oldest. It extends that prefix to the maximum infinitesimal depth of the owners' bases and performs the checked live gather. Later prefixes are not retried after gathering fails. It searches the supplied catalog rather than creating a new joint real-provider field. none reports failure of this gathering attempt.

The semantic laws require Hex.RealClosure.BaseContext.Catalog.Models: every installed prefix has some Hex.RealClosure.BaseContext.RealPrefix.Model of that exact prefix. This is a mathematical premise, not a runtime model check. Hex.RealClosure.BaseContext.Catalog.Models.empty supplies this law for Hex.RealClosure.BaseContext.Catalog.empty, whose only prefix is rational. Hex.RealClosure.BaseContext.Catalog.Models.insert preserves it when the context of a supplied provider model is successfully installed. Under this premise, Hex.RealClosure.Tower.Live.Request.gatherReconciledFrom?_success proves actual gathering success whenever an installed prefix contains every owner's duplicate-free key list. The selected prefix need not be the particular prefix used to establish that coverage. Thus a modeled catalog does not fail to gather after selecting a compatible prefix. Hex.RealClosure.Tower.Live.Request.gatherReconciledFrom?_history records an installed prefix, a provider model of it and a staged realization, together with the common target, owner and cache model. Hex.RealClosure.Tower.Live.Request.gatherReconciledFrom?_models gives the model-existence conclusion alone. The Hex.RealClosure.Tower.Live.Request.gatherReconciledFrom?_realize law states a prefix/provider history together with an ordinary-real reader and domain for the original and refreshed finite live inventories. Use its returned history and reader together with their accompanying evidence. This is a scoped reader conclusion, not an ordinary-real embedding of the whole infinitesimal field. It also does not supply a recursive exporter for arbitrary serialized tower evidence.

The existing examples are in the library's BaseTests, ReconciledGatherTests and ReconciledBaseTests, and the semantic ReconciledCatalogTests and ReconciledEnlargementTests. Their executable selection, gathering and conditional provider-model theorems exercise different parts of this interface; the success theorem above supplies the general producer guarantee.

39.9.8. Constructing a provider history🔗

When no installed prefix contains the needed provider keys, use Hex.RealClosure.BaseContext.RealPrefix.extend? with a starting prefix, a requested key list and a reader supplying progress at each new predecessor. The constructor skips keys already present. For a new key it calls the reader at the prefix constructed so far, appends that provider and continues there. A missing step returns none; it does not select an unrelated installed history.

Hex.RealClosure.BaseContext.RealPrefix.Ready states that the reader supplies progress along precisely this path, including skips of existing keys. Hex.RealClosure.BaseContext.RealPrefix.extend?_isSome characterizes success by that condition. It does not require progress at every possible registry history.

The two-stage fixture supplies the second packet at the newly constructed first predecessor. The example uses the existing Hex.RealClosure.BaseContext.HistoryTests.construct_two proof:

These packets contain the registered provider's presence and erased sign and approximation progress proofs. They do not by themselves interpret the provider in the reals. The companion's Hex.RealClosure.BaseContext.RealPrefix.Model.Valid requires the caller to prove containment and relative transcendence for each returned step over the interpretation constructed so far. It requires no width bounds: the packet already contains the search progress proofs. Hex.RealClosure.BaseContext.RealPrefix.Model.progress derives a packet from containment, interval widths at most δ for every positive δ, and that relative transcendence. A proof about the new constant over the rationals alone cannot replace its premise over the whole predecessor field.

Starting with a provider model of the seed prefix and those step premises, Hex.RealClosure.BaseContext.RealPrefix.Model.extend?_model proves that the actual returned prefix has a provider model, and Hex.RealClosure.BaseContext.RealPrefix.Model.extend?_embedding preserves its predecessor interpretation. No model of a completed joint target is an input. The existing BaseHistoryTests also cover duplicate-key reuse and rejection of a missing second step. The semantic HexRealClosureTheory.BaseHistoryTests contains install_providers, which derives readiness, validity and a staged realization for its two-stage reader from containment, width and transcendence at the two actual predecessors.

Hex.RealClosure.BaseContext.Catalog.construct? retains the constructed prefix and the returned catalog, which is unchanged if the path is already installed. For live values, Hex.RealClosure.Tower.Live.Request.gatherConstructed? requests their owners' provider keys, constructs that history, extends to their maximum infinitesimal depth and runs the checked reconciliation. Use its returned catalog for subsequent requests. If gathering fails, no construction packet is returned; call Catalog.construct? separately to retain the history regardless of that outcome. The development-only HexRealClosureTheory.ConstructedCatalog provides Hex.RealClosure.Tower.Live.Request.gatherConstructed?_success: starting with a provider model of the seed prefix, path progress, path validity and distinct keys in every owner's signature imply success. Coverage and the depth bound follow from construction; those other conditions are hypotheses.

To reuse the installed-prefix selection laws, retain the catalog model invariant. Hex.RealClosure.BaseContext.Catalog.Construction.models proves it for the returned catalog from the input catalog's Catalog.Models and the caller's path validity.

This route constructs the real-provider prefix before the infinitesimal and algebraic suffixes. Its staged interpretation and all-live gathering do not establish general ordinary-real realization of arbitrary serialized tower evidence or an ordinary-real embedding of the infinitesimal field.

39.9.9. Exact stored data and exploration🔗

Context-bound serialization records the ordered base signature, selected descriptors and recursively encoded coefficients. This is reconstructible data, not a decimal approximation of the selected root.

Hex.RealClosure.Tower.Context.write and Hex.RealClosure.Tower.Context.read use the exact whole-context binding. Hex.RealClosure.Tower.Context.read_write proves the value roundtrip; Hex.RealClosure.Tower.Context.read_stale proves rejection of a different binding. Polynomial read/write has its own roundtrip theorem, Hex.RealClosure.Tower.Context.readPoly_write.

A Hex.RealClosure.Tower.Catalog resolves previously installed context handles before reading values. Unknown algebraic signatures reject; the reader does not manufacture missing progress proofs or roots. Hash lookup still checks the full literal binding. A successful payload roundtrip is separate from mathematical certificate acceptance.

For a checked algebraic root, Hex.RealClosure.Algebraic.RootReplay.readDescriptor_covered restores the same descriptor from its complete subject and encoded evidence. Its hypotheses require the supplied readers to cover only the finite lists Hex.RealClosure.Algebraic.RootReplay.coefficients and Hex.RealClosure.Algebraic.RootReplay.contexts. These include every retained graph entry and moment; their contexts equal the checked subject's context. Partial predecessor readers are allowed, and hashing uses the caller's instances. Hex.RealClosure.Algebraic.RootReplay.readDescriptor_tree takes coverage of Hex.RealClosure.Algebraic.RootReplay.treeCoefficients and Hex.RealClosure.Algebraic.RootReplay.treeContexts instead, so coverage can be proved from the original tree without evaluating hash-table lookups. The byte theorem Hex.RealClosure.Algebraic.RootReplay.decodeDescriptor_covered takes the graph-form inventories and lexical resource checks on the encoded subject and evidence bytes.

For univariate exploration, Hex.RealClosure.Tower.Sample.family orders and deduplicates root handles before constructing sections and open sectors. Sections and rays reuse their root's cached context; a bounded sector collects only its two endpoint roots, and the root-free line stays in the input context. This does not build a shared arithmetic context for the whole family. Hex.RealClosure.Tower.Sample.partition instead collects all boundaries in one native arithmetic context. Samples retain the coefficient inclusion and requested sign order. Zero polynomials contribute no boundary, since their sign is identically zero. The converse, that only zero produces .all, requires the model laws. A diagnostic .all or .eq fallback would lose boundaries or merge distinct ones. Context.collect also has a diagnostic panic fallback to an empty collection, which would lose collected boundaries and invalidate bounded sectors. Use Hex.RealClosure.Tower.Context.collect? to retain failure; Hex.RealClosure.Tower.Context.collect?_success excludes it under the common model laws. The family semantics require the laws excluding each of these fallbacks. Cell membership, coverage and sign constancy belong to the companion's family theorems; a sample data structure alone does not prove these claims. This interface does not provide full CAD or multivariate coverings.

39.9.10. The Mathlib correspondence🔗

Hex.RealClosure.Tower.Model interprets one native context in a field with a linear order, binding zero reflection, arithmetic and sign. The root theorems additionally require ordered-ring laws and real closedness. The TowerRoots development import supplies Model and its constructors. Models are built from lawful base interpretations with Hex.RealClosure.Tower.Model.base and extended at selected roots with Hex.RealClosure.Tower.Model.adjoin. Their hypotheses bind the actual operations and selected embeddings. A model is a mathematical consumer hypothesis, not a runtime root-constructor argument.

Hex.RealClosure.Tower.Context.roots_spec.{u}
  {registry : Hex.RealClosure.BaseContext.Registry}
  {parent : Hex.RealClosure.Tower.Context registry} {K : Type u}
  [Field K] [LinearOrder K] [DecidableEq K] [IsStrictOrderedRing K]
  [IsRealClosed K] (model : Hex.RealClosure.Tower.Model parent K)
  (p : Hex.DensePoly parent.Value)
  {out : List (Hex.RealClosure.Tower.RootEntry parent)}
  (returned : parent.roots p = Hex.RealClosure.Tower.RootSet.finite out)
  (x : K) (label : ℕ) :
  (∃ entry ∈ out, entry.denote model = x ∧ entry.multiplicity = label) ↔
    (HexPolyTheory.Interpret.interpret model.value ⋯ p).IsRoot x ∧
      label =
        Polynomial.rootMultiplicity x
          (HexPolyTheory.Interpret.interpret model.value ⋯ p)
Hex.RealClosure.Tower.Context.roots_spec.{u}
  {registry :
    Hex.RealClosure.BaseContext.Registry}
  {parent :
    Hex.RealClosure.Tower.Context
      registry}
  {K : Type u} [Field K] [LinearOrder K]
  [DecidableEq K] [IsStrictOrderedRing K]
  [IsRealClosed K]
  (model :
    Hex.RealClosure.Tower.Model parent K)
  (p : Hex.DensePoly parent.Value)
  {out :
    List
      (Hex.RealClosure.Tower.RootEntry
        parent)}
  (returned :
    parent.roots p =
      Hex.RealClosure.Tower.RootSet.finite
        out)
  (x : K) (label : ℕ) :
  (∃ entry ∈ out,
      entry.denote model = x ∧
        entry.multiplicity = label) ↔
    (HexPolyTheory.Interpret.interpret
            model.value ⋯ p).IsRoot
        x ∧
      label =
        Polynomial.rootMultiplicity x
          (HexPolyTheory.Interpret.interpret
            model.value ⋯ p)

Hex.RealClosure.Tower.Context.roots_all characterizes the zero polynomial; Hex.RealClosure.Tower.Context.roots?_success proves actual diagnostic success; Hex.RealClosure.Tower.Context.roots_sorted proves strict order of the returned native values. Their common model is essential. It does not give an ordinary-real embedding of an infinitesimal.

This example reuses the downstream tower consumer's composition. Given a nonzero interpreted polynomial, the actual native producer returns a finite strictly sorted list; no successful-output premise is supplied.

For rational input, Hex.RealClosure.Trivial.Rational.roots converts generic roots to the independent real-algebraic carrier, retaining the all-roots case, order and multiplicities. This is an agreement and differential-testing route, not the fastest entry point: generic isolation and canonical conversion have separate costs. Use the real-algebraic backend directly when that conversion is unnecessary.

Ordinary-real tactic proofs belong to the existing real-coefficient rcf adapter and its manual. Its source-expression guards, selected embeddings and accepted-certificate realization remain separate from the root-model hypotheses here. Existing owner Lean tests and conformance cover non-monic definitions, reducible inversion, nested roots, stale evidence and transport. Transport controls include small executable build-time guards. The deep four-level fixture is type-checked; its execution is outside routine CI. Exact Z3/python-flint oracles separately check the emitted arithmetic and root fixtures. Retained tower and clean/eager measurements supply computational evidence; these examples and theorem applications do not replace it.