Skip to content

Implement BKR/Thom sign determination and checked replay #10377

Closed
Closed
Implement BKR/Thom sign determination and checked replay#10377
Assignees
kim-em

Description

@kim-em
kim-em
opened on Sep 21, 2026

Mathematical task

Given a squarefree polynomial P and an ordered list of polynomials Q₁,…,Qₛ over an ordered field, count the roots of P in a specified interval having each possible sign pattern of the Qᵢ. This is univariate BKR sign determination.

For example, for P=x²−1 and Q=[x,x−1] on the whole line, one root has signs (−,−), one has signs (+,0), and every other pattern has count zero. A complete sign table must justify those zero counts as well as the patterns it lists.

Also identify and order individual roots using signs of derivatives of their defining polynomial: these are Thom encodings. Supply the algorithms, independently checkable records of their calculations (certificates), proofs of correctness in the Mathlib companion, and the specified performance evidence. This is the library assignment under #10331 for #10143. The user-facing tactic belongs to #10358; this issue does not implement quantifier elimination.

The contracts are hex-sign-det, hex-sign-det-mathlib, and the shared execution contract, revised by merged PR #10365.

Current assignment and examples

Continue the existing sign-determination implementation; do not restart the
initial tactic demonstration. The shared query semantics (#10521), finite BKR
correspondence (#10530), and Thom completion/identity/order/re-encoding (#10547)
are proved. The required foundation is present in the current Tau Ceti pin.

This issue alone owns BKR/Thom algorithms, certificate formats, correspondence,
direct API examples and independent library conformance. #10358 alone owns the
rcf integration and its manual examples. #10378 owns tower consumers and
samples. Supply the merged upstream APIs those workers need; this issue's
closure does not wait for their tactic/tower integration or manual PRs.

Direct library tests must still cover actual nonquadratic QAdjoin coefficients,
independently constructed common fields with selected embeddings preserved,
noninjective representations and infinitesimal fields. These are generic
coefficient fixtures using existing libraries, not an import of the tower or
a second number-field implementation. Merged #10550 supplies common-field
examples. Tactic-specific examples consume these APIs under #10358.

Required algorithms and proofs

  • Complete sign tables. Use the shared prepared Tarski queries and existing rational matrix, rank and row-reduction libraries. Fix the order of queries, rows and columns. Return exact nonnegative integer counts, including empty query lists, zero polynomials among the Qᵢ and domains containing no roots.
  • Justified removal of sign patterns. In the BKR recursion, prove that every pattern occurring at an actual root remains among the candidates. Include the child calculations and the argument that their complete tables cover the parent's possible patterns. An invertible submatrix and an equation M*c=t establish a solution on the chosen columns; they say nothing about omitted columns. The checker must validate both the matrix calculations and why omitted patterns cannot occur.
  • Root identity and order. Validate squarefree defining polynomials and partial/full Thom encodings. A validated descriptor must select exactly one root. Implement completion, equality, ordering and the sign of another polynomial at that root. To compare roots of different polynomials, express their identities using the specified common squarefree polynomial and prove that the selected roots are unchanged.
  • Correct interpretation of stored coefficients. Reuse ordinary total arithmetic, natural-number casts and an explicit sign operation. Zero has one stored representation, but other values may have several. Test mathematical polynomial identities by zero differences. Retain exact equality for integer/rational matrix identities and for bindings to the particular stored polynomial, interval and coefficient context.
  • Reject mismatched evidence. Derivative signs copied from another polynomial do not identify the same root. After a defining representation changes, reject old descriptors and child certificates unless an explicit checked conversion justifies their use, even if some stored operands look unchanged.
  • Correctness of the actual code. Prove the finite linear algebra and induction on the possible sign patterns, then relate the implemented calculations and accepted certificates to mathematical roots and signs. Use the required Tau Ceti Thom/BKR results through the companion library.
  • Interfaces for other libraries. Provide the specified root/sample operations for real-closure arithmetic, CAD and coverings. Do not implement those clients here or import the real-closure tower into this library.
  • Independent verification. Independent root/sign comparisons, deliberately invalid/incomplete-support certificates, ordinary Lean-kernel correctness examples, and the final coefficient-field conformance are delivered, including Retain independent direct BKR and Thom conformance #10775.
  • Performance evidence. The reviewed report and retained measurements are delivered by Summarize BKR/Thom performance evidence and qualify timing claims #10808, with rational/nested operand diagnostics (Record intermediate rational coefficient sizes in small BKR comparisons #10825/Record small nested BKR coefficient operand sizes #10826), the proved denominator-one optimization and controlled comparison (Skip trivial rational-function gcds and check interacting BKR workloads #10835), and complete small maximal-support workflows. The report preserves inconclusive results and gives their evidence-based dispositions and coverage limits.
  • Final Phase-4 attestation. Complete BKR/Thom Phase-4 attestation #10861 records HexSignDet and HexSignDetMathlib through Phase 4 after the prerequisite readiness delivered by Complete Sturm and real-algebraic prerequisite readiness for the real-closure family #10577/Complete Sturm and real-algebraic Phase-4 prerequisite readiness #10860, with the actual direct dependency records, retained evidence, ordinary-kernel proof roots and required CI verified.

Completion

All algorithm, correspondence-proof, certificate-interface, direct-library-example and independent-conformance work owned here is delivered. The compiled performance evidence is consolidated in reports/sign-det-performance.md, merged through #10808. #10825 and #10826 supply scoped intermediate-coefficient diagnostics; #10835 supplies the proved denominator-one shortcut and its retained controlled comparison. Original inconclusive observations and their supported dispositions remain retained.

#10577/#10860 supply prerequisite Sturm readiness. #10861, merged as 112de5a94de8598e6a3fc8c2b48bbd09df1547c8, verifies direct dependency eligibility and records HexSignDet and HexSignDetMathlib through Phase 4. Full CI passes on final head 47a81d0f565a25db90b3e5f4d7618f8a8e762195, including actual library/conformance builds, benchmark verification and independent oracles. Its final required CI passes; independent Opus reviews identified no owned implementation blocker, and all substantive findings are addressed. An optional recheck of the final documentation-only corrections was unavailable because Claude reached its weekly limit; no review verdict on that last head is claimed. The local proof/library build, all 34 benchmark verification cases, all 33 coefficient-field API checks, evidence regression tests, archive reconstruction, import and admission audits pass. The report retains finite-range and memory-accounting limits; the attestation asserts no general practical high-degree or arbitrary tower-depth claim.

There is no remaining algorithm, proof, certificate, direct example, conformance or Phase-4 obligation owned by this issue. Actual Tau Ceti Thom/BKR foundations are consumed, and the former #10389 admission is removed. Tactic/manual integration remains with #10358, tower consumers with #10378, and integrated acceptance/publication with #10575; these do not block this issue's closure.

Upstream follow-up #10863 tracks avoidable repeated zero/one construction in nested rational-function arithmetic; #10864 reopens its performance attestation. Neither arithmetic owner is a declared dependency of HexSignDet. The source recurrence describes that cost and is not a claim that it has been optimized. Remaining manual-consumer interpreter/caching work stays with #10635; the per-sign canonical conversion was removed by #10641. These findings are not hidden or transferred into an extra BKR implementation gate.

Earlier delivery notes below describe individual PRs; their then-outstanding work is superseded by the completed deliveries above.

Dependencies and remaining interfaces

#10375 supplies the shared computation and algebraic correctness results. The prepared polynomial/interval interface was merged in #10385. Use the particular merged functions and theorems needed for each step; #10375's completion does not establish the general root-sum theorem.

#10389 is complete through merged PR #10521. HexRealRootsMathlib.Tarski.check_rootSum now proves the original arbitrary-certificate statement over ordered real closed fields, including noninjective coefficient representations and finite/infinite endpoints. Its proof uses the pinned Tau Ceti Sturm–Tarski foundation; the former admission is removed. Use this proved bridge without changing its meaning or duplicating the computation.

The current Tau Ceti pin 0dbbe255a4f418084b30a3ffe6763d824a6b4250 supplies finite BKR foundations in TauCeti.Geometry.RealAlgebraic.SignDetermination: matrix identities, inversion of full ternary moments, and recovery of sign counts from an inverse plus independently complete candidate support. Merged PR #10530 connects the actual Tau Ceti finite counting and count-recovery theorems to the implemented matrix checks and BKR replay induction, with candidate coverage supplied independently of matrix rank. The pinned Tau Ceti revision 0dbbe255a4f418084b30a3ffe6763d824a6b4250
supplies Thom identity/order and derivative count reconstruction. Merged #10547
connects those proofs to the actual completion, root identity/order and general
re-encoding algorithms. The separate foundation gate is discharged; do not
repeat that work or wait for the broader roadmap.

Merged #10548 proves success, completeness, uniqueness and sorting of the actual
root-list producer over valid domains, including nonzero constants and
finite/infinite endpoints. Merged #10549 supplies total common-polynomial
comparison. Merged #10550 supplies independent common-field examples against those proofs,
including selected embeddings in quartic and cubic coefficient fields.

Merged #10581 supplies selected-root sign checking from supplied same-level
shared graphs, exact acceptance/rejection and finite coefficient-sign transfer
proofs, mathematical selected-root value correspondence and adversarial
ordinary-kernel/byte examples. It does not discharge cross-level evidence. JSON byte-roundtrip laws are now supplied by #10598. Merged #10582 reconciles the representative proof
roots with CI while retaining all inexpensive correctness checks and measurement
integrity checks. Merged #10588 adds operation-scoped allocation capture with
explicit coverage limits. Merged #10589 retains 55 joint-family allocation captures;
these do not complete wider allocation families, live memory or the inconclusive
timing requirements. Merged #10590 proves a total integer-only JSON byte backend
and independently checks it; the actual certificate-codec integration is supplied by #10598. Merged #10594 supplies proved iterative byte parsing/printing and the retained native capacity checks; it does not establish combined depth/width memory bounds. Merged #10605 retains 30 operation-scoped matrix solve/check allocation captures, with exact callback and binary bindings. Cross-level evidence, wider allocation families, live memory and the remaining timing requirements are still open.

Merged #10598 integrates the proved integer-only JSON type into the actual coefficient, context, evidence and graph codecs. Its byte-roundtrip proofs preserve exact context and subject bindings. The regenerated isolation fixtures and independent oracles pass. The ordinary algebraic coefficient decoder still recomputes signs; this does not finish shared replay across successive coefficient fields.

Merged #10608 supplies 42 operation-scoped allocation captures for coefficient-height growth, with input, binary and callback bindings and retained native/GMP attribution. Together with the joint and matrix captures, this records allocation traffic for those measured operations. It does not measure peak live memory or finish the remaining performance families and timing analysis.

Merged #10578 supplies selected-root naturality requested by #10378: for a
strictly monotone field embedding between real closed fields, checked conversion
preserves the selected mathematical root and its Thom encoding through the
shared coefficient interpretation interface. Do not duplicate the tower here.

Merged #10754 completes the dependency-envelope byte proofs and checked
selected-root certificate reader. #10758 supplies the generic coefficient
fact reader. #10764 supplies ordinary, in-process Lean-kernel proof assembly
and intermediate fact collection across exact typed coefficient contexts.
Missing evidence stops at its actual context and polynomial; supplied facts
are kernel-checked before reuse. Shared facts preserve their full literal
bindings. Caller context and tower-catalog reconstruction remain with #10378.
This interface introduces no arithmetic worker process and does not claim
that native coefficient arithmetic avoids every lower-level computation.

Merged #10775 supplies final independent library conformance, including actual
nonquadratic QAdjoin values, independently constructed common fields,
noninjective representations, infinitesimal fields, adversarial replay and
parser mutations. The algorithms, totality/correspondence proofs, certificate
interfaces and direct library examples are delivered. The remaining work
owned here is the compiled Phase-4 evidence and justified phase attestation.
#10768 supplies retained whole-process memory observations with explicit
resident/mapped-page distinctions; it does not supply live-object accounting
or settle inconclusive scaling results. #10773, #10771, #10776 and #10779
track the current nested-sign, wider joint, wider matrix and nested-table
performance work. Preserve all completed samples and resolve the findings
without changing models to fit observations.

Matrix/rank libraries remain inputs. Their separate Phase-4 obligation #10352 is complete through merged #10584 (8b129a0ff5dde24137f8697d03675902ecf1bda6). The merged source contains the proved native checking changes, the retained checker/comparator/profile evidence, and Phase-4 attestations for HexRank and HexRankMathlib. Reuse those inputs; do not wait for or repeat the rank campaign. They do not establish this library's own performance requirements. Coefficient facts come through the shared interpretation interface, without importing the tower implementation.

Scope and delivery

This combines #10341 and #10346. Close it only when all work owned here, the direct library examples and required performance evidence are delivered, including actual use of the required Tau Ceti foundations. Direct library examples belong here; the rcf manual belongs only to #10358. The former #10389 admission is already discharged. The required Thom foundation is now used by #10547. Do not close #10377 while any required algorithm, proof, direct library example or performance requirement is outstanding; retain the proved guarantees and introduce no new admission. Partial PRs use Refs and list what remains.

If a requested statement is false or an essential mathematical implication is missing, report concrete evidence here and seek correction. Do not invent field instances, use fallible arithmetic records, duplicate query algorithms, weaken theorems, or count placeholders as finished proofs. HexInterval work, new CI jobs and release publication are outside scope. Immediately after opening each PR, request Claude Opus review using $second-opinion while CI runs. Address substantive findings, failures and conflicts, discuss substantial architecture changes with the user, and merge green with gh pr merge --squash --auto without --delete-branch. No automatic worker launch is requested.

Evidence policy and final integration

Follow current PLAN/Phase4.md: representative CI-built ordinary-kernel
certificate/tactic examples and axiom audits for the proof track; no mandatory
sweeps of ordinary theorem applications. Targeted proof-cost comparisons must
answer a concrete replay/quotation/sharing decision or observed bottleneck.
Keep all compiled scaling/comparator/profile obligations and retained evidence.
Final family acceptance and split-package preparation are tracked separately
under #10331; they do not transfer any missing sign-det algorithm or proof out
of this issue.

Phase readiness

#10577 owns prerequisite Sturm/real-algebraic phase readiness; #10352 owns rank
readiness. This issue owns HexSignDet and HexSignDetMathlib phase attestation
through Phase 4 once their prerequisites are satisfied. #10575 owns final
integrated acceptance and subsequent family proof/API/documentation finishing.
These phase requirements do not prevent supplying the already-supported
naturality/enumeration/comparison APIs to the #10378 worker now.

Merged #10582 delivers the representative CI-built proof examples and moves
optional diagnostics out of the declared proof roots. It preserves the retained
measurement integrity checks and useful correctness cases. The expensive
depth-three diagnostics remain a separately named manual-only target; they are
not a required CI proof root. Other proof/API/compiled-performance requirements
still need their own attestation.

Activity

  1. kim-em
    marked this as blocked on Sep 21, 2026
  2. kim-em
    marked this as blocking on Sep 21, 2026
  3. kim-em
    self-assigned this
    on Sep 22, 2026

  4. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    Claimed; implementation branch: issue-10377.

    The first reviewable tranche will implement the finite BKR replay boundary in HexSignDet: integer moment matrices and scaled left-inverse checks, complete leaf support, recursive child-product validation, exact counts/zero pruning, retained row-basis validation, and shared HexSturm query replay. It will include adversarial omitted-support tests and ordinary-kernel finite-algebra proofs. It will use Refs, not close this issue.

    Placement audit:

    1. SPEC hex-sign-det, “Moments and complete support certificates” and “Headline theorems and proof ownership”: “HexSignDet proves finite matrix identities/uniqueness, literal replay checks, structural termination, and support induction conditional on abstract moment, query and Thom contracts.” Files belong in HexSignDet/; no tower imports.
    2. This tranche uses existing Mathlib-free HexMatrix operations and their algebraic laws; no Mathlib structures are needed. Later mathematical matrix/root correspondence belongs in HexSignDetMathlib.
    3. Existing source inspected: HexRank/Cert.lean (RankCert, checkRank, right inverse on a selected minor), HexRank/Check.lean (determinantal soundness), HexRowReduce/Solve.lean (exact solving), and HexRankMathlib/Sound.lean (rank interpretation). The replay will check its scaled left-inverse identity directly, as permitted by the SPEC, without assuming the rank certificate's order/orientation matches.
    4. HexSturm/Basic.lean provides certifyPrepared and literal check; it does not yet provide generic root-sum soundness. Prove Sturm–Tarski root semantics after the Tau Ceti foundation #10389 remains that precise proof gate. The independent Thom/BKR foundations and all producer/descriptor/Phase-4 obligations remain open here; this first tranche will not claim semantic root correctness or performance completion.

  5. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    Merged #10397 as the first replay tranche. HexSignDet now checks fixed leaf supports, complete child Cartesian products, integer moment systems and zero pruning, exact context/domain/query-list bindings, retained row bases, and shared HexSturm query evidence. Finite proofs establish integer-solution uniqueness, positive-coordinate retention, elementary child-product membership, and that every accepted tree reaches checked Tarski evidence.

    Regression coverage includes leaf and internal-node omitted-realized-support forgeries whose local systems pass, same-size row/column permutations whose local equations remain valid, zero/empty cases, stale bindings, and ordinary-kernel acceptance/rejection probes with guarded axiom inventories. Full local build, targeted conformance and PR CI passed. No phase was advanced (done_through: 0).

    This does not close #10377. Remaining work:

    • Total production sign determination and the full small-case reference solver, opaque complete sign tables, reduced moment chains, tensor/retained-row-basis existence and producer integrality/nonnegativity exclusions.
    • Squarefree root descriptors, validated partial/full Thom encodings, completion, ordered roots, sign/equality/order, common-product comparison, re-encoding, and the sample-point interface.
    • Full conditional support induction and companion correspondence for the actual algorithms. Generic query/root-sum and arbitrary-certificate semantics still consume Prove Sturm–Tarski root semantics after the Tau Ceti foundation #10389; the separately specified BKR/Thom foundations need actual delivered declarations, not roadmap closure. No replacement soundness premise was introduced.
    • Serialization, nested evidence DAGs and supplied coefficient-proof replay, full immutable context/refinement fixtures, and checked transport. The present tree repeats and rechecks head squarefree evidence per moment; shared domain replay and its measured costs remain explicit integration work.
    • The full independent FLINT/real-algebraic/Z3 root/sign oracle suite and required Phase-4 runtime, ordinary-kernel proof-cost, scaling/comparison and attribution evidence. Current regression tests and CI smoke checks do not supply those gates; Complete hex-rank Phase-4 benchmarks and performance evidence for certified row selection #10352 remains its separate rank-performance obligation.

  6. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    PR #10400 adds prepared-query BKR certificate construction and full finite support induction. It constructs balanced trees from Tarski moments, solves with existing rational inversion/rank code, checks integrality and nonnegativity before extracting integer counts, and returns independently accepted replay. The exponential ternary constructor is a small-case reference only.

    count_moments proves the actual finite counting identity on complete candidates. Replay.support_complete establishes child-to-parent coverage and exact counts by induction on the checked tree; Replay.support_iff rules out both missing and spurious positive conditions. Their explicit remaining hypothesis is moment interpretation over one finite observation family, restricted to the actual query positions. Deriving that hypothesis from roots consumes #10389 and is not claimed here. Axiom audits report only the standard kernel axioms.

    Full local build, targeted conformance and structural checks passed. Opus review and CI are running. The diagnostic constructor is not yet the specified total determinePrepared API: producer completeness, tensor/retained-row-basis existence, complete opaque table API, reduced moments, Thom/sample-point operations, serialization/shared evidence and coefficient-proof replay, companion root semantics, full independent oracles and Phase-4 evidence remain open. No phase advancement or issue completion is claimed. Reduced-moment work is proceeding independently while this PR is reviewed.

  7. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    PR #10400 is merged as 752d0f1 after successful CI and an independent Opus review plus follow-up. It adds prepared-query BKR construction, the exponential reference, finite actual-count moment identities, and recursive support/count induction over accepted replay. Its explicit finite moment interpretation contract is not the root-sum bridge.

    PR #10401 now adds reduced-moment construction and arbitrary-certificate replay, with algebraic companion proofs of producer acceptance and sign preservation at every root under the shared noninjective coefficient interpretation. Full local build, computational/companion conformance, and ordinary-kernel axiom inventories pass. Claude Opus review was launched immediately after opening the PR while CI runs.

    The next local tranche proves full column rank after pruning, correctness/order/left-inverse properties of the actual retained rank certificate, exact tensor-product ordering and inverse composition, and acceptance of integer scaled-inverse solving. The tensor constructor integration passes current conformance; this work is saved separately from #10401 and has not yet been independently reviewed or merged.

    Remaining gates stay open: total determine/SignTable APIs and complete producer correspondence, full tensor/basis integration and conformance, Thom descriptors and selected-root/root-order/re-encoding/sample-point operations, shared/nested evidence and serialization, complete independent-oracle conformance and Phase-4 evidence. Full semantic proofs require #10389 and the separately specified Tau Ceti Thom/BKR foundations. No proof or performance phase is advanced by builds, fixture tests or metadata checks.

  8. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    PR #10401 merged as a260c1e after successful CI and independent Opus review. It supplies checked positive-scaled moment reductions, algebraic producer acceptance and arbitrary-accepted-reduction sign preservation under noninjective coefficient interpretation, with ordinary-kernel probes and identity-consistent scale forgeries.

    PR #10402 now adds tensor composition of child inverses, exact integer solving, retained-basis/rank/order proofs, and initial query reductions reused throughout the balanced construction. Its finite replay proofs cover child slices, query lengths, degree bounds and the actual Tarski operand signs. The independent conformance harness checks 59 rational cases against pinned FLINT qqbar and the existing real-algebraic API, including complete sparse counts and malformed-support tests. Full local build and conformance pass after rebasing; a fresh Opus review is running alongside CI.

    This issue remains open. The outstanding gates still include total producer completeness and the public table/descriptor operations; shared domain checking, finite-DAG serialization and nested/refined contexts; Thom completion, root order, sign-at-root, common-product comparison, re-encoding and sample-point interfaces; the root-sum/replay bridge in #10389 and the separately required Tau Ceti Thom/BKR foundations; descriptor/extension/infinitesimal conformance; and the full Phase-4 runtime, proof-cost, comparison and profiling evidence. #10352 remains a separate rank-performance obligation. None of the local builds, fixtures or CI benchmark smoke checks is claimed as a semantic proof or Phase-4 gate.

  9. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    #10402 merged as 6342f46131a7ae26a44dbefe343b6806f240f69c after green CI and independent Opus review. It adds shared query preprocessing, reduced-query degree bounds, and the actual retained-basis/tensor-inverse correspondence.

    #10403 is open and under fresh Opus review while CI runs. It implements checked partial/full Thom descriptors, sparse tables, completion, root lists, selected signs, common-product comparisons and re-encoding. Companion proofs cover formal derivatives, accepted root-union identities, finite endpoint constraints, the actual rational solver, complete leaf systems and parent systems derived from complete child supports. The rational proof uses the core rank API at the executable Rat instance; it does not assume equality with Mathlib's separate field dictionary.

    Local validation: full lake build (14662 jobs), both conformance targets and emitter, ordinary-kernel axiom guards, and the actual filtered oracle harness (101 exact cases, 15 adversarial Python tests, no failures). Source/DAG/registration checks and existing performance-data freshness pass. These checks do not establish the outstanding semantic or Phase-4 gates.

    Remaining gates:

    The issue stays open, and work continues across PRs. Section/sector samples and tower enlargement remain owned by real-closure as specified; this library supplies their root identity/order/sign operations.

  10. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    #10403 merged as bf6aa48 after green CI and an independent Claude Opus review. It provides checked partial/full Thom descriptors, completion, selected signs, root ordering, common-product comparison and re-encoding, with explicit remaining semantic/totality gates.

    #10404 is open for the next tranche: actual producer replay acceptance under the generic coefficient interpretation laws, finite node assembly from checked systems and actual prepared-query values, and full-root extraction sharing one checked table. Its full local build, ordinary-kernel probes, axiom checks and 101-case independent rational oracle suite pass. A fresh isolated Claude Opus review is running alongside CI. This PR proves producer acceptance, not unconditional producer success or arbitrary-certificate root semantics.

    Independent work continues. Separate local commits add 26 exact infinitesimal cases checked against pinned Z3 RCF (including the corrected de Moura–Passmore example and two coefficient levels), and typed topological BKR graph replay with checked earlier-node references and ordinary-kernel probes. These commits are not included in #10404 and are not yet merged or independently reviewed.

    Outstanding gates remain: general finite producer completeness and domain-exact total APIs; the #10389 root-sum/arbitrary-certificate semantic bridge and separately required Tau Ceti Thom/BKR foundations; shared domain verification inside query evidence; byte decoding, lower-level coefficient-sign edges and tower-generated/nested proof integration; final total sample-consumer interfaces; and the full Phase-4 runtime, proof-cost, comparison and profile evidence. Typed same-level graph replay and infinitesimal test providers do not discharge those downstream proof/serialization gates. Compilation and oracle agreement are not substitutes for the missing proofs or performance evidence. #10352 remains the separate rank-performance obligation. This issue stays open.

  11. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    PR #10404 now includes the independent-review fixes at 76572c3: shared preparation decisions, public root-list producer proofs, and the exact parent matrix adapter. Full local build and conformance pass; CI is running on that head.

    Independent Phase-4 work on the local issue branch now has committed evidence (2327cca21, b8166e5f1, ecd0bfb39): six fixed trials at 64–2048 repeated queries for reduced/direct production, literal tree replay and shared-graph replay. All 144 samples completed, passed independent expected-output and exact-schedule checks, and returned the declared-model consistency verdict. No sample was discarded or rerun. The accompanying timed-region profile passed its diagnostics with 4,526 samples: final replay is 56.74% inclusive, moment-matrix construction 17.83%, and coefficient sign 0.66%; these shares overlap. Raw exports, provenance and profile summaries are retained in reports/data/sign-det-sparse, with the family analysis in reports/sign-det-sparse-model.md. These later commits are not yet part of #10404 or merged.

    This is one sparse-support family, not Phase-4 completion. Remaining evidence includes separate query/product/matrix phases; degree, coefficient/witness-bit, maximal-support, extension-depth and nested-evidence sweeps; adjacent AB/BA comparisons; allocated bytes and certificate bytes; and fresh-module proof evidence. The infinitesimal Z3 conformance and same-level graph checker tranches remain local and still require their own PR review/CI. General producer totality, final total consumer APIs, nested coefficient-proof graphs/serialization and full root/sign semantics remain open. #10389 is still open with its particular Tau Ceti foundation gate; its bridge and the separate Thom/BKR foundations are not supplied by executable tests or these performance observations.

  12. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    Further independent work is committed locally after the #10404 head:

    • Five separate sparse-family schedules now measure prepared queries, reduced moment products, moment matrices, actual solver calls including their system checks, and rational coefficient signs. All 180 additional samples were retained, matched expected outputs, and returned the declared-model consistency verdict. Together with the four earlier schedules, that is 324 validated samples. The phases overlap and are not an AB/BA speed comparison. Sources, complete raw exports and models are retained under reports/data/sign-det-phases and reports/sign-det-phase-model.md. Source-closure patches reconstruct the measured versions after rebases; every archived source hash was checked in a temporary Git index.
    • ThomOrder proves transitivity and reversal directly for the finite comparison algorithm, including sign-shape and literal descriptor guards. The insertion and public root-list sortedness theorems now consume those proofs, removing their caller-supplied comparator-law premises. Full local build, computational/companion conformance and axiom inventories pass. This proves ordering by the executable comparator, not its correspondence with real-root order.

    These commits remain outside #10404, whose latest reviewed-fix head is 0183d25 and whose CI is still running. Remaining gates still include general producer totality, final total consumer APIs, nested coefficient-proof graph serialization and integration, full semantic correspondence through #10389 and the separately required Thom/BKR foundations, all non-sparse performance axes, paired comparisons, allocated/certificate-byte measurements and fresh-module proof evidence. No Phase-4 completion or issue closure is claimed.

  13. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    The ordinary-kernel graph replay measurements are retained locally in commit e906d997d, following the probe implementation in 06d77092b. All 48 adjacent pairs (96 fresh-module builds) completed on the shared host with six rotated rounds and alternating arm order; no samples were discarded and no rerun was used. All eight candidate theorems report exactly propext, Classical.choice, and Quot.sound. Source reconstruction verified all 197 recorded source hashes against the archived patch.

    The family uses accepted and stale-context same-level graphs at depths 1, 3, 5, 7 (query arities 2, 8, 32, 128), fixed rational coefficients and support one. Median candidate-minus-literal overhead ranges from 646.696 to 1196.948 ms for acceptance and 506.164 to 1115.630 ms for rejection. The report retains the full spread and explicitly makes no asymptotic or absolute-time gate claim. Raw compiler outputs, artifact sizes, RSS and all paired measurements are committed under reports/data/sign-det-proofs/06d77092b; reports/sign-det-proof-model.md explains the measured scope and limitations.

    PR #10404 remains under its existing CI monitor; this measurement tranche has not yet been submitted or reviewed. Remaining gates include review/merge of the held implementation and evidence tranches, broad degree/support/bit/extension/nested-proof coverage, adjacent reduced/full and modulo/direct comparisons, descriptor/joint-reencoding measurements, allocation/certificate-byte/peak-bit accounting, shared/nested coefficient-proof graph transport and serialization, general producer totality and final total interfaces, plus the exact semantic bridges from #10389 and the separately required Thom/BKR foundations. This evidence does not close #10377 or those gates.

  14. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    The general same-level graph encoder now uses exact hash consing: every node field, literal context, witness and child reference participates in equality; hashes only narrow lookup. Conformance includes deliberately colliding inverse witnesses, stale contexts, repeated leaves, and a produced tree with repeated internal subtrees. Distinct or invalid evidence is not silently replaced by a cached valid node.

    Dag.replay_encode now proves that encoding any accepted literal tree and running the actual graph checker returns that exact tree with the original caller bindings. The proof follows Encoder.insert and encodeFrom, preserving acceptance of every emitted entry and exact cache bindings. Dag.check_encode gives Boolean acceptance. The new finite proofs use only propext, Classical.choice, and Quot.sound; they do not assume root-sum semantics. These changes are held locally in a5c29f2c8/e2d13d798 pending the current PR sequence.

    Separate general-encoder measurements are retained in 988541fc8 from clean source 5329cec59: all 36 fixed trial-major samples completed on shared-host CPU 88, without a rerun. Exact graph equality returned true throughout. Median time was 0.519 ms at 64 queries and 25.397 ms at 2048; the harness reports consistency with the preregistered s(log₂s+1) model, normalized slope −0.027712, no advisories. reports/sign-det-encode-model.md gives every size and range; raw samples, logs and a hash-verified source archive are under reports/data/sign-det-encode/5329cec59. This measures encoding plus full literal output equality, separately from graph checking.

    Local verification: full lake build (14670 jobs), graph conformance and four new axiom inventories, benchmark build/smoke, dependency/source checks, 58 Mathlib-free bench import closures and 2691 build-only proof probes, and nine benchmark-export validation tests. PR #10404 CI has completed its library/benchmark build and is running conformance under the existing monitor.

    The issue remains open. Review/merge of held tranches, shared Tarski-domain and nested coefficient-proof transport/serialization, the total producer/consumer interfaces, broader Phase-4 support/degree/bit/extension/nested-proof coverage, paired reduced/full and modulo/direct comparisons, descriptor/joint-reencoding measurements, allocation/certificate-byte/peak-bit accounting, and semantic correctness through #10389 plus the separately required Thom/BKR foundations remain gates. This forward encoder correspondence and one-family scaling measurement do not discharge those requirements.

  15. kim-em commented on Sep 22, 2026

    @kim-em
    kim-em
    on Sep 22, 2026
    OwnerAuthor

    Benchmark finding: the full-reference arm of the required reduced/full comparison is inconclusive.

    Outcome: resolve the full-reference performance model against the actual dominant operation while retaining the complete comparison. This is a finding within this SPEC assignment, not a decomposition issue or a completed Phase-4 claim.

    Symptom — declared expectation: runSmallFull s => 27^s, based on dense inverse-identity multiplication for the full 3^s square moment system. The companion comparison arm declares s * (Nat.log2 s + 1). Both use P=X²−1, s copies of X, direct products and the same prepared domain; s=1,2,3,4,5, six adjacent AB/BA rounds.

    Observed result: all 60 arm samples completed and matched the independently checked complete tables. No samples were discarded and no rerun was used. The reduced arm is consistent_with_declared_complexity (cMin=58055.149089, cMax=82326.100911). The full arm is inconclusive (cMin=108.586434, cMax=558.226078); the narrow parameter range uses the harness's multiplicative-range fallback, with no reported slope. The full/reference normalized constant decreases over the ladder: this is a faster-than-declared mismatch, not a passing upper-bound verdict.

    Representative retained full-arm rows (trial 0):

    {"param":1,"inner_repeats":2048,"total_nanos":93855770,"per_call_nanos":45828.012695,"status":"ok","result_hash":"0x97b867a988595d4e"}
{"param":5,"inner_repeats":1,"total_nanos":1571811616,"per_call_nanos":1571811616,"status":"ok","result_hash":"0x652cefb9fbb0489f"}

    Median full/reduced paired ratios at s=1..5 are 0.505, 1.414, 10.936, 126.641, 1704.712. These are end-to-end table constructors, not isolated matrix solves. Raw samples, both unmodified harness summaries, paired values, source reconstruction and before/after source/binary checks are retained locally under reports/data/sign-det-compare/fb98e6554. Source fb98e655470d5b1d8683b4596f87b8cd57da2997, shared-host CPU 40.

    Root-cause hypothesis: cubic integer identity checking is present, but may not dominate this finite ladder. Rational row reduction branches on zero elimination coefficients in a progressively sparse tensor system, and query/rank work has different growth and scalar costs. A timed-region profile of runSmallFull 5 will distinguish these contributions. The model is unchanged pending that evidence.

    Deliverables: retain/report the mismatch; profile and verify the dominant source path; correct the implementation or derive a justified model/protocol from that path, then obtain the required evidence. Both HexSignDet and HexSignDetMathlib already have done_through: 0, so no further phase rollback is possible or necessary. No rollback-only PR will be manufactured. The full comparison performance gate and the broader #10377 gates remain open.

  16. 161 remaining items

  17. kim-em commented on Oct 6, 2026

    @kim-em
    kim-em
    on Oct 6, 2026
    OwnerAuthor

    Merged #10790: Retained complete wider production/replay observations for all four nested-table families, with source bounds and explicit finite-range limits.

    The published head passed CI and independent Opus review; merged with squash/auto and no branch-deletion flag. Other performance evidence and final phase attestation remain open.

  18. kim-em commented on Oct 6, 2026

    @kim-em
    kim-em
    on Oct 6, 2026
    OwnerAuthor

    Merged #10805: Recorded justified Phase-3 readiness for the delivered algorithms, proofs, conformance and certificate interfaces. Compiled Phase-4 evidence and prerequisite readiness remain separate.

    The published head passed CI and independent Opus review; merged with squash/auto and no branch-deletion flag. Other performance evidence and final phase attestation remain open.

  19. kim-em commented on Oct 6, 2026

    @kim-em
    kim-em
    on Oct 6, 2026
    OwnerAuthor

    PR #10835 addresses an actual cost found during the final performance review: rational-function normalization and cancellation recomputed polynomial gcds and exact divisions for denominator-one operands. The new direct branches are checked by the existing reconstruction and Mathlib correspondence proofs; the 3455-job local build passes without new admissions.

    A short controlled LeanBench comparison retained all 24 adjacent AB/BA observations. Identical interacting-infinitesimal callbacks show median within-pair speedups of 3.86× at depth one and 19.41× at depth two, with matching answers in every pair. All four current interacting-field conformance cases pass independent Z3 checks and complete in about 0.55 seconds locally. This is a different source from the older 442-second observation; only the two-level paired collection is a controlled speedup claim.

    The PR also supplies independently checked intermediate-operand observations for interacting reduced/direct/reference tables and actual joint comparison pipelines at degrees 3, 7 and 15. It includes retained source reconstruction, archive checks and mutation tests. Opus review was requested immediately after opening while CI starts. #10825 is a merge prerequisite. The consolidated report and Phase-4 attestation remain outstanding, including the actual #10577 prerequisite gate. No 30–40-hour ladder is planned.

  20. kim-em commented on Oct 6, 2026

    @kim-em
    kim-em
    on Oct 6, 2026
    OwnerAuthor

    Merged #10826 as 87f65c2 after full green CI and independent Opus review.

    The diagnostic records small depth-one/depth-two BKR coefficient operations and normalized operand sizes. Ordinary replay checks the actual polynomial, interval and context; independent input/sign checks and adversarial mutations pass. Archived sources reconstruct from a permanent merged base after squash merges. The report states that these are outer arithmetic observations and do not measure temporaries inside the nested coefficient dictionaries or establish a general growth law.

    The algorithms, semantic proofs and library conformance remain delivered. Remaining integration is #10825, #10835 and the consolidated evidence in #10808, followed by justified Phase-4 attestation once #10577 supplies prerequisite readiness. No larger benchmark ladder is planned.

  21. kim-em commented on Oct 6, 2026

    @kim-em
    kim-em
    on Oct 6, 2026
    OwnerAuthor

    Merged #10825 as f4de50d33fb2f3ae74e826840d148230242f95f2 after Opus review, local verification, and green CI run 37438348740.

    This supplies the small rational arithmetic diagnostic, independent ordinary-result checks, intermediate coefficient observations, and source-bound retained archives. It does not claim general polynomial-chain or nested-field internal bit bounds.

    Remaining delivery: #10835 (proved denominator-one shortcut and interacting-field/joint operand evidence), then #10808 (consolidated performance report and complete maximal-support workflow measurements). Both reviewed heads are already integrated with their prerequisites and remain in CI. Final Phase-4 attestation requires the prerequisite readiness owned by #10577; #10377 stays open.

  22. kim-em commented on Oct 6, 2026

    @kim-em
    kim-em
    on Oct 6, 2026
    OwnerAuthor

    Merged #10835 as 7bd0be2e706ce56ac78ab5b03828766f24557b26 after Opus review, local verification, and green CI run 37453403470.

    Rational-function normalization and cancellation now skip polynomial gcd and exact division when the denominator is one. The existing reconstruction and correspondence proofs cover the new branches. The retained controlled comparison contains all 24 observations and median within-pair speedups of 3.86 and 19.41 at the two tested depths. All four interacting-infinitesimal conformance depths pass the independent oracle; their complete current execution takes about 0.55 seconds, without claiming a controlled ratio against the historical emitter. The PR also supplies scoped rational/nested intermediate-operand evidence and independent checks.

    Remaining delivery: #10808, the consolidated performance report and complete small maximal-support workflows. Its reviewed head already includes #10835 and remains in CI. Final Phase-4 attestation still requires the prerequisite readiness owned by #10577. No larger timing campaign is required merely to cross a fitted-slope threshold. #10377 remains open.

  23. kim-em commented on Oct 6, 2026

    @kim-em
    kim-em
    on Oct 6, 2026
    OwnerAuthor

    Merged #10808 as 5d39918c26cf51c5435785a8ce394e11cad4ef60 after independent Opus reviews, local verification, and green CI run 37453415381.

    The consolidated report is reports/sign-det-performance.md. It links the retained scaling/comparison observations, allocation and process-memory records, profiles, ordinary-kernel examples, independent conformance, and scoped coefficient/derivative bounds. It explains the inconclusive findings without claiming they passed or requiring an expensive larger ladder.

    The small complete maximal-support workflows cover 3, 9 and 27 roots, with all 18 observations retained. Their medians are about 0.393 ms, 15.98 ms and 1.91 s for the entire diagnostic workflow, including input interpolation, three producers and replay. These are not isolated producer timings or a scaling law. The original measured source is reconstructible, and CI checks the archive and correctness cases.

    All outstanding implementation/evidence PRs from this session are merged, including #10825 and #10835. The remaining completion step is justified Phase-4 attestation for HexSignDet/HexSignDetMathlib. Current main still records HexSturm/HexSturmMathlib at Phase 3; prerequisite readiness is owned by #10577. No mathematical foundation theorem or #10389 admission remains missing. #10377 remains open until that prerequisite permits the final attestation.

  24. kim-em commented on Oct 8, 2026

    @kim-em
    kim-em
    on Oct 8, 2026
    OwnerAuthor

    Merged prerequisite improvement: #10856 shares certified canonical parent isolation between real-root entries and reuses factor arrays for reducible groups. Ordinary-kernel equalities preserve complete root results, canonical representatives, multiplicities and ordering. No reverse dependency on the real-closure family was added.

    Actual RealAlgebraicPoly.roots measurements show median adjacent Before/After ratios 1.27–1.56 where reuse applies; rational degree eight falls from approximately 147 ms to 94 ms. The singleton control is essentially unchanged; the reducible X^4−1 filter control has median ratio 1.037. Individual paired ranges, all 160 completed arms (including the rejected prototype), generated C and provenance are retained at reports/bench-results/real-root-isolation-reuse/README.md, with PNG/SVG/PDF degree plots against source-scoped historical FLINT/Z3 references. The severe external gap remains explicitly open.

    Both ordinary-kernel companion targets, all 196 real-algebraic benchmark checks under LEAN_ABORT_ON_PANIC=1, conformance, unchanged fixtures, all 83 exact oracle cases without skips, admission/phase/Mathlib-free checks and full required CI pass. Final-head CI: https://github.com/kim-em/hex-dev/actions/runs/37773135867 (232ed9a). Independent fresh Opus review and follow-up found no remaining merge blockers after fixes.

    All four assigned libraries remain Phase 3. Remaining #10577 work includes severe root/scalar isolation costs and complete advertised-operation/comparator coverage; Sturm timing-finding dispositions, retained-source/import-cone provenance and required production coefficient-sign coverage; then dependency-ordered Phase-4 attestation. The bench-local coefficient-sign traversal is an isolated diagnostic, not evidence of an end-to-end query/tactic speedup. The forward comparison-strategy extension stays excluded.

    #10377/#10378 and #10575 can use the merged proved APIs now; mathematical implementation should not wait for #10577 closure. Formal phase eligibility still follows actual direct dependencies. Full distribution readiness and unrelated transitive prerequisites remain with their existing owners.

  25. kim-em commented on Oct 8, 2026

    @kim-em
    kim-em
    on Oct 8, 2026
    OwnerAuthor

    #10577 readiness PR #10860 now contains the proposed Phase-4 attestation for all four Sturm/real-algebraic libraries and a proved shared-parent root enumeration fix. CI and fresh Opus review are running; the attestation is not merged yet.

    Do not wait for #10577 closure to use the merged proofs: HexSturmMathlib exports shared query/count semantics, and HexRealAlgebraicMathlib supplies implemented comparison and RealAlgebraicPoly.roots_spec completeness/multiplicity/order. Runnable integration: lake exe hexrealclosure_basic_conformance (retained exact Z3 check covers inverse/powers, positive enlargement, cubic roots and order).

    The four-library coverage/dependency matrix and ownership boundaries are in reports/real-closure-prerequisites.md. Reused #10377 BKR nested sweeps cover the Sturm prerequisite's required integration axes; #10378 retains tower-level costs beyond those observations. #10575 retains semantic-adapter/publication/package-boundary integration, including split-package fixture wiring. Forward comparison-strategy algorithms remain outside the implemented real-algebraic attestation.

    Current practical limits: scalar degree-eight addition ~158ms and square root ~5.6s; the newly corrected totally real degree-eight root enumeration ~203ms versus ~906ms for independent selectors in the same binary. Raw samples, plots, failed prototypes and source scopes are retained. No consumer issue or transitive library is automatically declared complete.

  26. kim-em commented on Oct 8, 2026

    @kim-em
    kim-em
    on Oct 8, 2026
    OwnerAuthor

    #10577 is closed by merged PR #10860 (upstream main 62f347465f46c9ab192d6d5c8fe0fb8129cd918d). All four prerequisites—HexSturm, HexSturmMathlib, HexRealAlgebraic and HexRealAlgebraicMathlib—now record Phase 4, with direct dependency eligibility, ordinary-kernel correspondence/axiom audits, compiled conformance, exact oracle evidence and final required CI verified. Final CI run: https://github.com/kim-em/hex-dev/actions/runs/37822662130 (successful exact reviewed head 39603195f2312b5e66293b04fc2f8f3f02e7d489).

    Ready APIs: shared Sturm–Tarski query/count semantics in HexSturmMathlib; implemented comparison correspondence and RealAlgebraicPoly.roots_spec completeness/multiplicity/order in HexRealAlgebraicMathlib. Runnable starting point: lake exe hexrealclosure_basic_conformance; checked examples also live in both computational READMEs. Proof consumers did not need to wait for formal phase attestation.

    reports/real-closure-prerequisites.md is the four-library readiness/dependency matrix. reports/hex-sturm-performance.md and reports/sturm-downstream-evidence.md reconcile the required report sections, prior timing findings and retained nested consumer sweeps. #10377 retains sign determination/BKR; #10378 retains tower/root assembly and tower-level extension/nested costs beyond those reused observations; #10575 retains semantic-adapter/publication/package-boundary integration (including split-package fixture wiring). This closes no downstream or unrelated transitive requirement automatically.

    Root filtering now shares certified factorization/isolation/Mahler refinement per irreducible parent group, with complete API equality and degree-eight independent/cached conformance. reports/bench-results/real-root-refinement-reuse/ retains raw observations and plots: eight-real-root enumeration ~203ms versus ~906ms for independent selectors in the same binary (4.46× median paired improvement). The four-quadratic reducible control costs ~196ms, with repeated per-factor certification still explicit. General large-factor reducible/high-degree latency is not attested.

    Current scalar size plots retain degree-eight addition ~158ms and square root ~5.6s; repeated interactive canonicalization remains a poor hot path. Historical FLINT/Z3 comparisons, failed prototypes and source-scoped profiles are retained. Forward comparison-strategy extensions remain outside this shipped-surface attestation. No publication or broad transitive promotion was performed.

  27. kim-em commented on Oct 10, 2026

    @kim-em
    kim-em
    on Oct 10, 2026
    OwnerAuthor

    Completed by merged PR #10861 (112de5a). Both SignDet owners now record Phase 4 with all declared prerequisites ready. Full CI passes on the final head: https://github.com/kim-em/hex-dev/actions/runs/38053042155. The implementation, correspondence proofs, certificate interfaces, direct examples, independent conformance and retained performance evidence are delivered. Opus review findings are addressed; the optional final wording recheck was unavailable due to its weekly quota, as documented on the PR. Upstream numeral-construction repair remains explicitly tracked by #10863, with its separate performance rollback merged in #10864. Tactic/manual and tower integration retain their own owners.

  28. kim-em
    closed this as completedon Oct 10, 2026

  29. kim-em commented on Oct 13, 2026

    @kim-em
    kim-em
    on Oct 13, 2026
    OwnerAuthor

    #10378 integration request: ordinary-kernel extraction of the second selected extension is blocked by context-frame serialization, rather than a missing sign theorem.

    Concrete source: two successive infinitesimals, the actual selected linear root α = ε + δ, then the positive selected root of Y² − α. Its native constructor compiles. NativeChain.ofContext stops in the second Descriptor.validate while comparing the nonempty predecessor signatures. Those signatures include Tower.rootData of the first descriptor, hence Dag.encode and a Std.HashMap lookup. Node replay/cache checks repeat this exact context comparison.

    Reduction reaches Std.DHashMap.Const.get? / Internal.AssocList.get?. The hash path uses opaque mixHash, and Internal.mkIdx uses USize with opaque System.Platform.getNumBits. Importing implementation bodies cannot remove these kernel reduction barriers. Independent Opus inspection confirmed both barriers. The existing one-level fixture does not force its first frame and therefore does not exercise this boundary.

    Proposed owner API: an exposed structural encoder with the same parameters and exact first-occurrence sharing/order as Dag.encode, using a structural list search in its logical definition, plus a proved function equality oriented as a compiler simplification to the existing HashMap implementation (@[csimp] theorem encodeLinear_eq : @encodeLinear = @encode). Tower.rootData would consume the reducible definition while compiled production keeps the current algorithm and exact packets. The proof invariant is state.indices[e]? = state.entries.toList.idxOf? e; existing Encoder.insert_valid demonstrates the needed HashMap insert reasoning. Leaf-only simplification would not cover arbitrary frame evidence.

    I am preparing a proof prototype in the #10378 experiment area, without changing the shared SignDet files. Please coordinate ownership/module placement for this small serialization API before shared-file integration. No new issue or worker is requested. This request does not dispute the already delivered BKR/Thom semantics or declare #10378 complete.

    The proof prototype is now available at commit 92b8241378 on issue-10378-multilevel. KernelReplay.FrameEncode.encodeLinear_eq proves unconditional exact output equality; FrameData.frameData_eq identifies the complete serializer. Ordinary-kernel probes force the entire retained first descriptor frame and check that a repeated child is stored once with both earlier references. All five axiom guards retain only the standard three axioms. Generated FrameData.c calls the existing Dag.encode, as required by the compiler simplification.

    The three-target Lake build passes (5,137 jobs), together with the 505-cone / 1,402-local-module source admission scan, DAG/source checks and both scanner/DAG test suites. The source experiments stayed below the enforced 8 GiB/no-swap cap. These are functional proof checks, not a Phase 4 performance campaign. The shared library files and Tower.rootData are unchanged pending ownership agreement; the two-level native staged fixture remains unproved.

  30. kim-em commented on Oct 14, 2026

    @kim-em
    kim-em
    on Oct 14, 2026
    OwnerAuthor

    #10575 API-polishing audit confirms the supplied-replay coverage and strict-order statement boundary requested in #10331 comments 6126809036 and 6129572591 is still absent from merged main. buildRoots_coverage and buildRoots_ordered take native producer success; rootsFrom_perm, rootsFrom_raw, rootsFrom_sorted, Replay.count_roots and descriptor root interpretation already provide the needed proof components.

    With #10377 implementation/Phase-4 ownership completed, #10575 will finish these two public semantic exports in HexSignDetMathlib as its assigned Phases 5–7 proof/API polishing. The existing producer theorems will delegate to the generalized supplied-replay statements, sharing the proof rather than copying it into the tactic adapter. The hypotheses will retain accepted full replay, successful extraction of the complete actual table and the existing coefficient/model laws. No algorithm or certificate contract changes are needed. The #10358 adapter can then reuse those owner-library exports.

    The current computational root-row polishing also proves exact output length and unit counts for arbitrary successful extraction; its manual distinguishes partial row extraction from full root coverage. This work does not advance phase counters or attest tower/tactic completion.

  31. kim-em commented on Oct 15, 2026

    @kim-em
    kim-em
    on Oct 15, 2026
    OwnerAuthor

    Existing-API question from the continuing #10358 adapter work. The four-boundary X²−sqrt2/(1,2] diagnostic now has per-child evidence: four section rows cost71,140 ms total; eight adjacent-root selected-sign boundary queries cost180,479 ms; five ordinary-point descriptors cost368 ms and their rows5,722 ms. Actual CellRead and both strict folds accept the produced matrix. All raw sources, completed traces and earlier profile limitations are retained. This is a shared-host diagnostic, not a scaling/speedup claim. The adapter’s mathematical typed-evidence existence/semantics proof is independently complete under its explicit ordinary-real model domain; executable/frozen integration continues.

    The actual hotspot calls Descriptor.buildSigns repeatedly at full descriptors sharing the same carrier/domain/full derivative prefix. The four section rows request the same additional atom list. For each interior proposed point, the two adjacent-root comparisons also request the same pointQuery, so identical prepared joint tables appear reusable across roots without enlarging query arity.

    Is there an existing executable API for extracting checked SelectedSigns d qs from a supplied checked prepared joint table, or reusing that table across descriptors? I inspected HexSignDet/SelectedSigns.lean: buildSignsPrepared always invokes buildPrepared, while buildSigns_ofTable is a success theorem, not a supplied-table extraction function. I found no public query-projection/restriction constructor. A small owner-level extraction operation shared with the existing builder would let the adapter cache actual tables with full literal context/head/endpoints/ordered-query bindings; no solver would run during frozen acceptance. Reusable extraction/search/replay stays with this owner. Please point me to the actual interface if I missed one.

    No new issue, worker or downstream dispatch is launched. The coordinator retains dispatch ownership, and independent adapter operational/serialization proofs continue while this API question is open.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

No labels
No labels

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions