18.15. Native sample coefficient conversion🔗

A Tower.Sample evaluates coefficient polynomials after entering its own context. NativeSamples.row_converted proves that its complete source row agrees with native specialization at the converted coordinates. It consumes the actual owner conversion model over an ordered model field; that field can be non-Archimedean. It assumes no global ordinary-real interpretation of the parent context. The shared specialization proof is generalized to that model field, retaining its existing real API. sign_converted retains every original divisor's sign. In an infinite model field, size_converted also preserves normalized sizes, hence degrees, including zero polynomials and leading cancellation. The owner interpretations reflect zero without identifying distinct nonzero representations; no global real reader is used for this step.

Here the public section constructor supplies the conversion for its selected root. The coefficient coordinates enter that same context before evaluation:

The sample conversion regressions use the actual selected positive root of X²-2. Its row retains zero and repeated-root atoms, leading cancellation, and the (1, 2] guard atoms. Changing the source coefficient from 2 to -2 changes the row at that same root; an empty atom traversal remains empty. Size tests distinguish zero from nonzero constants and retain repeated-root degrees and leading cancellation. Native execution and ordinary-kernel row proofs check the same expected sign words separately. A nested section uses the actual selected √2 coefficient in x² - c; the owner conversion model retains its selected embedding and polynomial sizes. Its source and converted rows are both [0, 1, -1], with separate ordinary-kernel proofs using the selected root’s actual facts. Changing the coefficient to the negative conjugate gives [1, 1, -1] at the same upper root, also kernel-checked. The source size words are independently kernel-checked. Actual point consumers construct the rational provider history and inherited coefficient identities for the X²−2 section: a true row retains the parent divisor 2, and a false row proves ¬ ∀ x : ℝ, x² > 2.

The infinitesimal-parent sample regression constructs the owner's ordered real-closed reference field from an actual infinitesimal base history. The supplied frozen descriptor selects the positive root of X² − ε in (0,1). The ordinary-kernel reader checks that replay and its exact polynomial, bounds and derivative slots. The public section constructor supplies its extension conversion model. A converted true row yields one ordinary reader on a finite closed domain, with 0 < x < 1, the root's square equal to the converted ε, and that original guard nonzero. No inherited source coordinate pins this guard to a predetermined real number. The sample and guard are realized together; an infinitesimal is never used as a real witness. The conformance file uses non-module imports, which expose private definitions in this toolchain; it does not establish public-only elaboration of this concrete fixture.

NativeSamples.true_real consumes a true sample row, inherited base/provider coordinate identities and strict nonzero parent-context signs for every supplied original divisor, using an infinite model field. It derives the matrix, sizes of the original parent polynomials and real nonvanishing at one reader. NativeSamples.not_forall uses a false point row with those same inherited coordinates for a universal counterexample; it takes no divisor guards. The target provider history and inherited identities remain explicit. Origin.RealValue only fixes values embedded from the staged base/provider; it does not fix arbitrary algebraic suffix coordinates such as the nested √2 coefficient. That test's coefficient_fixed is an identity in the owner conversion model, not an input to these point APIs. Proving selected-root source identities at the finite reader remains a separate obligation. These point laws establish the coefficient-conversion bridge; a complete sample certificate must still check cell membership and full coverage. They do not implement complete frozen context/cell replay or source-goal quotation.