Skip to content

chore(number-field-mathlib): re-audit phase evidence #9886

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kim-em merged 2 commits into from
Sep 1, 2026
Merged

chore(number-field-mathlib): re-audit phase evidence #9886

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
90f2609
chore(number-field-mathlib): re-audit phase evidence
Sep 1, 2026
d29633b
docs(number-field-mathlib): complete owner audit
Sep 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
49 changes: 42 additions & 7 deletions HexNumberFieldMathlib/SPEC/hex-number-field-mathlib.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,43 @@

This library is a `correspondence-only-layer`.

Computational conformance owner: `HexNumberField`
Computational performance owner: `HexNumberField`
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
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:

| 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?`; 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
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
Expand Down Expand Up @@ -310,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

Expand Down
39 changes: 26 additions & 13 deletions status/hex-number-field-mathlib.conformance-reviewed
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,14 +1,27 @@
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, 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
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 library graph, its proof and documentation
artifacts remain present, and its Phase-7 material is carried by the shared
number-field manual chapter. The pair remains unreleased and is intentionally
absent from the publish manifest.
Loading