18.20. A frozen row at an ordinary selected root🔗

Hex.RCF.RealCoefficients.SelectedFormula.checkRow checks one complete ordered source-atom row at one selected ordinary real root. Supply the fixed parent's faithful real model, the authenticated coefficients, every original divisor, the shared formula, the selected-root context and a literal sign packet. Divisors are checked before the packet. A packet must match the exact root and ordered specialized polynomial keys; its graph checks the claimed signs together at that root.

A true row supplies one ordinary witness:

Hex.RCF.RealCoefficients.SelectedFormula.row_domains proves nonzero values for the supplied divisors. The frontend must still authenticate their source identities and retain divisors erased by cancellation. A false row supplies a counterexample at that point through Hex.RCF.RealCoefficients.SelectedFormula.row_false; it does not decide that an existential sentence is false. Malformed evidence and incomplete rows retain separate diagnostics.

The frozen regression constructs the positive root α of X² − 2, proves that its original value is Real.sqrt 2, and constructs a further selected root of X² − α on (1, 2). Its shared formula retains the equation and both strict bounds, with the checked joint row [0, 1, −1]. The fresh source proof concludes ∃ x : ℝ, x² = Real.sqrt 2 ∧ 1 < x ∧ x < 2. The existing rcf example proves the same sentence through the independent polynomial-quotient path; the frozen regression exercises the native selected-field representation.

The regression restores the upper descriptor from parsed literal data and structural graph expansion with Descriptor.ofChecked. It supplies checked predecessor operations for both specialization and replay. Kernel diagnostics reject listed native sign/root producer unfolds during generated scalar, upper-data parser, root, row and collected refusal checks. Parent construction and separately elaborated source/codec controls receive ordinary kernel checks outside that diagnostic guard; zero requests alone would not establish it. Wrong coefficients, reversed keys, a forged sign with unchanged keys and graph, a crossed context, a stale version and an original zero divisor are rejected. Missing arithmetic intermediates stay unresolved rather than yielding a Boolean verdict.

Rebuilding the complete frozen conformance fixture with owner dependencies warm took about 140 seconds on the recorded shared host; its largest child used about 8.8 GiB RSS. These are ordinary build observations, not a scaling or speedup claim. They include parsing, root and row quotation, refusals and audits.

This is an ordinary selected-root row API, conditional on the supplied faithful parent model. It provides neither complete root coverage nor a generic frontend certificate producer, universal sentence decision or nested infinitesimal realization. Source reification and original-goal transport remain obligations of a caller integrating the API.

A second frozen regression uses the owner's original-packing records for row arithmetic. Each record binds its original polynomial, retained representative and scalar sign to joint evidence for the representative and their difference at the same selected root. A value-preserving reduction alone does not identify the original request: a record for −2 cannot replace the requested record for −α². The regression removes that record while retaining −2, and separately removes an original zero and a nonzero constant. Each missing request stops kernel replay before a Boolean verdict.

The fixture has 42 records captured from historical row collection and one additional nonzero original X² − 2 that packs to canonical zero. All 43 records have named kernel-checked laws tying them to the supplied scalar and joint packets. The complete literal closure and actual acceptance proof bodies are audited. Replay uses zero producer fuel; active kernel diagnostics separately exclude the listed native producers. Source coefficients use authenticated Element.restore; the upper descriptor and row packet still use checked scalar-fact inventories. This does not reconstruct a general context catalog, prove full algebraic progress or make arbitrary compiled dictionaries refuse on a missing record.

The byte entrypoints checkBytes and checkBytesWith apply the owner's byte/depth/integer-token limits, JSON parser and checked packet codec before the same selected-root row check. All supplied original divisors are checked before parsing, including malformed or zero-budget input. The eight supplied arithmetic operations have the same checked equalities as literal row replay. The limits bound lexical decoding only. Compiled canonical arithmetic can run native production, as can cached arithmetic on a fact miss; that cost is not bounded by these limits. Decoding also depends on the supplied value codec. The fixture uses the strict sign-fact codec. Its kernel proofs use the writer and parser laws, without evaluating native production branches.

The result is Except String (Except Replay.Error Bool). An outer error retains the owner's decoding or authentication diagnostic unchanged, including version, root-binding and stored-sign failures. Evidence rejection can occur in either result layer. An inner replay error, accepted true and accepted false stay distinct. Diagnostic strings never choose another solver. bytes_sound gives one ordinary real witness; bytes_false gives a counterexample at the selected point, without deciding an existential sentence false.

The byte regression uses the actual 38,990-byte encoding of the same frozen row. A kernel proof binds its constructor bytes to the owner writer; an independent lexical-limit proof and the owner's parser law recover the checked packet. The fresh source proof concludes the same complete original sentence. The byte data's entire definition closure is checked separately from proof axioms and compiled refusal controls. This checks bytes for a supplied immutable context; it does not reconstruct an arbitrary context catalog or remove the row API's source and model obligations.

A further conformance example supplies a complete selected-root packet to an empty catalog with its validated rational base. The 2,911-byte packet retains the full predecessor α=√2 and selected upper root of X² − α. Kernel proofs bind both constructor JSON and bytes to that root, reconstruct the original parent through writer identities and owner round-trip laws, and prove the same original existential statement at the returned root's ordinary real interpretation. Compiled catalog controls check the valid packet and reject a stale binding, the wrong root kind and a changed endpoint with its old graph binding. Separate kernel proofs check context-reader refusals, byte limits and truncation. The 75 JSON and 21 byte definitions have complete constructor audits; actual proof bodies separately exclude the listed root/sign producer definitions.

This checks one supplied root and its source statement. It does not establish root-set coverage, a generic certificate producer or strict compiled catalog replay. The round-trip proofs do not evaluate frame validation; compiled controls use the default codecs and adjunction, which retain native paths. The proof uses the owner's leaf-encoding law rather than evaluating a native hash function, and composes the byte parser before catalog reconstruction.

A retained Mathlib-free experiment at source d84cecf uses this one 2,911-byte packet. Six alternating trial blocks retain eighteen samples, with host-specific median cumulative costs of 44.080 μs for lexical bounds, 153.576 μs for parsing and 407.027 μs for default catalog reconstruction. Native coefficient/adjunction paths remain. Preparation and proof construction are excluded; no scaling, strict-replay or tactic-speedup claim follows. Child memory includes startup and the harness.