18.9. Algebraic coefficients🔗

Import HexRCF.RealCoefficients to extend the same rcf command. The original HexRCF import and all its rational examples keep their existing behavior. The adapter is currently available in the development monorepo; it is not in the released hex-rcf package. The optional adapter accepts a selected algebraic coefficient in an otherwise rational polynomial sentence. Its direct notation support covers positive rational square roots and positive rational bases with a reciprocal natural exponent, including Mathlib's (2 : ℝ) ^ (1 / 3 : ℝ). It also accepts the checked Hex values CubeTwo.realAlgebraic and CubeTwo.shifted. For a different coordinate in a chosen number field, write a Selected.field expression with the field element and its checked chosen root, as shown below. In these examples, the power in (2 : ℝ) ^ (1 / 3 : ℝ) defines a closed coefficient; the quantified variable still occurs in an ordinary polynomial. Products with rational constants are supported. Closed division is also supported for the selected and reconstructed Hex inputs and these checked positive-root aliases. The adapter checks every original divisor before solving the target, including divisors erased by cancellation, zero multiplication or an empty domain. Named square/cube aliases keep their existing direct path when all original divisors are rational; algebraic division uses the common field.

Visible RealAlgebraicNumber.ofRat constructors also retain their proved rational value. They use the rational decision path after checked source lowering; mixed expressions may still use the algebraic path. Divisions inside the rational constructor's input remain original guard obligations. A known zero guard reports rcf: original closed divisor is zero, including when zero multiplication or an empty domain would otherwise hide it.

The last example proves the radicand's equality to 2 before identifying its square root with the positive selected root. Square roots of rational constructors with zero or negative values reduce through the rational path; they do not select a positive algebraic root.

Positive rational roots use the same selected-field certificate machinery. For a rational base a and positive natural degree n, the frontend records a.den * X^n - a.num and checks a real-axis isolating square with a strictly positive lower endpoint. The proved root equation and positivity identify that selected root with a ^ (1 / n : ℝ); approximation proposes the square but supplies no proof. The base and exponent may also use inverse notation, and visible rational constructors are lowered in both. Every original denominator in the base, exponent or surrounding expression remains a source guard.

The first example uses the chosen positive square root in a polynomial whose minimum is zero. The third finds a further root over that coefficient field. The last checks the cube root's nonzero divisor before using its power equation. Division by a closed higher-root alias becomes multiplication by its closed inverse before abstraction, so the shared integer reifier receives no parameter denominator. Natural powers of the quantified variable keep their usual polynomial meaning. Nonreciprocal real exponents are outside this alias grammar. Roots with an algebraic base first authenticate that base in its selected field. Frozen polynomial, power and sign evidence then identifies the root with the original expression. For degrees greater than one, this checks the nonnegative branch; negative bases do not receive a signed-root interpretation. Degree one is ordinary identity and also accepts negative algebraic bases.

These examples respectively use a nested root as a coefficient, locate a root of a shifted algebraic base, and retain the original divisor guard inside a root. Cancellation can yield a zero base, but never removes a zero-divisor obligation. The same authentication supports reciprocal natural root degrees such as (3 + Real.sqrt 2) ^ (1 / 3 : ℝ) and further nesting. The ordinary proof checks recorded certificates; it does not repeat the native root or sign searches.

Before common-field search, rcf.algebraic.commonDegree bounds the product of the canonical degrees of distinct selected generators (default 64), reporting exhaustion through the shared exponent dimension. This is a conservative admission bound: aliases for one selected generator count once, but algebraic relations between different generators can make the actual common degree smaller than the product. The admission also applies to a single generator. Algebraic-base roots require the root degree times the degree of the field authenticating their base to fit the same limit. This conservative bound applies before native root production, including when cancellation reduces the base's minimal degree. Repeated uses of exactly the same base share authentication throughout one recursive preparation. These roots require supported selected-field presentations and irreducibility certificates. It does not establish complete witness search or bound every later operation. Authentication follows source order; a terminal failure or exhaustion prevents authentication of later coefficients, even when a later negative base would decline.

The adapter's source preparation applies its coefficient-size limit to intermediate arithmetic in rational-root bases, reciprocal exponents and dyadic endpoints. Cancellation and zero powers do not erase those bounds.

The selected-field constructions below use the real root of X³ − 2. The adapter records an isolating square and verifies its root witness. It reconstructs Hex's Hex.AlgebraicNumber and Hex.RealAlgebraicNumber through the existing canonical constructor. The second coefficient is computed as 1 + a inside Hex.QAdjoin, then converted through Hex.RCF.RealCoefficients.Coefficients.ofField; its selected real value is proved to be 1 + a.toReal. This ofField tactic example uses the specific checked value CubeTwo.shifted. The definitions CubeTwo.realAlgebraic and CubeTwo.shifted contain these constructions, and the following aliases show their types and use. The second construction below takes a checked selected root directly, computes (a² + 1) / 2 with ordinary Hex.QAdjoin arithmetic, and uses Hex.RCF.RealCoefficients.Selected.field to retain the same root when converting back to a real algebraic number. These examples set maxRecDepth to 2048 and maxHeartbeats to 1000000 so Lean can elaborate their literal certificates; users may need the same options for similar goals.

The same checked construction works for a different cubic, X³ − X − 1. The square below selects its positive real root. The Hex.RCF.RealCoefficients.Selected.real_rootNear theorem identifies that root with the ordinary Hex.ZPoly.rootNear value at the real projection of the square's centre. The tactic can use the selected root when it is named by a def in the same file. It also accepts the existing checked Hex.AlgebraicNumber.ofNormalized constructor directly, followed by Hex.RealAlgebraicNumber.ofAlgebraic with a reality proof. The original isolation square authenticates the chosen root. Elaboration executes canonicalization. Before common-field search, the adapter checks a direct root witness on the original square. The kernel authenticates its literal square and polynomial identities rather than replaying canonicalization. Both identities must reduce in the kernel, including across imports. A transported certificate without a direct witness is currently rejected. The example below computes α² − 1 in the field of the selected root of X³ − X − 1 and uses its proved real conversion. The constructor data must be executable and visible to the frontend; an arbitrary opaque algebraic value has no implicit reconstruction rule.

Field signs first try exact rational Horner bounds on the authenticated generator interval. A strictly separated bound proves its sign; exactly [0,0] proves zero. Other zero-containing bounds retain a full rational Sturm query. Replay checks the recorded branch, and never rescues malformed query evidence with interval evaluation. The complete algebraic producer still succeeds on its proved input surface. Indexed sign retrieval below reduces fresh-module build time on the recorded examples.

A four-round matched comparison on the further-root, reciprocal-root and cubic examples used raw carriers and favored interval quotation in all twelve pairs, with median paired margins 4.513, 4.752 and 13.553 seconds. The reference reconstructs full queries after interval production, so this measures quotation-mode selection, not a speedup against older code or isolated kernel time. Shared-host variation and all completed samples are retained in reports/hexrcf-interval-proofs.md. Those probes now pin raw carriers explicitly; the pin was added after the measurement. The default is rcf.algebraic.intervalSigns=true; the false arm remains a comparison control. Direct coordinate quotation remains off by default: its two separate comparisons did not establish a gain. The comparison control changes evidence from the tactic producers. Quotation and replay of a supplied frozen table, including the explicit prepared replay API, preserve its entries regardless of this option.

rcf.algebraic.singleReplay is also false by default. It compares one Boolean certificate replay goal with separately checked conjuncts; source authentication and the final proof check remain separate. A four-round comparison of the same three examples used raw carriers and did not establish a speedup. The probes now explicitly pin that mode; the pin was added after the retained measurement. Combined replay produced smaller private proof files but used more peak memory. The report and retained samples record every completed arm and the exact source and import identities.

rcf.algebraic.monicCore is true by default. It normalizes the proposed carrier core while retaining the original polynomial product and checking both radical identities. Signed Sturm chains keep their existing positive scaling. All twelve pairs in a four-round comparison favored this mode on the same three examples, with lower peak memory. The report and retained samples describe these full-build observations. Successful proposals have checked soundness and a proved monic core. Radical proposal progress and interpreted squarefreeness are proved at the actual selected field embedding, using zero-reflecting coefficient semantics that preserve arithmetic and inversion. These are radical laws; bounded isolation can still exhaust. The complete library producer retains raw cores and its existing progress laws. Direct produceWithin calls also retain their raw default; the tactic passes its monic option explicitly. The false mode retains raw cores as a comparison control. This normalization does not remove the common-field authentication limitation.

rcf.algebraic.indexSigns is true by default. It retrieves field signs through a frozen tree of positions in the original checked evidence table. Every hit checks its array bounds and exact key. A missing route uses the original table lookup, so malformed routing cannot lose a recorded sign; an absent original entry still fails preflight. The kernel checks the same sign evidence and uses a proved checker equivalence before the existing soundness theorem. It does not sort keys during replay. Two separate four-round comparisons favored indexed lookup in every pair on the further-root, reciprocal and cubic examples. The preserved-hit mode's median paired reductions were 3.774, 3.493 and 3.527 seconds, with lower peak memory and larger private proof files. These are full fresh-module costs, not isolated lookup timing or an asymptotic claim. The report and retained samples include every completed arm and their source identities. The false mode keeps linear retrieval; older comparison probes explicitly pin that mode.

rcf.algebraic.signRefinements is zero by default. Setting it to a positive natural number bounds producer attempts to tighten the generator interval when Horner signs are inconclusive. The certificate retains the original generator and checks that the tighter count-one interval selects the same real root. Replay checks frozen data and never runs refinement. Inconclusive signs keep full query evidence; invalid proposed evidence is terminal. The retained comparison found no useful whole-module speedup at a four-step budget, even though the lower-precision fixed-field case removed full queries. This mode therefore remains optional. The entire bounded refinement loop is one native call: cancellation is checked before and after it, not between its steps. A large chosen budget can therefore delay interruption.

A separate initial-precision comparison proves the same fixed-field sentence at eight and sixty-four generator bits, using a checked selected-root equivalence for transport. The full sign queries fall from three to zero, and the private proof file shrinks by 6,456 bytes. Four retained rounds give median fresh-module times of 12.689 and 12.556 seconds; the paired median change is −0.169 seconds, with one slower candidate. Arm-specific constructor checks and the candidate transport are prebuilt, so their initial elaboration is excluded. This does not measure the total cost of changing precision or general field reconstruction, and does not justify a default precision change.

The four-width study with constructor and transport included checks eight, sixteen, thirty-two and sixty-four initial bits through the actual tactic proof-acceptance routine. All 36 fresh-module arms retain their output and standard-axiom audit. The variable paired observations justify no default change. Each timed module proves its own generator validity and selected-root equivalence; common imported laws and the original target are prebuilt. This fixed-field experiment does not implement arbitrary field reconstruction or nested transport.

The source repeated/shared-root comparison uses actual rcf goals with a squared zero polynomial and an additional polynomial sharing existing roots. All three checked carriers have four root sections and five sectors. Sixteen retained arms include the named-√2 frontend preparation, quotation and kernel acceptance; paired medians increase by 0.890 and 1.266 seconds for these changed inputs, retaining a −8.198-second repeated-input observation as well. Several input dimensions change together, so this is not a one-parameter complexity model or a general scaling claim.

For these reconstructed inputs, closed arithmetic is compiled into the common field after authenticating its source values. A quotient is recorded as a rational coordinate polynomial and checked by its multiplication identity; kernel replay does not repeat inverse search. When all source coordinates use one selected generator, the adapter retains that generator and its existing power basis; it does not run general common-field search. Polynomial and isolation-square checks still authenticate every proposed source coordinate. If the common defining polynomial exactly matches an authenticated source's polynomial, quotation reuses its supplied CheckedIrreducible proof. The kernel proves equality of the original and literal polynomials and transports the source instance along that equality; runtime equality alone is insufficient. This supports source proofs beyond the frontend's single-witness and quadratic-norm search languages, including a checked real quartic with a multi-prime certificate. The fresh goal proofs use ordinary imports, including certificate construction and replay through the owner's public API.

For a new common polynomial, the frontend first checks for an existing CheckedIrreducible instance for its exact quoted DensePoly.ofCoeffs literal. It binds that literal to the runtime polynomial and checks the supplied proof's type, axiom dependencies and ordinary-kernel validity. A rejected proof or an instance-search resource failure is terminal. If no certificate language succeeds, the diagnostic prints the exact instance target. An instance written using DensePoly.ofList need not match instance search's transparency.

The degree-eight regression uses one previously proved instance for the compositum of the selected quartic and √2, enabled with open scoped Hex.RCF.SuppliedIrreducible; its kernel irreducibility check reuses that theorem. Common-field construction still runs the normal native algorithm during search.

The matched construction-cost report compares rebuilding this proof with importing it for the same degree-eight goal and private executable imports; it records shared-host running times and memory, without a general scaling or automatic-certification claim.

Without such an instance, the frontend tries quadratic-norm and free witness certificates, then the owner's multi-prime certificate producer and ordinary-kernel quotation. These certificate languages do not cover every irreducible common defining polynomial. Increasing a search bound need not resolve a refusal, and their failure does not imply reducibility. The cubic example below verifies x / α = (α² − 1) * x at the selected positive root of X³ − X − 1. The same example also uses the ordinary QAdjoin.toAlgebraicNumber conversion followed by a reality proof, without the Coefficients.ofField wrapper. Both forms preserve the selected embedding.

The two-square-root examples below combine Real.sqrt 2 and Real.sqrt 3 in one common field and check that each field coordinate names the intended positive root. This path accepts positive rational radicands as well as natural literals, and also accepts the positive rational-root aliases above. A lone Real.sqrt 2 whose original divisors are all rational uses the earlier single-coefficient path; other positive natural square roots use the common-field frontend, including perfect-square radicands. Algebraic divisors contribute generators even when their quotients cancel, so they can increase the common-field degree. The two-root examples use a larger heartbeat limit for the quartic common field. The retained measurements below do not measure that degree increase. The next examples mix Mathlib's Real.sqrt 2 with a Hex root selected from X² − 3. They also use the ordinary QAdjoin element 1 + √3, converted back to a real algebraic number. rcf checks each proposed common-field coordinate against the original selected root before proving the sentence. For multiple sources, the tactic checks a defining polynomial and selected real root for the common field, then verifies that every original coefficient has the proposed value there. The higher-degree example below combines the selected real root of X³ − 2 with Real.sqrt 2. Some larger combinations still decline with an irreducibility-witness diagnostic: the current certificate search does not cover every polynomial that can define a common field.

The existential statements have no witness supplied by the user. For the selected cubic coefficient, rcf isolates a root of x² − selectedCubic over its fixed real number field and checks both inequalities at that same root in the interval example. The fail_if_success examples show that a false algebraic statement produces no proof, nonpolynomial syntax in the quantified variable is rejected, and a cancelled zero divisor remains an invalid input. CubeTwo.realAlgebraic exposes its checked selected-root construction, so its lone examples use the selected-root frontend. Earlier cubic measurements record their stated source revision and do not measure this routing change. The adapter's source reifier preserves explicit coefficient aliases and original divisor obligations before normalization. Closed values built with Selected.real may be named using def in the same file. Across modules, use abbrev or @[expose] def so the defining expression remains visible. For supported sentences, a divisor must be proved nonzero before certificate construction.

The next construction selects the positive root near 1.675 of X³ − 4X + 2. Combining it with √37 creates a degree-six common defining polynomial. The frontend's single-witness and quadratic-norm producers decline that new polynomial; the public multi-prime certificate route authenticates it before the goal's root and sign checks.

The algebraic examples use the proved generic accepted-query soundness theorem HexRealRootsTheory.Tarski.check_rootSum. Their fixed-field certificate checks and chosen-root identifications use only Lean's standard logical axioms. See HexNumberField and HexRealAlgebraic for the underlying number APIs.

Visible checked conversions preserve the actual option branch. RealAlgebraicNumber.ofAlgebraic? succeeds for a selected real or rational value, or an element of QAdjoin a.toAlgebraic for a real algebraic generator a. When applied to AlgebraicNumber.I, it returns none, so getD denotes its stated fallback. An explicit .re projection instead denotes the real part; the real part of I is zero.

The frontend also lowers visible real-algebraic arithmetic, inverses, natural powers and integer casts using the number library's interpretation theorems. Supported projections include selected real values, rational values, real QAdjoin coordinates and sums of supported projections. This recognition does not provide a general procedure for arbitrary complex expressions or opaque conversion code. Original rational, real-algebraic and supported real-field divisors remain obligations, including divisors inside an unused getD fallback, before any branch is simplified. Division over other carriers, raw PolyQuot.div/inv, integer powers and divisions depending on a binder inside conversions are rejected.

A fresh-module comparison of the cubic reciprocal uses identical imports and shared source setup for Coefficients.ofField and direct QAdjoin.toAlgebraicNumber conversion. At source b10ded789, Lean v4.35.0-rc3 on shared chungus2 CPU 18, four adjacent alternating AB/BA rounds give median build times 10.441 and 10.443 seconds respectively, with median peak RSS 3.29 GiB in both arms. The median paired direct-minus-wrapped margin is +0.013 seconds; margins range from −0.045 to +0.071 seconds and do not resolve a cost difference. Both private olean files contain 603,000 bytes. These are fresh-module lake build wall times, including Lake startup and replay, for one identity whose specialized equality atom is zero. There is no import-only arm or root-search scaling claim. The report and retained samples record all eight arms and host activity, and retain the separate b0c583792 snapshot. Each measurement is tied to its recorded source; later routing and environment cleanup are outside those measurements. They do not isolate the cost of checking separate source and target sign tables or establish general extension performance or total algebraic search.

A separate fixed-field input report retains 24 matched-import builds varying variable degree, atom count and integer coefficient width independently. These root-free carriers do not measure precision or nested depth. A representative two-field further-root proof, ∃ x : ℝ, x² = Real.sqrt 2 ∧ 1 < x ∧ x < Real.sqrt 3, takes 43.672 seconds at its recorded source on leased CPU 14, including build and profiler overhead. That source used full Sturm-query quotation and predates interval signs; this profile does not attribute the cost of the current default. Its exclusive kernel type-checking category totals 30.1 seconds; the smaller literal-replay category excludes those child checks. The report retains source identities, memory, serialized sizes, unique syntax and expanded-reference counts. It does not claim a complexity law or complete Phase-4 attestation.