From fac6a10b5ac3c71980a71a44646ba7c5497198d7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 16 Oct 2026 07:31:51 +0000 Subject: [PATCH 1/2] Expose the number-field presentation model equation --- HexRealClosureTheory/README.md | 4 ++++ adapters/HexRCF/RealCoefficients/NumberField.lean | 5 +---- adapters/HexRealClosureTheory/NumberFieldTower.lean | 5 +++++ conformance/HexRCF/NumberField.lean | 4 +++- 4 files changed, 13 insertions(+), 5 deletions(-) diff --git a/HexRealClosureTheory/README.md b/HexRealClosureTheory/README.md index 3e8236749e..bdf3c95149 100644 --- a/HexRealClosureTheory/README.md +++ b/HexRealClosureTheory/README.md @@ -47,6 +47,10 @@ 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 exposes + `NumberField.Presentation.model_eq`, identifying the actual coefficient + conversion's target model. Adapters can bind the original factory model + through this public equation without a private import. # Verification diff --git a/adapters/HexRCF/RealCoefficients/NumberField.lean b/adapters/HexRCF/RealCoefficients/NumberField.lean index 67f5e1da07..75eb00320b 100644 --- a/adapters/HexRCF/RealCoefficients/NumberField.lean +++ b/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)) diff --git a/adapters/HexRealClosureTheory/NumberFieldTower.lean b/adapters/HexRealClosureTheory/NumberFieldTower.lean index 9155b65d14..3dbfa3fbac 100644 --- a/adapters/HexRealClosureTheory/NumberFieldTower.lean +++ b/adapters/HexRealClosureTheory/NumberFieldTower.lean @@ -109,6 +109,11 @@ noncomputable def model (source : Presentation generator registry) : Tower.Model source.context ℝ := (source.root.conversionModel (rationalModel registry)).target +/-- The presentation uses the target of its actual coefficient-conversion model. +This explicit equation leaves the model definition abstract through ordinary imports. -/ +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 diff --git a/conformance/HexRCF/NumberField.lean b/conformance/HexRCF/NumberField.lean index 85c659fb1f..eb7d3e97bc 100644 --- a/conformance/HexRCF/NumberField.lean +++ b/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 From d8fdc8fb0349a3c174c33ddb80a27322fed5aafc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 16 Oct 2026 07:49:02 +0000 Subject: [PATCH 2/2] Guard the public number-field model boundary --- HexRealClosureTheory/README.md | 7 +++---- .../HexRealClosureTheory/NumberFieldTower.lean | 5 +++-- scripts/check_dag.py | 4 +++- scripts/test_check_dag.py | 15 +++++++++++++++ 4 files changed, 24 insertions(+), 7 deletions(-) diff --git a/HexRealClosureTheory/README.md b/HexRealClosureTheory/README.md index bdf3c95149..0fdfb1e2d2 100644 --- a/HexRealClosureTheory/README.md +++ b/HexRealClosureTheory/README.md @@ -47,10 +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 exposes - `NumberField.Presentation.model_eq`, identifying the actual coefficient - conversion's target model. Adapters can bind the original factory model - through this public equation without a private import. +- 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 diff --git a/adapters/HexRealClosureTheory/NumberFieldTower.lean b/adapters/HexRealClosureTheory/NumberFieldTower.lean index 3dbfa3fbac..ef45ac3448 100644 --- a/adapters/HexRealClosureTheory/NumberFieldTower.lean +++ b/adapters/HexRealClosureTheory/NumberFieldTower.lean @@ -109,8 +109,9 @@ noncomputable def model (source : Presentation generator registry) : Tower.Model source.context ℝ := (source.root.conversionModel (rationalModel registry)).target -/-- The presentation uses the target of its actual coefficient-conversion model. -This explicit equation leaves the model definition abstract through ordinary imports. -/ +/-- 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) diff --git a/scripts/check_dag.py b/scripts/check_dag.py index 47492db78f..69155cc381 100644 --- a/scripts/check_dag.py +++ b/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(), diff --git a/scripts/test_check_dag.py b/scripts/test_check_dag.py index d6658bf2d5..cfbf204c9d 100644 --- a/scripts/test_check_dag.py +++ b/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)