Repository navigation
Implement the real-closure family through verified APIs and performance evidence #10331
Description
Outcome and ownership
Complete the real-closure family designed in #10143: computation in real closures of ordered rational-function fields, caller-supplied transcendental constants and infinitesimals; complete root/sign APIs and ordinary-real univariate rcf proofs. This is the coordinator, not a competing implementation assignment.
The contracts are the family design, execution contract, eight library SPECs and real-coefficient tactic contract. Issues govern scheduling; SPECs govern mathematical/computational behavior.
| Issue | Remaining owner / assignment status |
|---|---|
| #10377 | Active worker: finish BKR/Thom producer APIs, root naturality, certificate interfaces and performance. #10547 supplies the Thom bridge; #10548/#10549/#10550 continue enumeration/comparison/common-field examples. |
| #10378 | Active worker: complete ordered tower roots/multiplicities, all-live enlargement, native/union correspondence, samples/exploration and tower integration evidence. Preserve the implemented arithmetic, finite-suffix transport and checked enlargement through #10573. |
| #10358 | Ready to assign: remaining coefficient source coverage, caller-registered constants, complete tactic construction/checking, algebraic-only completeness, diagnostics and manual. Existing algebraic/common-field examples stay working. Independent work can start before the entire tower is finished. |
| #10352 | Ready to assign independently: finish the existing rank Phase-4 evidence and resolve the recorded quotient-checker concern. No duplicate rank assignment. |
| #10577 | Ready to assign: audit and complete Sturm/real-algebraic prerequisite implementation/evidence through Phase 4, including justified metadata. This avoids making upstream readiness depend on final downstream integration. |
| #10575 | Final integration, family proof/API polishing and documentation, acceptance audit and candidate split-package preparation. Formal distribution eligibility of every transitive input and actual release dispatch are separate. |
No additional implementation issues are needed merely to divide these assignments into PRs. Keep algorithms and proofs with their existing owners. A concrete false premise must be reported and corrected, not worked around by creating more issues or weakening the theorem.
Delivered foundations to reuse
- Implement effective Sturm–Tarski computation and algebraic correspondence #10375: shared polynomial/query computation, validity and producer/checking infrastructure.
- Prove Sturm–Tarski root semantics after the Tau Ceti foundation #10389 via Prove shared Sturm–Tarski root semantics and remove the RCF admission #10521: the full arbitrary-certificate
Tarski.check_rootSumtheorem, general and integer/dyadic semantics and exact-domain root counts. Its former admission is removed. - Implement ordered rational-function extensions and their proofs #10376: proved ordered rational-function extensions, successive infinitesimals, separate approximation computations/width/containment, total proof-founded searches, conditional progress and library-local Phase-4 evidence.
- Tau Ceti: ordered algebraic real-closure existence, IVT/Rolle, Sturm–Tarski, finite BKR and Thom identity/order. Hex's current pin and Prove Thom root identity, order and general reencoding #10547 consume the delivered results. Completion of the broader roadmap is not a family dependency.
- Existing real-coefficient rcf/manual work includes selected algebraic roots, sqrt/cubic aliases, QAdjoin arithmetic and independent common-field examples. The rational solver and its imports remain intact.
There is no named-admission exception. Every completed new claim and tactic result must reject sorryAx, new axioms and native_decide. Neither roadmap closure nor external numerical agreement establishes a theorem.
Completion DAG and readiness
Arrows below mean a prerequisite for final completion, not necessarily a barrier to starting independent work:
flowchart LR
readiness["#10577 Sturm / real-algebraic readiness"] --> sign["#10377 BKR/Thom"]
rank["#10352 Rank performance"] --> sign
sign --> tower["#10378 Towers and samples"]
tower --> tactic["#10358 Real-coefficient rcf"]
tactic --> integration["#10575 Integration and release preparation"]
integration --> tracker["#10331 Family acceptance"]
The rank and prerequisite-readiness edges govern phase attestation; they do not prevent use of proved merged APIs. #10577 owns the four upstream libraries through Phase 4, #10352 owns both rank libraries through Phase 4, and #10377/#10378 own their libraries through Phase 4. #10575 owns subsequent family proof/API/documentation finishing, so upstream phase readiness never depends on downstream closure. #10377/#10378/#10358 can continue using proved merged APIs. #10358 should start its source/registration and direct-real-sample work now; its general infinitesimal path waits for #10378's joint real realization. #10575 checks all three owner contracts and rank evidence, not only the tactic examples. Closed #10375/#10376/#10389 are available prerequisites, omitted from this open-issue view.
The important theorem-level handoff is #10377 → #10378: selected-root naturality under ordered embeddings, universal enumeration and total cross-polynomial comparison. The important downstream handoff is #10378 → #10358: complete root/cell coverage and one ordinary real witness realizing the full finite set of signs and boundary constraints. Do not substitute individually realizable signs for simultaneous realization.
Experiments, SPEC revision and implementation
Use experiments only to answer concrete unresolved integration questions: a nested sample exporter/checker fixture, the actual caller-registered-constant prepare/build/check/proof path, or an observed performance problem. Preserve failed attempts and completed measurements. An experiment does not discharge a universal correctness or totality statement.
If an experiment exposes a contract gap, amend the owning SPEC before implementing the changed contract; discuss substantial architecture changes with the user. Keep generic arithmetic total, reuse the single shared Tarski computation, and retain mathematical equality through interpreted zero differences rather than structural inequality.
Implement and prove the accepted contract, add independent tests and representative ordinary-kernel examples, and finish the required compiled performance evidence. Follow the current PLAN/Phase4.md proof track: CI-built tactic/certificate examples, not compulsory timing sweeps for ordinary theorem applications. Timing a theorem application does not prove computational complexity.
Family acceptance
Keep this tracker open until #10575 records integrated monorepo acceptance and its limited package-preparation result. Complete distribution readiness and release dispatch remain separate; record their precise prerequisites rather than claiming they are delivered. Required coverage includes:
- Complete sign tables with support completeness, selected-root identity/order, total root enumeration/comparison and properly bound cross-level evidence.
- Total tower arithmetic, reducible-root inversion/splitting, clean representation, all-live context transport, complete ordered roots with multiplicities, base enlargement and native/union correspondence.
- Exploration constructors/comparisons/roots and value-preserving roundtrips, with agreement over ℚ with HexRealAlgebraic.
- Section/sector interfaces for downstream CAD/coverings and simultaneous real realization of nested finite constraints; no implementation of those downstream algorithms here.
- The specified real-valued tactic grammar, fixed selected algebraic embeddings, authenticated caller constants, all original divisor guards, complete roots/cells, verified producer/checker and useful diagnostics/manual examples.
- Pinned independent Z3/python-flint conformance, corrected paper Example 3, successive infinitesimals, nested roots, non-monic/reducible definitions, representation changes, and malformed/stale evidence.
- Required tower8/MetiTarski/Rioboo/Strzeboński and clean/eager evidence, nested coefficient costs and the existing rank/BKR obligations. Do not advance dependent phases while a required result is unresolved.
- Integrated build/CI/import/axiom audit, appropriate proof/API polishing, runnable documentation and candidate downstream package consumption. Use merged staging infrastructure when available; a sync dry run alone is not staged-consumer evidence.
Scope and working rules
The caller supplies approximation computations with separate proofs of containment and requested width. General termination additionally needs transcendence over the entire preceding field; individual transcendence facts do not establish algebraic independence. No bundled π/e providers or HexInterval development is commissioned.
Computational libraries and executable benchmarks remain Mathlib-free. Preserve the existing rcf command, rational fast path, and optional adapter boundary. Full CAD/coverings, multivariate/nested QE, nonstandard-analysis tactics and unrelated Tau Ceti roadmap work are excluded. Actual release dispatch/announcements follow the maintainer's schedule.
The user assigns workers by hand. Issue edits do not start workers or monitors. PRs target upstream main, use independent Opus review through $second-opinion immediately after opening, address local/CI/review failures, and merge green with gh pr merge --squash --auto without --delete-branch. Do not edit AGENTS.md or PLAN.md.
Acyclic example ownership and distribution limits
#10377/#10378 own direct library examples and supply APIs; they do not wait for
#10358's tactic/manual PRs. #10358 alone owns those tactic examples. #10575
verifies the integrated result and completes per-library API documentation
without duplicating the tactic implementation.
Actual distribution also needs Phase-7-eligible inputs, maintainer-created
mirrors and release tooling. #9809's existing HexPolyFp performance concern is
an external release-readiness concern, not a request to expand this family into
finite-field polynomial development. #10575 must report it and any other
unmet distribution prerequisites; monorepo acceptance does not close them.
Activity
kim-em commentedon Sep 20, 2026
Foundation contract milestone: #10300's existing Tau Ceti roadmap PR420 now contains the missing universe-polymorphic ordered algebraic real-closure existence target at commit
a60977aeac0377e0d9efd3cbd508fd9584ddf3ba, alongside the abstract univariate theory. The worker reports full build, fresh Opus review and final green CI; code-owner review/merge remains required. Exact target/source and verification are recorded in #10300 (comment).This supplies a reviewed candidate statement and proposed ownership (
TauCeti/FieldTheory/RealClosure/), not an implemented theorem. No Hex proof dependency is released. The next foundation step is an audit of actual TauCetiProject/TauCeti source, existing work and contribution rules before issuing/dispatching the implementation in that repository. Do not send a foreign repository issue number to the Hex dispatcher.Separately, #10351 now owns real-closure computation; #10318 is running for its companion contract; #10350 owns the downstream real-coefficient RCF integration design after that contract. #10352 is the ready HexRank Phase-4 prerequisite, with existing algorithms/CI reused and no unrelated new rank features.
kim-em commentedon Sep 20, 2026
The Tau Ceti contribution audit is complete. TauCeti AGENTS.md says that “The roadmap gates new mathematics” and requires declarations to advance a roadmap target. The new RealAlgebraicGeometry area is absent from roadmap main; roadmap PR #420 still requires human code-owner review. Therefore foundation implementation dispatch waits for that scope decision. Green CI and the candidate statement do not discharge this requirement or any Hex proof obligation.
The coordinator will recheck the repository-qualified roadmap PR during reconciliation. After approval/merge, it will reread the approved targets, check existing APIs and work, then create the first concrete missing ordered-preordering prerequisite in TauCetiProject/TauCeti and launch from that repository under its own review rules. No overlapping implementation was found in the audit. Independent Hex work continues; #10352's worker has been verified live and has claimed the assignment.
kim-em commentedon Sep 20, 2026
#10332 tranche 1 is merged: #10347, commit
825fea66c757744a080f0e90cd5034beaa70d88c.HexRealRootsMathlib.RealClosedand the lower umbrella now provideReal.instIsRealClosed; the real-algebraic companion consumes the generic odd-root theorem instead of keeping its own private ℝ proof. Local builds, axiom guards, fresh-module use evidence, independent Opus review, and full CI passed.The exact declarations and remaining gates are recorded on #10332. This does not remove #10339's shared-interpretation/signed-query gate. #10333's API PR #10348 is still open, #10335 has no published query/replay milestone, and actual proved Tau Ceti foundations remain distinct from the roadmap. #10332 stays open; the worker is relinquished pending a usable continuation milestone.
kim-em commentedon Sep 20, 2026
Final scope clarification from the user: retain the paper's transcendental extensions through a user-supplied approximation procedure. HexInterval and HexIntervalMathlib are out of bounds today. We are not removing generic K(τ), relative-transcendence hypotheses or certified refinement; we are removing the commitment to build/admit an interval library and deliver bundled π/e providers.
#10334/#10342 and unmerged PRs #10345/#10349/#10357 remain cancelled; their branches and results are preserved, their workers have acknowledged stopping, and their CI runs were cancelled. #10337 now depends only on the shared polynomial milestone #10333. The owning family/OrderedFn/tower/RCF SPECs are being revised in a scope-correction PR. All current directives have the new approximation boundary; later optional adapters need separate authorization.
kim-em commentedon Sep 20, 2026
Work on the fallible HexPoly API is paused. The user has rejected this architecture and requested investigation and likely revert of #10348. Do not build on the merged PolyOps API or treat that merge as a released dependency gate.
The design originated in the family revision in #10319 (commit 2620731), was expanded into the HexPoly SPEC by #10322, and became implementation directive #10333. I own the mistaken directive and the corrective audit/revert; the implementation worker followed the specified contract. The central error was expanding a bounded transcendental sign-refinement requirement into a general budget/evidence framework for polynomial arithmetic. The affected family launches are held pending correction. No replacement architecture is authorized by the old directives.
kim-em commentedon Sep 20, 2026
Audited independent merged work:
75e903f08e93521685cc6a11355a84333931c2dd, with successful required CI and a fresh Opus review finding no soundness blockers. It produces shared syntax, fixed coefficient valuation, preserved divisor obligations and a kernel-checked equivalence. It does not authenticate coefficients or solve numerical goals. Delivered artifacts and remaining obligations.01ad7e59944bb637b306ab0ef166f8f640019b8dafter review responses and green CI. The full-rank quotient checker scaling concern remains; HexRank stays at Phase 3. The isolated tail-accumulator measurements finished without demonstrating a speedup. Audit and retained experiments.Both owning terminal workers stopped at their account usage limit; neither is actively progressing. Neither issue is complete and no dependent completion gate is released.
Correction #10365 is rebased without conflicts onto these merges, at
df07077cadfb3de6709e13257132a8265af47ae4; its SPEC now describes the actual delivered frontend. DAG, whitespace and 367 relative-link checks pass. It remains held for the previously surfaced benchmark law-proof setup decision; no policy exception or held implementation launch has been made. HexInterval remains out of bounds. The monitor service remains active.105 remaining items
kim-em commentedon Oct 17, 2026
#10358 continuation: #10974 is OPEN at ce33258, with its fresh Opus findings addressed and current CI38999776414 still running. It now audits 65 actual callback/public theorem bodies and 14 definitions, including accepted primitive, constant-form and metadata-wrapped callback equations. The original complete codec and checked target are retained; the native-producer/canonical-codec guard remains unchanged. The final affected compatibility/manual selection passes. #10973 is actually merged; #10974 is not yet a landed artifact.
#10975 is OPEN at ac8093c, targeting main and gated on #10974. Two fresh Opus reviews were addressed. The complete table now yields count2, Nodup, strict real ordering and both directions of the exact solution-set equivalence, plus the ordinary witness ∃x:ℝ, x²=Real.sqrt 2 ∧1<x∧x<2 with both exact original reader equations. Explicit compilation of emitted data fixes the earlier join-point/ExplicitBoxing failure: the compiled original reader, polynomial size3, restored roots2 and empty-scalar-facts refusal controls pass. No compiler/kernel check is disabled. Its 74-theorem/14-definition fresh audit, manual and final narrow/desktop captures pass. Current CI38999563953 is still running; auto-merge is off on both PRs and exact new-head green remains required.
The local continuation additionally validates a generic supplied-facts recursive predecessor callback at two selected-field levels and in an ordinary public module (34 actual theorem bodies/5 definitions, complete standard-three axiom closure, unchanged producer guard, exact/one-below budget and missing/wrong-context refusal). A fresh Opus review is running; this will continue #10975, without a duplicate issue/PR. It consumes explicit checked facts and does not yet discover/authenticate arbitrary histories.
#10358 remains OPEN for generic original-source/provider/predecessor assembly, the general tactic and accepted completeness, remaining conversion/finite realization, strict compiled whole-reader missing-arithmetic rejection, native inverse/xgcd stress and full required evidence. The latest #10967 check is still OPEN at8c1a092bfc28425a8b432cd2b4a55411d8b0d65e; its model equation is not an inverse/gcd or strict-reader repair. The existing owner request remains on10378. #10633/#10634 evidence is preserved; no new scaling or speedup is claimed. No owner arithmetic/proof, issue, worker or dispatch is duplicated. Own local Lean/browser work remains one job at a time under hard aggregate32GiB/no swap/two Lean threads.
kim-em commentedon Oct 17, 2026
PR #10974 is MERGED as squash
3ea33c756f3191a99264a01cc651c7eb7f51f9ae, from exact reviewed headce33258f013b1d1a909e1f22d2e1b563a8092340. CI38999776414 / job117300102478 completed SUCCESS, including conformance, the full manual, benchmark smoke and oracles/BZ gates. The same-run watcher exited0 after the quota reset; the earlier observation403 did not cause a CI rerun. The squash tree exactly equals the reviewed head (5028c71a68d6084169dec21de5aed856a9f323ce). Squash auto-merge used the exact match-head flag and omitted branch deletion; remote issue-10358-cell-decision is verified retained at ce332. #10358 remains OPEN.Landed artifacts: shared RootQuote.DecoderM/quoteWith/runWith/run transactions and accounting; ScalarQuote.quoteWith/quoteDecodeWith/quotePolyWith and public normalized-vector laws; strict coefficient-array decoding and exact original polynomial-reader transport using the original type/instance/codec spine; explicitly compiled public emitted data; actual nested, primitive, constant and metadata-wrapped callback regressions; separate ordinary public module consumers; and the checked manual/report/source-bound evidence in reports/hexrcf-shared-quotation.md and its linked records. The importing audit checks65 actual theorem bodies/14 definitions under unchanged native-producer/canonical-codec diagnostics and exact standard-three axiom closure. Nodes818/1579/2397/9143 and the8137+1006 final nested charge are pinned. Five fresh isolated Opus reviews completed; actionable findings were addressed before green merge.
The next existing continuation is #10975, now pushed at237dbbde24130f9686de0628b6d74b5f2c87051f (functional source01ced8d2be; final layout2920d47c93). It proves the complete strictly ordered real solution list and bounded fourth-root witness through the checked table, compiles the actual reader/data controls, and adds supplied-facts recursive scalar quotation. Its final audits pass87/5 recursive,74/14 root-table and65/14 callback bodies/data, plus scalar/rational compatibility and all42 originalπ/e proof bodies. Two fresh reviews of each component were addressed. The final book and all4 new1440/390px captures pass;6 local targets have zero overflow.88 verified artifacts retain the73px failed layout and all diagnostic attempts. This is not yet landed.
GitHub correctly reports merge conflicts against the newly landed prerequisite; that prevented creation of CI for237db. I am reconciling the actual squash in the same PR, then requiring exact updated-head green CI. This is not a CI failure or a rerun for the old observer403. Auto-merge on10975 remains off.
Remaining full scope: generic original-source/provider/predecessor assembly, general tactic/accepted completeness, remaining conversion/finite realization, strict compiled whole-reader missing-arithmetic rejection, native inverse/xgcd stress and full required evidence. The existing owner request remains on10378;10967 was still open at the latest owner check and is not assumed merged or an inverse/strict-reader repair. #10633/#10634 work stays preserved, no general speedup is claimed, and no owner proof, issue, worker or dispatch is duplicated. All own local Lean/browser work remains serial under hard aggregate32GiB/no swap/two Lean threads.
kim-em commentedon Oct 17, 2026
Continuation is pushed on the existing issue-10358 branch at
73776d2137c25215d8a3e3ca0a527d7c583c81ca; no new issue or PR was opened. This is not a merged artifact or full completion.RootQuote.quoteOptionWith,ScalarPacket.read_restoreandScalarPacket.quoteWithnow compose the exact original optional sign-packet reader through an equal checked prepared context, preserving the original model/codec/polynomial/sign/graph argument spine. The newly quoted fact alone drives coefficient decoding.decoded_valuecombines that exact canonical reader with the real interpretation −2√2; the fresh audit explicitly excludes the old Records fixture list. Actual caller assignment/restoration on success and final exhaustion, wrong-sign and wrong-polynomial rejection with an otherwise valid graph, empty-graph rejection and forged-context preflight pass. Context binder/type checks and inferred Option universes are in place; no failure is classified by diagnostic text.The final affected selection passes11787 Lake jobs:80 actual new-path theorem bodies/11 definitions and81 nonempty diagnostic traces, complete standard-three axiom closure, unchanged native-producer guard, scalar/rational/recursive/shared compatibility, all42 original named-constant proof bodies and the checked manual chapter. Runtime1min3.939s, CPU1min59.646s, peak2.2GiB/no swap are reused-dependency validation observations, not scaling or speedup evidence. The full book render is in progress, serially under the verified aggregate32GiB/no-swap/two-thread limit. Fresh Opus1 found no soundness defect; its meaningful refusal/manual/binder findings were addressed. Fresh Opus2 is running read-only.
A separate fully frozen ordinary-module packet probe exposes a precise owner API gate:
Tower.Signature.codecis unexposed, so the full-signature decode cannot be unfolded.codec_lawfulalone cannot connect its encoded input to the supplied frozen literal; the public rational-parent encoding identity fails by reflexivity. The requested publicSignature.codec_literalor encoding projection equation is documented with the actual reproducer at the existing10378 owner request. Encoded-context variants additionally reached a later Boolean replay boundary, so the first lemma is not presumed to solve every public import obstacle. All failed probes are retained outside the default build. I have not copied owner codec/arithmetic proofs or claimed passing public-module packet quotation.The already-reviewed10975 remains on its existing exact-head CI39003871439, with squash auto-merge enabled for ae50996 and no branch deletion. Its same-run monitor remains live; this continuation has not cancelled or restarted that CI.
#10358 stays OPEN for the public frozen-history boundary, generic original-source/provider/predecessor assembly, general tactic and accepted algebraic completeness, remaining conversions/finite realization, strict compiled whole-reader missing-record rejection, native inverse/xgcd stress, and all remaining acceptance/manual/evidence requirements. #10633/#10634 artifacts are preserved. Existing owner requests remain with10378, and10331 owns downstream dispatch.
kim-em commentedon Oct 17, 2026
PR #10975 is MERGED as squash
6c8a9a35f83fe2e75a71247d79a7cef615126118, from exact reviewed headae50996ab1a1f3ee0c71959d38eea722f48bc45c, at2026-10-17T06:15:26Z. CI39003871439 / job117312272681 completed SUCCESS, including architecture experiments, the full manual, benchmark smoke and conformance oracles/BZ gates. The same-run watcher exited0; its earlier observer403 never caused a CI rerun. The squash tree exactly equals the reviewed head (efc6dc9745d850671303ad7fe7cc2bac907d1f6f). Merge usedgh pr merge --squash --auto --match-head-commitwithout branch deletion. Remote issue-10358-reader is verified retained at ae509, and10358 remains OPEN and assigned.Exact landed artifacts: the six
conformance/HexRCF/RootTableQuote/modules,RecursiveScalarQuote, its ordinary public consumer and fresh audit, generic-Except RootQuote and recursive ScalarQuote callback wiring, default Lake targets, the two checked manual subchapters andreports/hexrcf-packet-quotation.mdwith its source-bound records/captures/failed attempts. The complete table gives two distinct, strictly ordered real solutions, both directions of the exact solution-set equivalence, and the ordinary witness ∃x:ℝ, x²=Real.sqrt 2 ∧1<x∧x<2, retaining the exact original polynomial and table reader equations. Actual compiled reader/data controls pass after explicitly compiling emitted data; no compiler/kernel check was disabled.The fresh importing audits check74 root-table theorem bodies/14 definitions and87 recursive theorem bodies/5 definitions with complete standard-three axiom closure and the unchanged producer guard. Recursive regressions cover actual accepted primitive/constant/metadata callback forms, charged decline/retry, wrong or missing inner facts, caller assignments restored on success/final exhaustion, exact/one-below budgets and an ordinary-module consumer. Two fresh Opus reviews of each component were addressed before green merge. The final manual and all four new1440/390px captures pass;88 verified recursive artifacts retain the failed73px layout and diagnostic attempts. These are validation and proof-accounting observations, not general scaling or speedup evidence.
Independent sign-packet continuation is pushed on issue-10358 at73776d / f47e495, with a checked narrow-layout change at6220ac. It replaces reliance on the old scalar fact list for the demonstrated coefficient with a checked original packet and reader/value composition. Its80-body/11-definition audit and meaningful failure/state controls pass; fresh Opus1/2 found no soundness defect and substantive findings were addressed. It is not landed and will be reconciled against this actual squash before a later Refs PR. The fully frozen public-module signature-codec equation remains an explicit existing-owner request at #10378 (comment); no public packet acceptance is claimed.
#10358 stays OPEN for generic original-source/provider/predecessor assembly, the general tactic and accepted algebraic completeness, remaining conversions/finite realization, strict compiled whole-reader missing-record rejection, native inverse/xgcd stress and all remaining required conformance/manual/evidence. The broader owner requests remain with10378; no owner proof, issue, worker or downstream dispatch is duplicated. #10633/#10634 artifacts are preserved. Own Lean/browser work remains serial under hard aggregate32GiB/no swap/two Lean threads;10331 retains dispatch.
kim-em commentedon Oct 17, 2026
PR #10976 is MERGED as squash
e63413f4be711404bb1eee6ec413434459c34e67, from exact reviewed head9a0a04244f71430d7b51f073639f62cb52e6bd5c, at 2026-10-17T07:54:20Z. CI39011084131 / job117333620626 completed SUCCESS, including conformance, architecture experiments, the full manual, benchmark smoke and oracles/BZ gates. The single120-second watch exited0. The squash tree exactly equals the reviewed head (33f7be540ac94155b3fa2ea34ecb030aca14c535). Exact-head squash auto-merge omitted branch deletion; remoteissue-10358is verified retained at9a0a04. #10358 remains OPEN and assigned.Landed artifacts:
RootQuote.quoteOptionWithand its ordinary optional-reader transport;ScalarPacket.read_restore;ScalarPacket.quoteWith; default optional umbrella/Lake wiring; the newSignPacketQuoteandSignPacketProofsconformance modules; checked manual/README coverage; andreports/hexrcf-sign-packet-quotation.mdwith97 source-bound verified artifacts, retained failures and actual desktop/narrow captures. The exact original optional packet reader is restored after checking through an equal prepared context, preserving its full model/codec/polynomial/sign/graph spine. The new fact alone drives coefficient decoding and its ordinary real interpretation−2 * Real.sqrt 2, without the old Records fixture fact list.The fresh audit checks80 actual theorem bodies/11 definitions in its stated module scope, with81 nonempty diagnostic traces, complete standard-three axiom closure and the unchanged producer guard. It explicitly records the legacy parent-construction boundary. Node counts54777/32815/966, exact/one-below budgets, caller assignments and full metavariable restoration, valid-graph wrong-sign/wrong-polynomial controls, empty-graph refusal and forged-context preflight are checked. Three fresh isolated Opus reviews completed; substantive findings were fixed before green merge. The initial copyright CI failure was corrected with an immutable
.lean.txtarchive rename and actual tracked-file metadata results, not by weakening checks. No general performance or physical-sharing claim is made.Independent continuation is committed locally at
b22ca86d55and is being strengthened after a fresh Opus review; it is not landed or pushed into10976. It generates ordered coefficient selectors and uniqueness, full finite-reader/source authentication and counterexamples, plus an actualQAdjoincoordinate/presentation assembly. A public-module rational-root quotation and exact original header-binding proof now pass using existing APIs (Dag.descriptor_rawand a checked direct binding reader), rather than private-import construction. The remaining full-signature codec boundary is separate. New native regressions use both computed coordinates and two original closed guards at one reader. Full validation/review of that continuation is still underway; no general tactic completion is claimed.Remaining full scope: generic original-source/provider/predecessor and frozen-context assembly, general tactic quotation and accepted algebraic completeness, remaining conversion/joint realization integration, strict compiled arbitrary-missing-record rejection, native inverse/xgcd stress and the remaining required conformance/manual/runtime evidence. Existing owner requests remain on10378, including the public full-signature encoding/decoding bridge. #10633/#10634 artifacts are preserved. No owner proof, issue, worker or downstream dispatch is duplicated;10331 retains dispatch. Own Lean/Lake/browser work remains serial under hard aggregate32GiB/no swap/two Lean threads.
kim-em commentedon Oct 17, 2026
PR #10977 is MERGED as squash
e0faead2f34b3b4379dd1c0ca0cfa1f2b1a2a43f, from reviewed head185e98ba0d7b0780af49ddfca01655868057c123, at 2026-10-17T11:51:55Z. Its tree exactly equals the reviewed head:e75e9d2133557aa59d9e7fa70cf33df83d277c13. CI39022375748, job117366621570, completed SUCCESS, including conformance, architecture experiments, the full manual, benchmark smoke and oracles/BZ gates. The resumed same-run watcher exited0; observer API403 errors never caused a CI rerun. Exact-head squash auto-merge omitted branch deletion. Remoteissue-10358is verified retained at185e98; #10358 remains OPEN and assigned.Landed artifacts:
SourceSelection.lean: ordered inherited/root/earlier-coordinate selectors, real/formula correspondence, uniqueness and full finite-reader source authentication. The native existential and independent false-universal consumers retain original matrix, coefficient, domain, sample and guard ties.FieldSelection.lean: actualRoot.toCanonical/QAdjoincoordinate and presentation assembly. The plain shifted-matrix point theorem concludes atpresentation.model.value sampleand preserves original guards. Factory conformance executesNumberField.present?; the sample is distinct from the generator.conformance/HexRCF/SourceSelection*.leanmodules,FieldSelectionConformance.lean,NativeSelectionOrderedConformance.lean, positive/negative checked root headers,conformance-fixtures/HexRCF/source-selection-negative.json, and its existingscripts/rcf/selected_literals.pygenerator. Controls include selector-only swaps, inherited origins, nonintegral coordinates and both selected roots of X²−2. The negative header deliberately uses interval-only selection, without a derivative word.NativeSourcesmanual chapter; and the source-selection report.The scoped fresh audit rechecks272 theorem bodies/97 definitions across nine named modules, with336 nonempty diagnostic traces, the unchanged producer guard and complete standard-three axiom closure. The report explicitly distinguishes its pre-existing parent-construction boundary. Source-bound verification passes for207 artifacts/23 committed sources, including byte-for-byte native-Repr conversion of the negative fixture. Fresh Opus findings were addressed before green merge. All eight final desktop/narrow captures were inspected. These are validation/provenance observations, not general scaling, speedup or physical-sharing claims.
An independent, unshipped continuation, outside10977, now kernel-checks a public-module canonical sign packet for the nonconstant query X at the selected cubic root. It transports trailing proofs of dependent matches using equality elimination; one/nested cases, caller-state restoration, exact/one-below budgets, charged decline, wrong-proof and terminal-failure controls pass. Its full-private fresh-body audit hit a kernel timeout; tracing identifies a costly generated
checkMomentcongruence checkpoint. That continuation remains scratch until the cost and audit are resolved. It retains closed signature-encoder expressions, so it does not discharge the separate fully frozen-literal encoding bridge requested from10378.#10358 stays OPEN for generic original-source/provider/predecessor and frozen-context assembly, complete-cell tactic quotation and the accepted algebraic-completeness integration, remaining conversions/joint realization and required conformance/manual/evidence. Strict compiled arbitrary-missing-record rejection and native inverse/xgcd stress remain existing10378 owner requests. #10633/#10634 artifacts are preserved. No owner proof, new issue, worker or downstream dispatch is duplicated;10331 retains dispatch. Own Lean/Lake/browser work remains serial under hard aggregate32GiB/no swap/two Lean threads.
kim-em commentedon Oct 17, 2026
PR #10978 is OPEN at
3b65efefa81e76a9f14db586db244b1c42d66fec, with implementation commitbaefcc39c32dec8ed1e6014f00d536997a9d5746. It is not landed. The earlier head passed CI; current exact-head run39043564986 remains in progress. Observation hit the shared REST quota and resumed the same run after reset; no CI rerun was requested.The tranche quotes a public nonconstant X sign packet at the selected root of X³−3, decodes a coefficient using its new fact alone, and proves its ordinary real value and positivity. Completed fresh Opus findings led to abstract-major transport, separately checked moved proofs, independent-data support, literal-Boolean callback bypass, and canonical-codec context conversion with dependent helpers. A two-codec counterexample caught native sign/query production when only one codec value was abstracted; abstracting the constructor removes those reductions. Permanent fresh actual-body audits pass: public packet656theorems/67definitions/713traces, synthetic dependent readers114/14/64, actual-codec readers61/4/56, complete transitive standard-three axiom closure and unchanged producer guard. Affected integration, rational compatibility, all refusal/restoration controls, full manual/HTML, four inspected desktop/narrow captures and metadata pass. The current record verifies67artifacts/40committed sources; the earlier source-bound record is preserved. An attempted third Opus pass hit Claude's weekly limit and is explicitly not counted as a completed review.
Independent continuation now reconstructs a new root and raw header from the exact original reader, using
RootReplay.readDescriptor_subjectand an independently quoted subject reader. A new packet and coefficient/value proof consume that generated binding without the fixture's handwrittenroot_raw,subject_readornativeRoot_read. Its fresh importing prototype audit665theorems/65definitions/720traces, header exact/one-below budgets and malformed-reader restoration, and five packet mutation controls pass. This is unshipped scratch, outside10978, not a second PR or full tactic closure.#10358 stays OPEN for generic original-source/provider/predecessor and fully frozen-context assembly, complete-cell tactic quotation and accepted algebraic completeness, remaining conversions/joint realization and required evidence. The fully numerical signature bridge, strict compiled arbitrary-missing-record rejection and inverse/xgcd stress remain existing10378 owner requests. Current10967 is still open; no unmerged API is claimed. #10633/#10634 artifacts are preserved. No new issue, worker, owner proof or CI job was introduced;10331 retains dispatch. All own Lean/Lake/browser work is serial under hard aggregate32GiB/no swap/two Lean threads, with observed current integration/render/browser peaks2.4/3.2/6.7GiB.
kim-em commentedon Oct 17, 2026
Landed #10978 at squash
e92beebc18c626ad94d0e64791b23239cdfdb9bbafter exact-head CI39043564986/job117427713684 completed successfully for3b65efefa81e76a9f14db586db244b1c42d66fec. Merged usinggh pr merge --squash --auto --match-head-commitwithout--delete-branch;issue-10358remains present. Shared REST quota failures resumed observation of the same run; no CI rerun was dispatched.Exact landed artifacts: RootQuote, public packet and selected-real value, actual-codec dependent readers, their fresh body audit, manual, and source-bound evidence. Three declared fresh-body scopes check656/67/713,114/14/64 and61/4/56 theorem/definition/nonempty-trace inventories, complete standard-three axiom closure and unchanged producer guards. Rational compatibility, nested and continued branches, multiple proofs, independent/genuinely dependent data, exact/below budgets, caller rollback, wrong proofs and five actual packet mutation controls pass. Two completed fresh Opus reviews were addressed; the attempted third pass hit Claude's weekly limit and is not counted as a completed review.
Independent continuation remains unshipped:
RootHeader.quoteWithderives raw-header binding from the original root reader and independently parsed subject; local commits956cd622c7e67fac0de51aea73cbe1b14604d757/43a3701c4e413321614743b5179d03fe902b087fretain46artifacts/51sources and a665/65/720 audit, avoiding old fixture header/reader identities. Further uncommittedRootContext.packWithassembles the actual native child through existing owner constructors, with exact signature,2653-node exact/below packing budgets, wrong-parent rollback, ordinary-model value/positivity and a673/67/730 fresh audit. New packing bodies also exclude root-data serialization and graph encoding. Its frame is still a serialization expression, not a frozen numerical history. Model construction is checked separately from the reported packing budget. These changes have not entered another PR and will be reconciled with the actual squash before delivery.#10358 stays OPEN and the full goal stays active for generic original-source/provider/predecessor and fully frozen-context assembly, complete-cell tactic quotation and accepted algebraic completeness, remaining conversions/joint realization and required conformance/manual/evidence. Existing10378 requests cover the public full-signature literal/encoding bridge, strict compiled arbitrary-missing-record rejection and inverse/xgcd stress;10967 was still open at the last check. They are not universal barriers to independent work. #10633/#10634 artifacts remain preserved. No new issue, worker, owner proof or CI job was introduced;10331 retains downstream dispatch. All own Lean/Lake/browser work remains serial under hard aggregate32GiB/no swap/two Lean threads.
feat(rcf): prepare reconstructed root contexts for quotation
test(rcf): retain reconstructed-root quotation evidence
feat(rcf): transport functions with proof inputs during quotation
test(rcf): retain proof-input transport validation
fix(rcf): quote public replay tree equations
test(rcf): retain public tree quotation evidence
kim-em commentedon Oct 19, 2026
Merged prerequisite update for #10358 / #10331: PR #10967 landed at
0738244bdda275a1273fc28a444cabc424dcf71e, usinggh pr merge --squash --auto --match-head-commit d8fdc8fb0349a3c174c33ddb80a27322fed5aafcwithout branch deletion. The recorded fresh Opus review found no blockers; the rebased head preserved the reviewed code except the documented checker-allowlist reconciliation. Exact-head CI run 39175085494 is confirmed completed/success, with its build job successful and no failed or cancelled steps. This was an existing reviewed prerequisite PR, not a new issue or dispatch.The artifact exposes
NumberField.Presentation.model_eq; the actual adapter'sNumberField.model_readconsumes it through ordinary imports.import all HexRealClosureTheory.NumberFieldToweris removed and the existing DAG checker seals that owner boundary. The equation, consumer proof and native interpretation remain ordinary-kernel checked; no model/arithmetic/search algorithm is changed.The continuing worker integrated current main without conflicts at local merge
e928d26d22ba0468004056542084eb7158778a9a. The actual owner module, NumberField consumer, native algebraic-cell regressions, original-source preparation/acceptance conformance and optional umbrella pass together: 11,169 Lake jobs with cached dependencies reused, 5min9.528s, peak 5.2 GiB/no swap, under the serial hard 32 GiB/two-thread cap. The preparation checks include original zero guards, false/empty-domain sources, ordered irrational/guard-only inputs, aggregate budgets, forged inventories and transactional refusal. A full current manual/fresh source-goal audit is still running; it is not yet claimed complete.This removes the private presentation-model boundary from the remaining gates. It does not supply numerical canonical-frame encoding, arbitrary frozen history/operation-record discovery, general joint finite replay realization or full automatic tactic integration. #10984 is still unmerged and its mandatory Opus review remains pending; general #10378 exporter obligations remain. #10358 stays OPEN. Existing draft #10981's source/goal work remains unmerged pending its actual fresh Opus review and final-head green. No owner proof copy, new issue/PR/worker or downstream dispatch; #10331 retains coordination.