18.12. Signs and selected roots with BKR🔗

The underlying sign-determination library can answer a more detailed question than whether a sentence is true: at the roots of x² − 1, which sign patterns of x and x − 1 occur, and how many times? The checked table below has one root with signs (−,−) and one with (+,0). Every omitted pattern has count zero. The query order is the order of the two supplied polynomials.

Hex.SignDet.determine returns none exactly when the defining polynomial and interval do not form a valid root domain. An interval with no roots returns an empty table. With no queries, the count at the empty sign pattern is the number of roots. To reuse a prepared polynomial and interval, call Hex.SignDet.determinePrepared directly.

The success and correctness theorems are in HexSignDetTheory.TableProducer. Hex.SignDet.determinePrepared_success proves that the actual prepared BKR producer always supplies a checked table under the coefficient-interpretation laws. Hex.SignDet.determine_correct identifies every returned count with the number of mathematical roots having that sign pattern, including zero for omitted patterns. Both the producer-success and count-correctness results use the shared proved root-sum theorem.

Derivative signs identify a selected root. Here the positive root of x² − 1 is selected by the sign of the first derivative. A second checked table gives the signs of three other polynomials at that root: x, x − 1, and x² − 2 have signs +, 0, and − respectively. The descriptor records the defining polynomial, interval and context as well as the derivative sign.

The same operation works over a real number field. Let α be the positive cube root of 2 constructed above, and work in ℚ(α) using ordinary Hex.QAdjoin arithmetic. The polynomial (x − α)(x + α) has two real roots; the positive first-derivative sign selects α. At that root, x − 1, x − 2 and x³ − 2 have signs +, − and 0. Repeating the first query repeats its sign in the same position. An empty query list returns an empty sign vector.

Import HexSignDetTheory.SelectedProducer for the success and correctness theorems. Hex.SignDet.Descriptor.buildSigns_success proves that buildSigns always succeeds for a validated descriptor when coefficient arithmetic and signs have their specified mathematical meaning. It proves preparation and table construction succeed and rules out every final internal error; successful output is not a hypothesis. Hex.SignDet.Descriptor.buildSigns_roots also proves that the returned list gives the signs at the original selected root, in query order. These proofs use the shared root-sum theorem HexRealRootsTheory.Tarski.check_rootSum.

For one polynomial, a validated descriptor provides an ordinary integer sign. The same cubic-field example can use this operation directly, receiving only the integer sign from the checked calculation:

Hex.SignDet.Descriptor.signAt_success proves that the underlying checked calculation succeeds, so its diagnostic zero fallback is unreachable when the coefficient operations satisfy their interpretation laws. Hex.SignDet.Descriptor.signAt_correct identifies the returned integer with the evaluation sign at the descriptor's original selected root. Both results use the same shared root-sum theorem. For several queries, buildSigns shares one table across the list; each signAt call constructs its own table.

Completing a partial derivative description supplies every derivative sign without changing the selected root. Over the same cubic coefficient field, P = (x − α)x(x + α) has roots −α, 0 and α. Its second derivative is 6x, so its positive sign selects α. Completion returns the signs of P′, P″ and P‴, all positive at α, in that order.

Import HexSignDetTheory.CompletionProducer for Hex.SignDet.Descriptor.buildCompletion_success and Hex.SignDet.Descriptor.complete_correct. They prove that completion succeeds for every validated partial description and retains its original mathematical root, head, interval and context. This includes an empty partial word when the interval contains exactly one root. The proofs use the shared proved root-sum theorem. They do not require the separate Thom ordering theorem. Each call computes and checks its full derivative table; use buildCompletion directly when you need the evidence as well as the completed descriptor.

For successive queries at one selected root, retain its prepared domain with Hex.SignDet.Descriptor.prepareQueries. This avoids the initial preparation call on each query list. Table construction and selected-sign validation still replay the domain evidence and joint table; the handle carries no measured speedup guarantee. Over the same cubic coefficient field:

Hex.SignDet.Descriptor.prepareQueries_success proves that preparation succeeds for validated descriptions under the coefficient laws. Hex.SignDet.QueryHandle.buildSigns_roots and Hex.SignDet.QueryHandle.signAt_correct identify all returned signs at the original selected root. These results use the shared proved root-sum theorem. The handle retains the original context, polynomial, interval and derivative selection; copied certificates must still pass the ordinary literal replay checks.

Re-encoding asks whether the same selected root can be described using a new defining polynomial and interval. It returns none if the target domain is invalid or excludes that root. Sharing a different root is insufficient: the source below selects +α from (x − α)(x + α), while the target x + α has only −α. Restricting the original head to (−2, 0) also excludes +α. Both calls return ordinary absence, with no internal error.

Import HexSignDetTheory.ReencodingProducer for Hex.SignDet.Descriptor.buildReencoding_absent. It proves this result for every lawful coefficient interpretation when the selected root is absent from the target domain. Preparation and joint table construction are proved from the input; successful output is not assumed. The proof uses the shared proved root-sum theorem. It needs neither a root-separating interval nor a Thom ordering theorem. Import HexSignDetTheory.ThomReencoding for Hex.SignDet.Descriptor.buildReencoding_success, which proves actual success for any valid target polynomial and interval containing the source root. It uses Tau Ceti Thom injectivity to establish a count-one target word; neither equality of defining polynomials nor a smaller interval is required. For an accepted re-encoding, Hex.SignDet.Reencoding.root_eq_source proves that the new descriptor retains the source root.

Refining the interval can retain the root instead. Here (1, 3/2) contains +α and excludes −α. The producer constructs a complete derivative word and fresh evidence for those bounds. Evidence from the original whole-line description is rejected at the refined interval.

Hex.SignDet.Descriptor.buildReencoding_refinement proves success and preservation of the selected root for a valid smaller root domain of the same polynomial containing that root. Its hypotheses describe the input interval; they do not assume a successful computation. The proof uses the old validated selection's uniqueness and the proved shared Sturm–Tarski theorem. It applies to generic lawful coefficients, including non-Archimedean interpretations, without assuming rational isolating bounds. Hex.SignDet.Descriptor.buildReencoding_congr also covers different stored coefficients representing the same polynomial, tested by a zero difference; the producer builds fresh evidence bound to the new representation. The general Hex.SignDet.Descriptor.buildReencoding_success theorem also covers changing the mathematical defining polynomial and enlarging the interval. A different head can include additional roots. Here the source selects +α in (0, 2) with an empty partial word. The target (x − α)(x + 1) on the whole line also contains −1, which was neither a root of the source head nor in its interval. Re-encoding retains +α and builds fresh evidence for the target.

A coefficient conversion lets a selected root participate in queries over a larger coefficient field. Here the source selects √2 over the rationals. Moving its descriptor into the existing field ℚ(∛2) allows a query comparing it with ∛2:

Hex.SignDet.Descriptor.convert maps the head and endpoints, retains the partial derivative selection and builds fresh evidence in the new context. It reconstructs every derivative query using the target's ordinary operations. A context identifier here stands for the caller's immutable context data; changing its binding requires fresh evidence even when all polynomial values stay the same. No old certificate is copied by this operation.

Hex.SignDet.Descriptor.convert_success and Hex.SignDet.Descriptor.convert_root prove success and preservation of the selected root when both coefficient interpretations are lawful and the conversion preserves their values. They cover noninjective representations and assume no Archimedean property or rational isolating intervals. Applying them to infinitesimal coefficients requires a lawful interpretation into a real closed field. The nested-infinitesimal fixture tests execution and context changes; it does not provide that interpretation. These semantic proofs use the proved shared Sturm–Tarski theorem. An arbitrary converter still has the builder's ordinary input and internal-error diagnostics.

Root enumeration constructs a full derivative description for each root. This example uses the same actual cubic coefficient field and enumerates the roots of P = (x − α)x(x + α). The returned words correspond to −α, 0 and α:

Hex.SignDet.Descriptor.buildRoots_coverage proves that every successful output covers every mathematical root in the interval exactly once. On valid domains with no roots, Hex.SignDet.Descriptor.buildRoots_empty proves the actual constructor succeeds with an empty list; Hex.SignDet.Descriptor.buildRoots_constant_success covers nonzero constant heads. Hex.SignDet.Descriptor.buildRoots_subsingleton proves success on every valid domain containing at most one root, including linear heads and isolating intervals, without a Thom-order assumption. Hex.SignDet.Descriptor.buildRoots_none_iff characterizes invalid domains exactly without using the root-sum theorem. The success and coverage results use the shared proved root-sum theorem. Import HexSignDetTheory.ThomRoots for Hex.SignDet.Descriptor.buildRoots_success, which proves actual success on every valid domain. Hex.SignDet.Descriptor.buildRoots_roots proves that the returned list contains every root exactly once, in strictly increasing mathematical order. These generic theorems include finite/infinite bounds, noninjective coefficient storage and non-Archimedean fields.

Infinitesimal coefficients can arise inside the decision procedure. Here ε is positive and smaller than every positive rational. The roots 0 and ε have no rational separator. Root enumeration uses their derivative signs to order them, and the selected-root API distinguishes their polynomial signs exactly.

Two roots can be compared even if their defining polynomials differ. The comparison constructs a checked common squarefree polynomial and expresses both root selections in it. This example finds 1 < 2.

The common-root case needs the shared factor removed before constructing the squarefree comparison polynomial. The two descriptors below select the same positive root of x² − 2, despite their different defining polynomials.

The same defining polynomial can name one root through different intervals. Both (0,2) and (1,2) contain only the positive root of x² − 2. The comparison completes these two descriptions and returns equality directly. It checks that construction succeeded before inspecting the total result.

Hex.SignDet.Descriptor.compare is the total root-order operation. It completes partial descriptors and compares their encodings directly when the stored defining polynomials agree, even across different intervals. For different heads it retains the original root selections when changing their defining polynomial. Import HexSignDetTheory.ComparisonProducer for Hex.SignDet.Descriptor.compare_correct and the equality and strict-order equivalences Hex.SignDet.Descriptor.compare_eq_iff, Hex.SignDet.Descriptor.compare_lt_iff and Hex.SignDet.Descriptor.compare_gt_iff. Hex.SignDet.Descriptor.buildComparison_success proves that the actual common-polynomial constructor, both joint re-encodings and the full-word comparison succeed under lawful coefficient interpretations. The total operation's internal error branch emits a diagnostic and returns eq. Hex.SignDet.Descriptor.compare_ofError proves that exact fallback value; Hex.SignDet.Descriptor.buildOrder_roots proves actual success and excludes that branch under the coefficient laws. The executable operation requires ordinary coefficient operations and signs, without a companion proof package. The proofs require canonical zero, allow other stored values to have multiple representations, and apply to arbitrary ordered real closed fields, including fields with infinitesimals. They use the proved shared root-sum semantics and Tau Ceti Thom identity/order foundations.

For two independently selected coefficients, the existing number-field constructor finds one coordinate field. Here √2 and √3 start as roots of different polynomials. The check confirms that the common generator is real and that both converted coordinates retain their original selected algebraic values, in the supplied order. Converting those coordinates to real algebraic numbers then checks the exact order √2 < √3 in their selected embeddings.

The converted coordinates can also be coefficients of a new sign/root problem. Write a = √2 and b = √3 in that common field. At the roots of (x − a)(x − b), the ordered queries x − a, x − b, and a − b have signs (0,−,−) and (+,0,−), each once. The impossible pattern (0,0,−) has count zero. The same check enumerates a before b and compares roots selected by x − a and x − b. Both derivative words are [+]; their equality does not identify roots of different defining polynomials. The sign function below evaluates a field coordinate on the common generator's certified enclosure, refining it when needed.

Here the common generator has degree four. Coefficient arithmetic uses actual QAdjoin coordinates. The sign function handles rational constants directly and uses interval evaluation for nonconstant coordinates. If its first two probes are inconclusive, an integer polynomial satisfied by the coordinate gives a proven precision bound for the final interval probe. The theorem Hex.QAdjoin.signApprox_spec proves that it returns the sign in the selected real embedding. The more extensive enumeration, comparison, re-encoding and replay checks run in the conformance suite against an independent exact algebraic-number oracle. The value-preservation theorem Hex.QAdjoin.common_get connects the coordinates to the independently selected original algebraic numbers. The table, selected-sign, and comparison correctness theorems apply to that embedding; their proofs use only Lean's standard logical axioms and the proved shared query and Tau Ceti foundations.

The sign-table and descriptor examples run checked producers and finite certificate checks; the changed sign vector above is rejected. The companion proves complete real-root counts, selected-root identity and signs using the proved root-sum theorem HexRealRootsTheory.Tarski.check_rootSum. The full-word comparison uses Tau Ceti’s delivered Thom identity and order theorems through the companion. Hex.SignDet.Comparison.order_root proves that all three orders returned by an accepted comparison agree with the original selected roots. Hex.SignDet.Descriptor.buildComparison_success proves that the actual comparison constructor succeeds; Hex.SignDet.Descriptor.compare_correct gives the result of the total operation. Universal root-list production and mathematical sorting are also proved. The common-field conversion preserves the selected algebraic values by the proved QAdjoin.common_get theorem.