18.14. Ordinary samples over a selected field🔗

The native tower API can find roots and choose ordinary real samples over an already selected algebraic coefficient field. Start with a checked Hex.SignDet.Descriptor; its polynomial, interval and derivative signs fix the selected root. Hex.RealClosure.Tower.Model.base interprets the rational base, and Hex.RealClosure.Tower.Model.adjoin preserves that selection in the child field. This real interpretation is used in correctness proofs; compiled arithmetic uses the owner's native stored values.

Hex.RCF.RealCoefficients.RepresentationSpecialize.prepare substitutes those values into the shared formula syntax using their actual arithmetic. It groups terms by the bound-variable exponent after evaluating coefficient coordinates directly. Its Hex.RCF.RealCoefficients.RepresentationSpecialize.prepare_eval law needs arithmetic preservation and zero reflection; Hex.RCF.RealCoefficients.RepresentationSpecialize.prepare_degrees needs zero reflection alone. These permit unequal stored nonzero expressions with the same real value. They retain repeated atoms, cancelled zero polynomials and the two atoms describing a half-open domain. No field instance on native stored expressions is required.

For example, the following API input describes X² = α in (1, 2], with α the fixed selected generator. The repeated square has the same roots.

Hex.RealClosure.Tower.Sample.family takes the specialized polynomial list. Hex.RealClosure.Tower.Sample.Family.cells_unique places every real point in exactly one section or sector, and Hex.RealClosure.Tower.Sample.Family.cell_signs gives every polynomial's sign at that same point. Each sector has an ordinary sample in its own compatible context; Hex.RealClosure.Tower.Sample.Family.sector_signs proves the entire sign vector throughout that sector. Here is the direct same-point conclusion for any family interpreted in ℝ:

Root sections use their selected boundary as the real witness. Hex.RealClosure.Tower.Sample.Family.sections_correct checks all signs at that boundary, with the original coefficient interpretation fixed:

The native root producer already provides complete coverage, multiplicities and order through Hex.RealClosure.Tower.Context.roots_spec and Hex.RealClosure.Tower.Context.roots_sorted. For the positive selected √2 fixture, the four source atoms above have four distinct boundaries, four sections and five sectors; the repeated polynomial adds no extra boundary. The negative selected √2 control has only the two guard boundaries and rejects the root equation everywhere. A separate mixed-input control sends a literally duplicated atom, a zero atom and a leading-cancelled polynomial through the native root/sample producer. The cancelled polynomial adds a section at zero. Every cell sign and the strict/non-strict domain relations are checked through the shared Boolean fold. Another control uses the selected root of (X² − 2)(X − 3) in (1, 2). Its distinct stored expressions α and α³/2 have zero difference; their leading-term cancellation still produces the correct degree and every cell sign.

Hex.RCF.RealCoefficients.Samples.run connects this native family to the shared Boolean formula and its one real quantifier. It prepares the atom list once, evaluates a complete sign row for each section or sector, and uses the existing strict quantifier fold. The result is some true or some false under an actual ordinary-real predecessor model. False is a diagnostic result. Hex.RCF.RealCoefficients.Samples.run_spec proves exactly the shared Hex.RealFormula.Prenex.toProp meaning at the fixed coefficient values:

All coefficient coordinates belong to one native parent context, and they may be different values there. Independently constructed fields require proved conversion into that common context first. The Hex.RCF.RealCoefficients.Samples.section_formula and Hex.RCF.RealCoefficients.Samples.sector_formula laws interpret the whole Boolean formula at the same selected boundary or ordinary sector point; Hex.RCF.RealCoefficients.Samples.cell_formula applies throughout the cell. These compose actual root coverage, cell membership and sign laws, without adding them as unproved assumptions.

The compiled regressions distinguish positive and negative selected √2 in ∀ x, x² + α > 0, and swap two distinct coefficient coordinates to check that their order changes the answer. They retain repeated/common roots, zero and cancelled atoms, all six comparisons and Boolean operations, and equal, reversed and half-open domains. Fresh modules check the public semantics and its standard axiom inventory. These are correctness regressions; no timing improvement is claimed for this composition.

For an existing Hex.RealAlgebraicNumber, Hex.RCF.RealCoefficients.NumberField.run constructs the native parent context with the owner's checked number-field factory. Its inputs are the original Hex.QAdjoin coordinates. The factory retains the generator's minimal polynomial and selected real embedding; packing preserves that embedding. Hex.RCF.RealCoefficients.NumberField.value_eq_ofField identifies the native interpretation with the frontend's existing Hex.RCF.RealCoefficients.Coefficients.ofField conversion. The following public law covers every shared one-quantifier formula at those converted original real values:

The compiled API regressions select both roots of X² − 2 and the positive root of X³ − 2, then find further roots of x² − α over each original number field. They test the complete conjunction with the squared atom (x² − α)² ≥ 0, whose repeated roots are shared with x² − α, and the half-open guards 1 < x and x ≤ 2. Positive √2 and the cube root return true; negative √2 returns false. Further controls select all three roots of the totally real cubic X³ − 3X + 1, a non-monic quadratic and a rational generator. They compute the irrational coordinate α² − α in both conjugates of X² − 2, swap the coordinate order, and compare a degree-two coordinate with its negative in the cubic field. They cancel a leading term and retain zero atoms and exact endpoint, equal and reversed domains. All six comparisons and both quantifiers are exercised. The public correctness, totality and truth laws have only the standard three axioms. These compiled controls are diagnostic examples; they do not supply frozen certificates or quoted source proofs. This API performs root production and does not complete generic replay or frontend authentication for that backend. No timing improvement is claimed.

All coordinates supplied to this entry point belong to the same original number field. Each run call constructs its presentation anew. Hex.RCF.RealCoefficients.NumberField.runWith reuses one checked presentation across formulas; its Hex.RCF.RealCoefficients.NumberField.runWith_spec law preserves the original selected coordinate values directly. A compiled control evaluates both quantifiers over the same retained presentation.

Independently constructed contexts use checked maps that retain each original owner in input order; repeated owners can reuse the same cached predecessor. Hex.RCF.RealCoefficients.Gather.values applies those maps to the ordered coefficient coordinates. The explicit Hex.RealClosure.Tower.Shared.gather? operation accepts a caller-selected target. The following automatic entrypoint selects an installed target from the catalog before applying the same maps. No new quotient-field representation or field instance on stored expressions is introduced.

The following computation constructs √2 and √3 independently, gathers them, and checks ∃ x, x² = √2 ∧ 1 < x ∧ x < √3. Its variable roots are therefore computed over the already gathered algebraic coefficient field. The catalog contains its validated rational prefix; the automatic entrypoint selects the shared base and gathers every original owner without a caller-selected target.

Hex.RCF.RealCoefficients.Gather.prepare_eval proves the meaning of every original atom after transport. Hex.RCF.RealCoefficients.Gather.run_spec relates native production to the shared quantified formula in the original owner order. Hex.RCF.RealCoefficients.Gather.gather_subsequence proves actual gathering and decision production when each owner's registered keys form an ordered subsequence of the supplied target's keys and its infinitesimal depth does not exceed the target's. Thus an owner over [β] can enter a target over [α, β], retaining the same provider identity and version. Reordered or stale keys do not satisfy this condition. The operation needs a provider realization of the target and a real model of its base; it does not construct a new registered base for incompatible owners or infer independence of named constants. Hex.RCF.RealCoefficients.Gather.gather_spec retains the prefix-compatible API. For supplied source models, Hex.RCF.RealCoefficients.Gather.run_original requires their actual factory equations at the target realization. These equations bind their values to the common model; key compatibility alone does not identify an independently registered interpretation. Their complete theorem axiom inventories use only the standard three axioms. These laws do not treat the computed Boolean above as a proof of a source goal. The compiled controls also distinguish the two selected roots of X² − 2, reverse coefficient order, retain a repeated owner, and check zero and leading-term cancellation. Empty collections retain the rational case.

Gather.runFrom? tries the rational prefix first, then installed prefixes from newest to oldest, and retains coefficient order. Gather.gather_catalog proves gathering and native decision production from authenticated models of admissible prefixes and compatible original bases of depth zero. It infers no relative transcendence or global real model of symbolic infinitesimals. Gather.runFrom?_original preserves supplied owner-model values when each model is exactly the result of its factory at the selected target realization. These equations are explicit premises; the theorem does not identify an independently registered model from compatible keys alone. An absent joint prefix yields no verdict. Controls cover conjugates, repeated owners, cancellation, empty coefficients, actual one-provider version refusal and rational-first selection. Parameterized [β] to [α, β] instances use the provider-induced owner interpretation; they do not identify it with the independent source model. Correctness/refusal laws have exact complete standard-axiom audits.

Gather.runReconciled? also accepts checked provider-key permutations through the owner's reconciled catalog. It retains the original coordinate order and returns no verdict when a joint prefix is absent or a version is stale. Gather.gather_reconciled derives gathering and an ordinary-real native decision from actual models of the installed prefixes. All original bases have depth zero; the reconstructed owner models come from the selected joint history. Separate registrations do not supply a joint-transcendence premise. Gather.gather_history also retains the selected provider, catalog membership and exact realization/reference-model identities.

The catalog regression reversed contrasts the two routes on an arbitrary algebraic suffix: [α, β] entering [β, α] is rejected by the ordered route and admitted by the reconciled route. It is conditional on a supplied joint provider model; this tranche constructs no two-key model. Actual one-provider controls take the ordered fast path and execute true and false paired-root sentences, stale-version refusal and rational-first empty selection. Literal two-key controls check the reconciled metadata predicate and literal ordered sublist rejection, including duplicates.

Gather.runReconciled?_original preserves separately authenticated original values when their models equal the reconciled factory results. Those equations remain explicit; keys alone do not authenticate a source expression. Neither route quotes frozen evidence or collects every original divisor guard. A positive infinitesimal depth does not supply a faithful global model into ordinary reals.

InverseReplay.check reads a supplied closed-coefficient inverse equation from a checked memo. It preflights every supplied original divisor and the requested operand before reading that equation. A zero divisor returns the structured divisor error; missing or mismatched equation evidence returns the evidence error. Neither case starts another solver. The caller still authenticates the source expressions and retains the complete original guard list, including guards removed by cancellation.

The reader checks the operand and product-minus-one signs at the same selected root. Its output need not be the native gcd algorithm's literal representative. Under an authenticated ordinary-real predecessor model, check_source identifies the output with the inverse of the exact source coefficient and proves that source nonzero. check_domains proves every supplied guard nonzero at that same selected root. These are coefficient-source laws, not a complete tactic certificate or a replacement for the native arithmetic dictionary's stronger equality.

The frozen inverse regression checks a supplied packing whose original polynomial contains an additional copy of the defining polynomial, reads its inverse equation and identifies its value with (Real.sqrt 2)⁻¹. A Mathlib-free producer generates the literal scalar, packing and inverse graphs; the ordinary kernel checks the stored data independently. The source and domain proofs use only the standard three axioms. Zero guards take precedence over absent evidence; empty and out-of-range memos return the evidence error. A changed operand is refused even with an otherwise valid memo; a zero original guard is refused alongside valid evidence. Acceptance is checked with kernel diagnostics rejecting native root/sign production. This finite example supplies no recursive reached-data exporter.

For an ordered nonempty list of coefficients from one authenticated real prefix, Gather.run_registered_many derives the selected target and the identity-factory equations and preserves each source index. Every coordinate belongs to that prefix's base-field context. Gather.run_registered is the singleton case. Empty owners retain the existing rational-first selection. The prefix must be the only inserted nonrational entry; successful insertion already excludes the empty rational key path. The returned decision retains each coefficient's value in the caller's own RealPrefix.Model. That model already carries the actual provider interpretations and relative-transcendence/progress laws; a bounded rcf_constant registration alone does not supply it.

The registered conformance module provides guarded_root, which is a producer law using the sentence adapter's RealFormula.guard atoms for (0, 2]; one ordinary real square root satisfies the equation and both guards. The (2, 3] producer law returns false because both roots are excluded. Separate guard checks exclude the lower endpoint and include the upper endpoint, with executable rational checks covering a fractional lower bound. These do not exercise the real-coefficient source reifier's Set.Ioc lowering.

The same module proves production laws for the ordered pair (L, L⁻¹), where L = liouvilleNumber 2: the shared equations x² = L and x² L⁻¹ = 1 have a root above 1, whereas exchanging the coordinates makes the sentence false. A standalone repeated-root polynomial retains the same guarded roots; its square cannot be negative. Catalog controls also execute these paired and repeated-root searches. These are native producer laws and compiled controls, not quoted frozen evidence.

Samples.run performs production, including root finding. Its Boolean output is not frozen certificate evidence. Turning it into a source-goal tactic proof still requires checked literal context/root/sign data, exact source coefficient identities and every original divisor guard. Its real-model hypothesis does not supply a global real interpretation of symbolic infinitesimals or discharge their required finite joint realization.

The owner already provides a native finite-sign realization law in HexRealClosureTheory.NativeRealization. Context.realize_values takes the actual provider history at the context's stored origin and one finite list of values. It supplies one ordinary reader preserving all requested signs together, arithmetic on its closed domain, and inherited fixed real coefficients. This applies through the stored nested root suffix and successive native infinitesimals. Its partial domain does not assert a field embedding of symbolic infinitesimals into ℝ.

This direct API example realizes both operands, their sum and their product with the same reader: