[kim-em]

The real-coefficient number-field adapter uses a private import solely to unfold Presentation.model while identifying the original factory model. Export Presentation.model_eq and rewrite that existing consumer proof with the public equation, removing import all HexRealClosureTheory.NumberFieldTower.

The model definition remains abstract through ordinary imports; the parenthesized rfl proof intentionally suppresses Lean's automatic defeq attribute. Extend the existing number-field conformance axiom audit to the equation and model_read, and document the development API. No model, arithmetic/search, factory or source-certification algorithm, package requirement or phase counter changes.

Validation: full monorepo build14,744; owner module10,824 and actual ordinary-import adapter/number-field conformance10,919; final consumer refresh passes after documentation polish. Import DAG,669 scanned adapter/conformance cones and Mathlib-free benchmark/proof boundaries pass. The existing sealed-import guard now rejects import all of this owner module, with all12 DAG regression tests passing. Fresh Opus review began immediately after opening and found no blockers; the documentation and import-boundary findings are addressed. Exact updated-head CI remains required.

Refs #10575, #10378, #10358.

[kim-em]

Fresh Opus review found no blockers and confirmed the exact factory-model identity, need for the public rewrite and deliberate parenthesized rfl. Fixed terminology in the README, documented why the implicit defeq attribute is suppressed, and sealed import all of NumberFieldTower using the existing DAG mechanism. All12 DAG tests pass, including the real adapter path allowed through public import and refused through import all. Full monorepo14,744 and final NumberField consumer10,919 builds pass; new equation and model_read have ordinary-kernel axiom checks. The optional private-wrapper cleanup is left outside this small boundary change. Exact updated-head CI remains required.

[kim-em]

Rebased onto current main c1a871fda3140e81cb40421db4fb1f01b2ff20df, retaining both the newly merged KernelReplay fixture exceptions and this PR's sealed NumberFieldTower boundary. All five other changed files are byte-identical to the reviewed 8c1a092bfc head; the only conflict was the checker allowlist. All twelve checker tests, current DAG and whitespace checks pass. The actual owner module, ordinary-import adapter and NumberField conformance build pass together (10,922 jobs). No new measurements or contract changes. New exact head d8fdc8fb0349a3c174c33ddb80a27322fed5aafc has CI run39175085494; its existing single native watcher is running.