Expose the number-field presentation model equation

HexRealClosureTheory/README.md

@@ -47,6 +47,9 @@ example {registry : BaseContext.Registry}
   appropriate cofactor, including reducible defining polynomials.
 - Conversion, enlargement and sample-family proofs retain their explicit
   model, dependency and selected-embedding hypotheses.
+- The development `NumberFieldTower` import exports
+  `NumberField.Presentation.model_eq`, identifying a presentation's real model
+  with the target of its actual coefficient-conversion model.
 
 # Verification
 

adapters/HexRCF/RealCoefficients/NumberField.lean

@@ -9,10 +9,6 @@ public import HexRCF.RealCoefficients.Samples
 public import HexRCF.RealCoefficients.Coefficients
 public import HexRealClosureTheory.NumberFieldTower
 public import HexRealClosureTheory.ContextModel
--- The original-source factory binding unfolds only `Presentation.model`:
--- its chosen target is the public root conversion model. No owner proof or
--- arithmetic/search implementation is copied into this adapter.
-import all HexRealClosureTheory.NumberFieldTower
 
 public section
 
@@ -59,6 +55,7 @@ private theorem readModel (following : (BaseContext.PackedContext.pack (BaseCont
     {generator : RealAlgebraicNumber}
     (source : Hex.RealClosure.NumberField.Presentation generator registry) :
     source.context.model? following (Hex.RealClosure.NumberField.rationalModel registry) = some source.model := by
+  rw [Hex.RealClosure.NumberField.Presentation.model_eq]
   exact readCast following source.root.conversion_context
     (source.root.conversionModel (Hex.RealClosure.NumberField.rationalModel registry)).target
     (source.root.model (Hex.RealClosure.NumberField.rationalModel registry))

adapters/HexRealClosureTheory/NumberFieldTower.lean

@@ -109,6 +109,12 @@ noncomputable def model (source : Presentation generator registry) :
     Tower.Model source.context ℝ :=
   (source.root.conversionModel (rationalModel registry)).target
 
+/-- A presentation's real model is the target of its coefficient-conversion model.
+Use this equation instead of unfolding `model`, whose body is not exported. -/
+-- Parentheses suppress implicit `@[defeq]`, since `model` is abstract.
+theorem model_eq (source : Presentation generator registry) :
+    source.model = (source.root.conversionModel (rationalModel registry)).target := (rfl)
+
 /-- The retained generator has the original selected embedding. -/
 theorem generator_value (source : Presentation generator registry) :
     source.model.value source.root.convertedValue = generator.toReal := by

conformance/HexRCF/NumberField.lean

@@ -207,7 +207,9 @@ run_meta do
 #guard_msgs in
 #print axioms Hex.RCF.NumberFieldTests.coefficients
 run_meta do
-  for name in [``Hex.RCF.RealCoefficients.NumberField.value_eq_ofField,
+  for name in [``Hex.RealClosure.NumberField.Presentation.model_eq,
+      ``Hex.RCF.RealCoefficients.NumberField.model_read,
+      ``Hex.RCF.RealCoefficients.NumberField.value_eq_ofField,
       ``Hex.RCF.RealCoefficients.NumberField.runWith_spec,
       ``Hex.RCF.RealCoefficients.NumberField.run_coefficients,
       ``Hex.RCF.NumberFieldTests.coefficients] do

scripts/check_dag.py

@@ -32,7 +32,7 @@
     r"^\s*(?:(?:public|private|meta)\s+)*import\s+all\s+([A-Za-z0-9_.]+)\s*$"
 )
 
-# Private constructors in these modules are an ordinary/public-import API
+# Private constructors and definition bodies form an ordinary/public-import API
 # boundary. `import all` is a deliberate trusted-internals escape hatch, so
 # every owning exception must be an exact reviewed path rather than a suffix or
 # directory convention. The ECM diagnostic observes private preparation costs.
@@ -48,6 +48,8 @@
         Path("experiments/KernelReplay/FrameOwners.lean"),
         Path("experiments/KernelReplay/FrameOperand.lean"),
         Path("experiments/KernelReplay/FrameFrontier.lean")}),
+    # The model equation supports consumers without exposing the implementation.
+    "HexRealClosureTheory.NumberFieldTower": frozenset(),
     "HexInterval.Executable": frozenset(),
     "HexInterval.Runtime": frozenset(),
     "HexInterval.RuntimeController": frozenset(),

scripts/test_check_dag.py

@@ -165,6 +165,21 @@ def test_private_facets_are_build_dependencies(self) -> None:
 
 
 class SealedImportAllTest(unittest.TestCase):
+    def test_number_field_model_uses_public_imports(self) -> None:
+        with tempfile.TemporaryDirectory() as directory:
+            root = Path(directory)
+            path = Path("adapters/HexRCF/RealCoefficients/NumberField.lean")
+            full_path = root / path
+            full_path.parent.mkdir(parents=True)
+            module = "HexRealClosureTheory.NumberFieldTower"
+            full_path.write_text(f"public import {module}\n", encoding="utf-8")
+            self.assertEqual(check_sealed_import_all(root, [path]), [])
+            full_path.write_text(f"import all {module}\n", encoding="utf-8")
+            self.assertEqual(check_sealed_import_all(root, [path]), [
+                f"{path}:1 uses `import all {module}` outside its exact "
+                "trusted-internals allowlist"
+            ])
+
     def test_sturm_replay_exception_is_exact(self) -> None:
         with tempfile.TemporaryDirectory() as directory:
             root = Path(directory)