From 90f26097d4be33c2f536b078319f24ddf351b0dc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 1 Sep 2026 08:24:46 +0000 Subject: [PATCH 1/2] chore(number-field-mathlib): re-audit phase evidence Co-Authored-By: Codex --- .../SPEC/hex-number-field-mathlib.md | 34 ++++++++++++++++- ...-number-field-mathlib.conformance-reviewed | 38 ++++++++++++------- 2 files changed, 57 insertions(+), 15 deletions(-) diff --git a/HexNumberFieldMathlib/SPEC/hex-number-field-mathlib.md b/HexNumberFieldMathlib/SPEC/hex-number-field-mathlib.md index 1dc451eeb..079a9ee1d 100644 --- a/HexNumberFieldMathlib/SPEC/hex-number-field-mathlib.md +++ b/HexNumberFieldMathlib/SPEC/hex-number-field-mathlib.md @@ -4,8 +4,38 @@ This library is a `correspondence-only-layer`. -Computational conformance owner: `HexNumberField` -Computational performance owner: `HexNumberField` +Computational conformance owners: `HexNumberField`, `HexRoots`, `HexResultant`, `HexBerlekampZassenhaus`, `HexPolyZ` +Computational performance owners: `HexNumberField`, `HexRoots`, `HexResultant`, `HexBerlekampZassenhaus`, `HexPolyZ` + +The complete public surface is correspondence-only. The library declares no +`meta`, `partial`, `unsafe`, `IO`, syntax, macro, elaborator, tactic, reifier, +or certificate-checker entry point. Its semantic maps, polynomial views, ring +maps, equivalences, and field dictionaries are noncomputable. The +`LawfulBEq` and `DecidableEq` instances only package the executable +`AlgebraicNumber.beq` from `HexNumberField`, while the field dictionaries pin +every data field definitionally to the existing executable operations. The +`RootSet` predicates and multiplicity observers are proof-side views of a root +set already computed by `HexNumberField`; they do not construct, check, or +reify algebraic data. + +The transported operations and their computational owners are: + +| Transported surface | Computational owner | Owner evidence | +| --- | --- | --- | +| `QAdjoin` reduction, arithmetic, scalar actions, powers, inversion, approximation, and checked/total canonical conversion | `HexNumberField` | `conformance/HexNumberField/Conformance.lean`, `hexnumberfield_bench`, and `reports/hex-number-field-performance.md` | +| Lazy and canonical algebraic-number equality, zero recognition, arithmetic, exactification, and field operations | `HexNumberField` | The same conformance target covers checked and total lazy operations, semantic equality, rational construction, casts, scalar actions, and powers; the same benchmark target registers the corresponding compiled surfaces. | +| Yun decomposition, candidate disambiguation and merging, fixed-field roots, algebraic-coefficient roots, and common-field presentation (`rational?`, arithmetic and shifts, primitive search, powers, traces, coordinates, and `presentation?`) | `HexNumberField` | The root and algebraic-polynomial sections of the owner conformance target exercise the public pipelines, including common presentation transitively; the owner benchmark registers their components and end-to-end paths. | +| Selected-root isolation and `RefinedIsolation.refineTo?` | `HexRoots` | `conformance/HexRoots/Conformance.lean`, `hexroots_bench`, and `reports/hex-roots-performance.md` | +| Executable bivariate resultants used by lazy eliminants and fixed-field norm/evaluation eliminants | `HexResultant` | `conformance/HexResultant/Conformance.lean`, `hexresultant_bench`, and `reports/hex-resultant-performance.md` | +| Checked irreducibility and integer-polynomial factorization used by canonicalization and exactification | `HexBerlekampZassenhaus` | `conformance/HexBerlekampZassenhaus/Conformance.lean`, `hexbz_bench`, and `reports/hex-berlekamp-zassenhaus-performance.md` | +| Integer-polynomial representation, normalization, and conversion transported into Mathlib polynomials throughout the bridge | `HexPolyZ` | `conformance/HexPolyZ/Conformance.lean`, `hexpolyz_bench`, and `reports/hex-poly-z-performance.md` | + +There is deliberately no `conformance/HexNumberFieldMathlib` or +`bench/HexNumberFieldMathlib` source tree, no dedicated Lake conformance or +benchmark target, no `proof_probes` registry root, and no +`reports/hex-number-field-mathlib-performance.md`. Building the library checks +its correspondence theorems and axiom-regression guards; those guards are not +timed proof probes. Mathlib companion for `hex-number-field`. It interprets the executable types in `ℂ` and proves fixed-field correspondence, canonicalization, factorization-lazy diff --git a/status/hex-number-field-mathlib.conformance-reviewed b/status/hex-number-field-mathlib.conformance-reviewed index d01f4c42e..37646ffcb 100644 --- a/status/hex-number-field-mathlib.conformance-reviewed +++ b/status/hex-number-field-mathlib.conformance-reviewed @@ -1,14 +1,26 @@ -HexNumberFieldMathlib Phase 3 was reviewed on 2026-08-26. The library is a -proof-only correspondence layer with no executable reifier, certificate -checker, tactic, or other runtime surface, so the absence of a dedicated -Conformance module and HexConformance glob is intentional per -SPEC/testing.md's ceremonial-bridge ban. +HexNumberFieldMathlib satisfies the correspondence-only Phase-3/4 contract. +The complete source, umbrella, import, SPEC, and public-declaration audit is +recorded in HexNumberFieldMathlib/SPEC/hex-number-field-mathlib.md. It found no +executable reifier, certificate checker, tactic, proof-producing operation, or +independent kernel-cost surface. Semantic maps and structure transport are +noncomputable; the law-bearing equality and field dictionaries reuse the +executable operations of HexNumberField without replacing them. -The executable surface it verifies (QAdjoin arithmetic, root isolation and -disambiguation, approximation, Yun square-free decomposition) is exercised -by conformance/HexNumberField/Conformance.lean and the python-flint oracle -wired through scripts/ci/run_oracles.sh. The correspondence and -completeness declarations here are proofs rather than executable -destinations for conformance cases. Precedent: -status/hex-roots-mathlib.conformance-reviewed and -status/hex-truncated-series-mathlib.conformance-reviewed. +The SPEC maps the transported surface to the computational conformance and +performance owners HexNumberField, HexRoots, HexResultant, +HexBerlekampZassenhaus, and HexPolyZ. Each owner has its dedicated +conformance module and Phase-4 benchmark/report evidence. HexNumberField is +recorded through Phase 4; the other four owners are recorded through Phase 7. +The NumberField python-flint/PARI oracle is wired through +scripts/ci/run_oracles.sh, and the lower-level owners carry their own oracle +assignments. + +No conformance or bench source directory, Lake conformance or benchmark +target, headline performance report, or proof-probe registry root exists for +HexNumberFieldMathlib. Its build-enforced axiom guards check trust provenance; +they are not timed proof probes. The explicit `correspondence_only: true` +registry classification and the absence of ordinary Phase-4 metadata are +therefore consistent. The later phase record remains valid: the library is +still integrated in the build and release graph, its proof and documentation +artifacts remain present, and its Phase-7 material is carried by the shared +number-field manual chapter. From d29633b64c3ebca78b247d6dc54b883808beaf5d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 1 Sep 2026 08:36:02 +0000 Subject: [PATCH 2/2] docs(number-field-mathlib): complete owner audit Co-Authored-By: Codex --- .../SPEC/hex-number-field-mathlib.md | 33 +++++++++++-------- ...-number-field-mathlib.conformance-reviewed | 17 +++++----- 2 files changed, 28 insertions(+), 22 deletions(-) diff --git a/HexNumberFieldMathlib/SPEC/hex-number-field-mathlib.md b/HexNumberFieldMathlib/SPEC/hex-number-field-mathlib.md index 079a9ee1d..61b23c69a 100644 --- a/HexNumberFieldMathlib/SPEC/hex-number-field-mathlib.md +++ b/HexNumberFieldMathlib/SPEC/hex-number-field-mathlib.md @@ -4,19 +4,21 @@ This library is a `correspondence-only-layer`. -Computational conformance owners: `HexNumberField`, `HexRoots`, `HexResultant`, `HexBerlekampZassenhaus`, `HexPolyZ` -Computational performance owners: `HexNumberField`, `HexRoots`, `HexResultant`, `HexBerlekampZassenhaus`, `HexPolyZ` +Computational conformance owners: `HexNumberField`, `HexRoots`, `HexResultant`, `HexBerlekampZassenhaus`, `HexPolyZ`, `HexPoly`, `HexRowReduce`, `HexMatrix` +Computational performance owners: `HexNumberField`, `HexRoots`, `HexResultant`, `HexBerlekampZassenhaus`, `HexPolyZ`, `HexPoly`, `HexRowReduce`, `HexMatrix` The complete public surface is correspondence-only. The library declares no `meta`, `partial`, `unsafe`, `IO`, syntax, macro, elaborator, tactic, reifier, or certificate-checker entry point. Its semantic maps, polynomial views, ring maps, equivalences, and field dictionaries are noncomputable. The -`LawfulBEq` and `DecidableEq` instances only package the executable -`AlgebraicNumber.beq` from `HexNumberField`, while the field dictionaries pin -every data field definitionally to the existing executable operations. The -`RootSet` predicates and multiplicity observers are proof-side views of a root -set already computed by `HexNumberField`; they do not construct, check, or -reify algebraic data. +field dictionaries pin every data field definitionally to the existing +executable operations. `RootSet.totalMultiplicity` is the only +bridge-originated ordinary definition with a data result: it is the linear +structural fold used to state the root-result multiplicity theorem, not an +advertised algebraic operation. The `LawfulBEq` and `DecidableEq` instances +package the executable `AlgebraicNumber.beq` from `HexNumberField`. These +result observers and law dictionaries introduce no independent algebraic +algorithm, checker, reifier, proof generator, or kernel-cost surface. The transported operations and their computational owners are: @@ -25,10 +27,13 @@ The transported operations and their computational owners are: | `QAdjoin` reduction, arithmetic, scalar actions, powers, inversion, approximation, and checked/total canonical conversion | `HexNumberField` | `conformance/HexNumberField/Conformance.lean`, `hexnumberfield_bench`, and `reports/hex-number-field-performance.md` | | Lazy and canonical algebraic-number equality, zero recognition, arithmetic, exactification, and field operations | `HexNumberField` | The same conformance target covers checked and total lazy operations, semantic equality, rational construction, casts, scalar actions, and powers; the same benchmark target registers the corresponding compiled surfaces. | | Yun decomposition, candidate disambiguation and merging, fixed-field roots, algebraic-coefficient roots, and common-field presentation (`rational?`, arithmetic and shifts, primitive search, powers, traces, coordinates, and `presentation?`) | `HexNumberField` | The root and algebraic-polynomial sections of the owner conformance target exercise the public pipelines, including common presentation transitively; the owner benchmark registers their components and end-to-end paths. | -| Selected-root isolation and `RefinedIsolation.refineTo?` | `HexRoots` | `conformance/HexRoots/Conformance.lean`, `hexroots_bench`, and `reports/hex-roots-performance.md` | +| Selected-root isolation and `RefinedIsolation.refineTo?`; dyadic-ball construction and arithmetic; radius, extent, membership, and square-intersection semantics | `HexRoots` | `conformance/HexRoots/Conformance.lean`, `hexroots_bench`, and `reports/hex-roots-performance.md` | | Executable bivariate resultants used by lazy eliminants and fixed-field norm/evaluation eliminants | `HexResultant` | `conformance/HexResultant/Conformance.lean`, `hexresultant_bench`, and `reports/hex-resultant-performance.md` | | Checked irreducibility and integer-polynomial factorization used by canonicalization and exactification | `HexBerlekampZassenhaus` | `conformance/HexBerlekampZassenhaus/Conformance.lean`, `hexbz_bench`, and `reports/hex-berlekamp-zassenhaus-performance.md` | | Integer-polynomial representation, normalization, and conversion transported into Mathlib polynomials throughout the bridge | `HexPolyZ` | `conformance/HexPolyZ/Conformance.lean`, `hexpolyz_bench`, and `reports/hex-poly-z-performance.md` | +| Dense-polynomial Euclidean operations, composition, scaling, and coefficient transforms used by Yun, resultants, and presentation proofs | `HexPoly` | `conformance/HexPoly/Conformance.lean`, `hexpoly_bench`, and `reports/hex-poly-performance.md` | +| `Matrix.spanCoeffs` used by common-field coordinate recovery | `HexRowReduce` | `conformance/HexRowReduce/Conformance.lean`, `hexrowreduce_bench`, and `reports/hex-row-reduce-performance.md` | +| Matrix/vector construction, row access, multiplication, and conversion used by exactification and coordinate recovery | `HexMatrix` | `conformance/HexMatrix/Conformance.lean`, `hexmatrix_bench`, and `reports/hex-matrix-performance.md` | There is deliberately no `conformance/HexNumberFieldMathlib` or `bench/HexNumberFieldMathlib` source tree, no dedicated Lake conformance or @@ -340,11 +345,11 @@ No external comparator is required. **Justification:** `correspondence-only-layer` per `SPEC/benchmarking.md §"Comparator naming"`. The library introduces no -number-field arithmetic algorithm; it verifies the executable QAdjoin -arithmetic, root isolation, and Yun decomposition implemented -elsewhere. The computational performance owner is hex-number-field, -where the arithmetic and root ladders and the PARI/GP comparator are -measured. +number-field arithmetic algorithm; it verifies operations implemented by the +computational performance owners enumerated in the correspondence-only table +above. Their own Phase-4 targets and reports carry the measurements and +comparator decisions. In particular, `hex-number-field` measures the +high-level arithmetic and root ladders and its PARI/GP comparator. ## References diff --git a/status/hex-number-field-mathlib.conformance-reviewed b/status/hex-number-field-mathlib.conformance-reviewed index 37646ffcb..e4c242408 100644 --- a/status/hex-number-field-mathlib.conformance-reviewed +++ b/status/hex-number-field-mathlib.conformance-reviewed @@ -8,12 +8,12 @@ executable operations of HexNumberField without replacing them. The SPEC maps the transported surface to the computational conformance and performance owners HexNumberField, HexRoots, HexResultant, -HexBerlekampZassenhaus, and HexPolyZ. Each owner has its dedicated -conformance module and Phase-4 benchmark/report evidence. HexNumberField is -recorded through Phase 4; the other four owners are recorded through Phase 7. -The NumberField python-flint/PARI oracle is wired through -scripts/ci/run_oracles.sh, and the lower-level owners carry their own oracle -assignments. +HexBerlekampZassenhaus, HexPolyZ, HexPoly, HexRowReduce, and HexMatrix. Each +owner has its dedicated conformance module and Phase-4 benchmark/report +evidence. HexNumberField, HexPoly, and HexRowReduce are recorded through Phase +4; the other five owners are recorded through Phase 7. The NumberField +python-flint/PARI oracle is wired through scripts/ci/run_oracles.sh, and the +lower-level owners carry their own oracle assignments. No conformance or bench source directory, Lake conformance or benchmark target, headline performance report, or proof-probe registry root exists for @@ -21,6 +21,7 @@ HexNumberFieldMathlib. Its build-enforced axiom guards check trust provenance; they are not timed proof probes. The explicit `correspondence_only: true` registry classification and the absence of ordinary Phase-4 metadata are therefore consistent. The later phase record remains valid: the library is -still integrated in the build and release graph, its proof and documentation +still integrated in the build and library graph, its proof and documentation artifacts remain present, and its Phase-7 material is carried by the shared -number-field manual chapter. +number-field manual chapter. The pair remains unreleased and is intentionally +absent from the publish manifest.