18.16.1. Ordered coefficient dependencies🔗

SourceSelection assembles a selector for an ordered coefficient tuple. Each coordinate is either inherited from the actual origin, a checked selected rational root, or a rational polynomial in an earlier generator. The earlier index has type Fin n before appending the coordinate, so forward references and cycles cannot be represented. For example, this plan describes a selected root, an inherited value, and the coordinate α² − 1 computed from that root:

formula uses the existing shared integer syntax, retaining the selected root's ordered constraints and clearing rational denominators by a positive multiplier. unique identifies the whole tuple from this formula and the inherited identities. It follows the coordinate dependencies; clients need no bespoke tuple-uniqueness proof. The four-coordinate checks identify √2, −√2, an inherited 2, and √2² − 1. The final coordinate references the first generator across the other coordinates. Wrong conjugates and swapped computed coordinates fail the same selector. The native-point case generates its selector from actual QAdjoin computations −a, 2, and a*a−1, with the selected generator prepended. Its existing native fixture supplies the matching values, whose interpretation is proved. The matrix uses both computed coordinates, through x*c₁+c₂=0 and x²−c₃−1=0. One reader retains all four coefficient identities, the matrix, and both original closed divisors 2−√2 and 1+√2. Swapping the two computed native coordinates fails the selector alone, in both an ordinary interpretation proof and a separate compiled row control. These two supplied closed divisors test the finite-reader API; this example does not extract them from division syntax.

exists_real composes this generated uniqueness proof with the actual finite joint reader. It needs authentication of the requested source tuple, real-value evidence for precisely the inherited coordinates, the actual origin/provider history, a true joint row, and the signs of all supplied original divisor operands. Its conclusions retain the coefficient identities, sample, matrix and nonzero guards at one reader. The plan does not discover those inputs from arbitrary source syntax, construct a frozen context certificate, establish root coverage or provide general tactic acceptance. The rational descriptor is quoted in a module with public imports. A separate checked binding reader and the owner's Dag.descriptor_raw law bind its exact original header; the positive square-root alias follows from that checked head and interval. The native-point fixture retains its existing non-module construction boundary. The generic library laws use ordinary public module imports.

real interprets the plan, and formula_iff reduces source authentication to coordinatewise real equalities. A chained regression uses an inherited value, a computed generator and the non-integral relation c₂ = 1/3 + (2/5)*c₁, and rejects an incorrect final coordinate. Concrete two-root controls use separately quoted positive and negative √2 descriptors and reject their swap. The negative descriptor retains the strict interval (-3/2,-7/5) and its exact supplied polynomial. Its empty derivative request list selects by interval alone; the positive descriptor also checks its two supplied derivative signs. not_forall supplies the universal counterexample route, tested on the separately evaluated false sentence ∀ x : ℝ, x * (-Real.sqrt 2) + 2 ≠ 0. Its conclusion retains the reader, closure, all coefficient identities, the sample equation and both supplied guard domains and nonvanishing facts. A native inherited case consumes the actual origin identity for the coefficient 2. exists_real also retains negation closure, specialized polynomial sizes and agreement with every inherited origin value, so later proof assembly can use them for other guards.

FieldSelection.prepare constructs the plan directly from a checked rational root and existing QAdjoin coordinates. Its source tuple uses the actual Coefficients.ofField conversions; authenticated proves the full tuple identity using the owner's chosen-generator and coefficient interpretation laws. Clients need no proof about nested selector conjunctions:

nativeValues uses the owner's actual number-field presentation to pack these coordinates. nativeValues_real proves that their selected real values are unchanged. matrix_correct adds the generator at coordinate zero and shifts the original matrix, retaining coefficient order, the quantified variable and every domain guard atom. These inputs already belong to one primitive field; common-field construction and conversion of independent fields remain with their existing owners and frontend preparation. This assembly is not general frozen source/context quotation or accepted algebraic completeness.

The public factory consumer executes NumberField.present? and packs the original QAdjoin coordinates through nativeValues. Its sample is the packed value 1, distinct from the selected generator. It checks the shifted matrix and isolates the selector-only swap control. Its ordinary point theorem uses true_real, which interprets the plain matrix row through the actual model and ordered coordinates. The conclusion names the interpreted sample itself, so its sample-dependent divisor sample − generator is attached to that exact point. This model route does not need a selector conjunct: the presentation laws authenticate all coordinates. The separate finite-reader test consumes the selector and recovers the shifted original matrix at its identified reader. The proof presentation is a successful result of that same factory, by the owner's existence law; compiled execution is separate evidence. This module uses ordinary public imports and public meta imports for its executable controls, without import all. The direct point law retains every supplied nonzero guard; source-division collection remains the frontend's responsibility. A public inherited-coordinate consumer also applies formula_iff and exists_real with a supplied origin.RealValue identity, retaining coefficient/sample/guard ties without private imports.

18.16.2. Frozen selected-section replay🔗

SectionBuild.build searches the native family for a true selected section and freezes its descriptor, graph and complete ordered row. This producer currently visits selected roots; point roots and sectors need other producers. No supported witness returns none, which is not a false existential verdict. Producer failures retain the owner's actual error.

SectionReplay.check reads those supplied records and checks the shared matrix. It checks all supplied original divisors before parsing any packet. A malformed descriptor, graph or row is rejected. A true row yields an ordinary real witness; a false row yields only a counterexample at that section. Domain inequalities remain matrix atoms.

checkWith uses the owner's eight equal supplied coefficient operations during reconstruction and row checking. Missing stored literal facts reject decoding; missing intermediate arithmetic facts remain explicit demands. ScalarPacket.read validates each supplied scalar graph; restore retains its checked literal key and sign without repeating graph validation for subsequent lookups.

SectionQuote.finish reifies the original target again, checks the exact existential matrix, fixed valuation equality and every original divisor identity, then transports the checked witness to that target. These identities are ordinary proofs. The model and fixed coordinates must already be authenticated.

The fresh-source regression reifies ∃ x : ℝ, x^2 = Real.sqrt 2 ∧ 1 < x ∧ x < 2, produces a new native section and row, checks seed packets for the stored predecessor coefficients, and supplies newly reached scalar packets during kernel replay. This is independent of the existing hand-written row's truth theorem. In particular, the source matrix contains 1-x<0, while the older row used x-1>0; the new evidence binds to the actual reified polynomial order. The fixed positive √2 coordinate and its real interpretation use the existing checked fixture. A fresh compilation-unit regression quotes the source proof again with ordinary imports, audits its complete axioms and checks that its local proof closure retains replay rather than production. These concrete fixtures use the pinned toolchain's non-module import closure. The generic adapter modules use public module imports.

This does not supply arbitrary source coefficient discovery, recursive provider history restoration, all reached packing/inverse assembly, frozen complete cell coverage, or accepted algebraic search completeness. It does not register another rcf handler. Existing rational and real-coefficient tactic examples retain their current behavior.

18.16.3. Ordinary point replay🔗

PointBuild.build proposes ordinary parent-field points using the owner's sorted, deduplicated root family. It visits sections and sectors with point or linear-head boundaries. Its linear-head quotient and midpoint calculations are search proposals; replay does not trust a region label or an identity with a selected root. Nonlinear boundaries require further conversion certificates and are outside this helper. Returning none means no supported witness was found.

PointReplay.check restores a supplied point through a strict coefficient codec, evaluates the complete ordered source row and folds its Boolean matrix. All original divisors are checked before decoding. Missing recorded scalar facts reject the point; missing arithmetic records remain explicit replay demands through checkWith.

PointQuote.finish freshly reifies the original existential goal and authenticates its exact matrix, fixed valuation and ordered divisor identities through the shared Quote.finish boundary. These identities are mandatory input checks. The source equivalence is unconditional; they are checked separately from the returned proposition. check_domains proves nonzero interpretation of every supplied guard. Failure restores the saved state. The source tests produce and check witnesses equal to √2, above √2, between 1 and √2, and above √2 with x/2<1 and x/3<1, a zero section and a left ray. The scalar records are independently checked from new proposals; no old row-truth theorem is used. A separate ordinary import module quotes the between-roots source again. These fixtures use the already checked positive √2 parent and the pinned non-module import closure. The public generic modules have ordinary public imports.

This point path proves individual existential successes and gives point counterexamples to universal sentences. It does not certify a false existential, restore general recursive provider histories, or prove complete frozen cell coverage. It does not register another rcf handler.

18.16.4. Frozen root-table extraction🔗

RootReplay.read binds a supplied graph to one parent context, polynomial and open query interval. It derives the full derivative queries from that polynomial and checks supplied original divisors before parsing. Graph validation checks every entry, including unreachable ones; versions, context/domain bindings and earlier-only references remain mandatory. A rejected graph is evidence failure, not a root-nonexistence verdict.

For positive degree, extract uses the owner's accepted shared table instead of replaying BKR for each root descriptor. Every table word is retained, each descriptor has the original head/endpoints/full derivative slots, and the finite comparator sorts the list. The resulting domain proof establishes a nonzero squarefree head and valid root-free open endpoints. Repeated input polynomials need the owner's squarefree decomposition and transport; they cannot be passed unchecked to this reader. Half-open source domains continue to be shared matrix guard atoms.

Result.root_spec proves that every emitted descriptor denotes a root in the original interval. The frozen regressions check both roots of X²−2, an interval with just its positive root, a nonzero constant and an empty real root set. Acceptance runs under ordinary kernel diagnostics that forbid native root production and per-descriptor replay. Changed polynomials/domains/contexts, missing support, cyclic graphs and stale versions are evidence errors; a zero original guard is a divisor error even with a zero polynomial and malformed graph. The predecessor codec and arithmetic remain part of the surrounding assembly; frozen quotation must supply their checked finite facts and reject native coefficient production. These fixtures use the rational base, not general nested arithmetic quotation. A fresh module uses an emitted descriptor and checked domain to prove ∃ x : ℝ, x²=2 ∧ 1<x ∧ x<2 and a negative conjugate ∃ x : ℝ, x²=2 ∧ x<0, both with the standard three axioms. The negative proof consumes the actual checked derivative word at that root. These concrete proofs retain the pinned non-module import closure.

Result.coverage proves that every root in the bound open query interval occurs in Result.values, with no duplicate interpreted roots. Result.ordered proves strict mathematical ordering of that same list. Both laws consume the accepted full table and actual extraction, using the owner's supplied-replay exports. The native producer's coverage equation is not a certificate premise.

The fresh frozen-table consumer characterizes the complete real root set by x² = 2, proves absence for a nonzero constant and for X²+1, and checks strict order and absence of duplicates. Its actual theorem bodies and axiom inventories are checked separately from the reader's producer diagnostics. These laws interpret the list in the supplied lawful model; they do not construct that model from arbitrary provider history. Complete formula-cell assembly and joint real realization of internal infinitesimal samples remain separate requirements. This reader adds no tactic handler.

18.16.5. Frozen selected-root transport🔗

RootTransport.read checks a supplied descriptor after coefficient conversion. It preflights supplied source divisors and matches the context, polynomial, endpoints and derivative word against the actual map. A valid descriptor for a different root yields binding; invalid or incomplete evidence yields evidence. A zero source divisor yields divisor before parsing. A frontend must authenticate this guard list against the original source; this reader does not infer it from a goal.

readWith accepts equal supplied maps and arithmetic dictionaries. Its result has canonical proof indices, and readWith_eq preserves every result and error. The coefficient codec must independently restore its finite checked records.

An accepted descriptor gives the next actual context conversion through step. model consumes the owner's Conversion.Model.adjoinWith law and preserves every old-context value:

No native root-isolation success premise is used. Later scalar packing and quotation still need their own finite checked assembly. The fixed-parent regression moves the positive root of X²−2 into an authenticated positive-√2 context using three proved constant-sign records. The converted root still denotes Real.sqrt 2; a separately valid negative-root certificate rejects with binding. Missing records and a stale context yield evidence.

This checks one conversion step. Recursive provider/context history, all-live assembly and complete cell replay remain separate requirements.

The target context retains the supplied descriptor’s evidence. Equivalent roots with different evidence need not have equal context signatures. step_native agrees with adjoinChecked only if native production returns this exact descriptor; frozen acceptance does not use that premise. The checked result retains its exact source guard list and nonzero evidence. Checked.domains gives the source interpretation; Checked.transported gives nonzero converted guards through the owner’s zero-reflection law. A frontend must still authenticate that list against the original source goal.

18.16.6. Replay through a second selected-root context🔗

A selected root can be restored after its coefficient context has been rebuilt. The deeper frozen example first moves the selected positive √2 root, then restores the root of X²−√2 over that rebuilt context. The reader checks the full mapped subject; the owner's selected-root law preserves its ordinary real value. The fresh source proof uses the accepted converted root as the witness for ∃ x : ℝ, x²=Real.sqrt 2 ∧ 1<x ∧ x<2. The conversion identity links this witness to the original descriptor; its root membership and endpoints prove the property. A transitive dependency scan excludes the earlier row-truth and existential source proofs.

A checked frame retains the exact signature. Supplied operations at both levels and a proved reduction policy keep ordinary-kernel replay from calling native sign production. Five joint scalar records, two constant records for 1 and 2, and fourteen additional rational predecessor literals supplement the existing first-field inventory. Joint keys and signs are restored from checked evidence; the constant records use the authenticated parent sign. An interval or callback alone is not evidence.

The controls reject a different original descriptor and a self-consistent different endpoint as binding failures. Omitting one higher-level record or changing only the subject endpoint rejects as evidence failure. Removing the required 98/81 predecessor literal prevents joint packet decoding. A zero source guard rejects before malformed data. This extends fixed-parent replay; arbitrary histories, complete root/cell assembly and automatic source quotation still require their owning interfaces.

18.16.7. A complete matrix at one selected real point🔗

FiniteSigns.check checks a whole matrix at one selected point. Its query list starts with every source divisor as a constant polynomial, followed by the shared specialization's atom polynomials. The owner's finite descriptor and replay laws interpret that entire list at the same ordinary real point. The checker validates the guard prefix before evaluating the matrix, and rejects missing or extra signs.

A false matrix result describes this selected point. It neither refutes an existential sentence nor establishes that all roots and intervening cells have been considered. Boolean evaluation is strict: an apparently decisive left branch does not hide missing right-branch evidence.

FiniteQuote.finish quotes accepted finite evidence against a freshly translated source goal. It checks an exact ordered identity for every original divisor, derives its nonvanishing in the kernel, checks the fixed coefficient valuation and shared formula, and checks the resulting proof against the original target. These source protocol checks remain mandatory even when the unconditional source equivalence means the final theorem does not logically depend on their proof terms. A refusal restores the environment and metavariable state.

The frozen matrix regression uses this public quotation API to prove ∃ x : ℝ, x² = Real.sqrt 2 ∧ 1 < x ∧ x < 2. A second source retains x / (2 - 1) before normalization and checks its original divisor through the same joint replay. The proofs use canonical shared specialization and the owner's actual algebraic interpretation laws; the audit excludes the named earlier source theorems and reuse of the other quoted source. The fixed packet contains 31 scalar facts, 43 packing records and 21 stored-sign records.

The two-divisor regression quotes ∃ x : ℝ, x² = Real.sqrt 2 + 0 / (Real.sqrt 2 - 1) + 0 / (-1 : ℝ) ∧ 1 < x ∧ x < 2. Source preparation retains the ordered divisors [Real.sqrt 2 - 1, -1] and a second coefficient representing the whole first zero quotient. Both divisor signs are checked at the same point as the matrix, using one additional stored-sign record and the existing scalar and packing inventory.

Reversing or omitting their source identities refuses quotation and restores state. Replacing the first denominator by Real.sqrt 2 - Real.sqrt 2 also refuses, despite the zero numerator. A separate frozen packet records a zero first guard; it rejects before even a constant true matrix is evaluated.

Reordered queries, changed contexts and cyclic evidence reject during restoration. Missing stored evidence remains a kernel-assembly refusal; the supplied operation dictionaries are not a strict compiled checker for arbitrary packets.

The supplied-inverse regression quotes ∃ x : ℝ, x² + 1 = 1 / (Real.sqrt 2 - 1) + 0 / (-1 : ℝ) ∧ 1 < x ∧ x < 2. The inverse is a coefficient used by the matrix. The owner's checked inverse equation identifies its supplied value at the selected positive √2 root. One further packing record lets canonical specialization recover the existing selected-point queries; the matrix packet is reused through that checked equality. Both original divisors remain authenticated in source order.

A separate inverse packet is valid for the different pair (√2 + 1)·(√2 - 1) = 1; using it for the original request rejects. Changed outputs and context identifiers reject too. A zero inverse operand rejects before graph decoding. Source quotation refuses a changed numerator or zero denominator and restores state. The fresh inverse proof audit requires the actual inverse law, reader binding and whole-matrix checker in the proof dependencies. This is a supplied finite certificate at a fixed parent.

The fresh proof audit follows project theorem types and bodies, including private auxiliaries, and checks the exact standard three axioms. Separate kernel diagnostics check actual reader conversions and rebuilt acceptance decisions, require that the reader was unfolded, and reject native production during those checks. This is a fixed authenticated parent and supplied finite matrix. Automatic provider/context history, complete root/cell assembly and accepted algebraic decision progress remain separate requirements.