From 12da871b638188ddb43170038aa97a16a013a910 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 18 Oct 2026 23:47:36 +0000 Subject: [PATCH] Document original infinitesimal comparisons and finite joint real witnesses --- HexManual/Chapters/HexRealClosure.lean | 70 ++++++++++++++++++++++++++ HexRealClosureTheory/README.md | 7 +++ reports/real-closure-requirements.md | 38 ++++++++++---- 3 files changed, 104 insertions(+), 11 deletions(-) diff --git a/HexManual/Chapters/HexRealClosure.lean b/HexManual/Chapters/HexRealClosure.lean index db256bb80f..41f89a3f09 100644 --- a/HexManual/Chapters/HexRealClosure.lean +++ b/HexManual/Chapters/HexRealClosure.lean @@ -276,6 +276,18 @@ The result retains both the original request and the checked conversions. Its {name}`Hex.RealClosure.Tower.Live.Request.gatherReconciled?_shared` law identifies the actual successful owner gather used by the live collection. +For a returned {name}`Hex.RealClosure.Tower.Live.Collection`, the original +request position determines the retained owner map. +{name}`Hex.RealClosure.Tower.Live.Collection.frame_transport` identifies the +transported frame at that same position; +{name}`Hex.RealClosure.Tower.Live.Collection.frame_values` and +{name}`Hex.RealClosure.Tower.Live.Collection.frame_polynomials` identify its +mapped values and polynomials. +{name}`Hex.RealClosure.Tower.Live.Collection.frame_descriptors` retains the +complete raw descriptors through that map, including heads, bounds, +derivative positions and signs. These equations concern the actual returned +collection. They do not construct an ordinary-real interpretation of its data. + This route permits different orders of registered provider keys. It preserves the existing ordered conversion when one is available; otherwise it uses the checked provider reconciliation. Key coverage and infinitesimal depth are @@ -426,6 +438,13 @@ Context-bound serialization records the ordered base signature, selected descriptors and recursively encoded coefficients. This is reconstructible data, not a decimal approximation of the selected root. +For a full signature, +{name}`Hex.RealClosure.Tower.Signature.codec_encode` identifies the encoded +structured literal and +{name}`Hex.RealClosure.Tower.Signature.codec_literal` restores the original +signature from that literal. This proves identity decoding, separately from +validation of the context and its selected roots. + {name}`Hex.RealClosure.Tower.Context.write` and {name}`Hex.RealClosure.Tower.Context.read` use the exact whole-context binding. {name}`Hex.RealClosure.Tower.Context.read_write` proves the value roundtrip; @@ -476,6 +495,25 @@ coverage and sign constancy belong to the companion's family theorems; a sample data structure alone does not prove these claims. This interface does not provide full CAD or multivariate coverings. +# Original infinitesimal comparisons + +The existing native `BasicConformance` examples cover all seven comparisons +from the recovered paper's `ex2.py`. For the first positive infinitesimal `ε` +they check `1 / ε > 10^28` and `(1 + ε) / (1 - ε) > 1`. For the selected +cube root `a` of `ε`, both `a > ε` and `a² > ε` hold, whereas `a⁴ > ε` is +false. A second positive infinitesimal `δ` satisfies `δ < ε` and `δ < ε^10`. + +Adding `δ` enlarges the actual context containing the cube root. The example +retains the earlier square root, cube root and all seven computed cubic values; +it checks the transported equation and signs. The +[comparison record](https://github.com/kim-em/hex-dev/blob/main/reports/real-closure-original-ex2/README.md) +links the existing emitter, exact Z3 oracle and mutation controls. The original +`10^28` comparison is separate from the retained `10^27` regression. +These are conformance examples for native infinitesimal computation. They +neither assert the inequalities for every positive real choice of `ε` and `δ` +nor supply computational scaling evidence. The paper's introductory cases +using π still require their caller-supplied provider. + # The Mathlib correspondence {name}`Hex.RealClosure.Tower.Model` interprets one native context in a @@ -550,3 +588,35 @@ Z3/python-flint oracles separately check the emitted arithmetic and root fixtures. Retained tower and clean/eager measurements supply computational evidence; these examples and theorem applications do not replace it. + +# Joint ordinary-real witnesses for a finite tower + +A finite set of guards can hold at chosen real coordinates even though a +positive infinitesimal field has no order-preserving embedding into the reals. +The interpretation and coordinates must work together for the original +coefficient data, selected roots and arithmetic records. + +The existing nested fixture starts over two successive infinitesimals `ε` +and `δ`. It selects a root `α` of `X - (ε + δ)`, then the positive selected +root of `Y² - α`. Its public theorem `GuardJointPublic.exists_points` gives +one interpretation of the requested coefficient data and two real coordinates. +The coefficient interpretation is a ring homomorphism on a subring containing +the required finite inventory. +At those same witnesses it retains the ordered coefficient agreement, +inherited provider values, both packing/sign/inverse inventories, every +original guard and the computed native product. + +The ordinary-import consumer +[`GuardJointUse.coordinates`](https://github.com/kim-em/hex-dev/blob/main/experiments/KernelReplay/GuardJointUse.lean) +extracts those witnesses and proves both original defining-polynomial equations +and the native square equation at them. Reuse that checked consumer; its +[joint realization record](https://github.com/kim-em/hex-dev/blob/main/reports/real-closure-joint-replay.md) +links the full proposition and the independent body/dependency audit. The audit +checks the permitted standard-three axiom closure and excludes the older +cached operand and whole-field reference construction. + +This is a fixed two-level example. The general recursive exporter for +arbitrary interleaved live collections, direct `Sample.realizeReplay`, strict +compiled rejection of missing inventories and the specified tower performance +evidence remain separate requirements. The ordinary-real tactic interface and +its examples remain in the {ref "hex-rcf"}[real-coefficient `rcf` manual]. diff --git a/HexRealClosureTheory/README.md b/HexRealClosureTheory/README.md index 3e8236749e..5ccb624e2d 100644 --- a/HexRealClosureTheory/README.md +++ b/HexRealClosureTheory/README.md @@ -53,6 +53,13 @@ example {registry : BaseContext.Registry} A common ordered real-closed model can be non-Archimedean. These correspondence laws do not give an ordinary-real embedding of a positive infinitesimal or construct the whole joint realization of an arbitrary serialized tower. +The development [nested joint fixture](../reports/real-closure-joint-replay.md) +does supply one interpretation on the required coefficient subring and two +ordinary real coordinates +for its original guards and computed product together. Its ordinary-import +consumer derives both original root equations and the native square equation +at those witnesses. This fixed example does not supply the general exporter +or an ordinary-real embedding of the infinitesimal field. Producer totality is distinct from soundness of arbitrary accepted evidence. Source-expression divisors erased by cancellation remain the consumer's guards. diff --git a/reports/real-closure-requirements.md b/reports/real-closure-requirements.md index aa9c8d676f..ce10f64ef3 100644 --- a/reports/real-closure-requirements.md +++ b/reports/real-closure-requirements.md @@ -88,9 +88,9 @@ Owning SPECs: [RealClosure](../SPEC/Libraries/hex-real-closure.md), | Missing joint provider histories and gathering | `RealPrefix.extend?`, `Catalog.construct?`, `Live.Request.gatherConstructed?`; the real-only prefix is constructed before its infinitesimal/algebraic suffix | `RealPrefix.extend?_isSome` characterizes producer success by path-local `Ready`; `RealPrefix.Model.extend?_model` and `extend?_embedding` prove existence and predecessor preservation under caller-proved `Valid`; `Catalog.Construction.models` preserves an input catalog model invariant; `gatherConstructed?_success` proves live gathering. Core `BaseHistoryTests` cover two stages, duplicate reuse and a missing second packet; semantic `install_providers` and `KernelReplay.ProviderHistoryAudit` cover the provider premises | Merged [#10962](https://github.com/kim-em/hex-dev/pull/10962). Gathering success requires a model of the seed prefix, actual-path progress/validity and distinct owner keys, without a completed target model. These are caller premises, not generated analytic evidence. Arbitrary serialized frontend/provider certification, interleaved ordinary-real realization and the owner Phase-4 attestation remain separate requirements. The constructed-catalog laws are development APIs in `HexQuerySemantics`, not published companion imports | | New infinitesimal below all transported positive old values | `Context.enlargeWithParameter?`; `enlargeWithParameter?_model`, `_ordered`, `_algebraic` | `TowerEnlargeOrderTests`: successive square roots, old inverse/gaps and preceding infinitesimal | Delivered for the actual returned conversion; not total all-live enlargement | | Compatible algebraic union and real-closedness | `Union`, `TowerUnion`, relative ambient model; union real-closedness and common extension | `UnionTests`, `TowerModelTests` | Native finite `Presentation` quotient bijection, algebra equivalence and real-closedness merged in [#10616](https://github.com/kim-em/hex-dev/pull/10616); gathered-union identification in [#10667](https://github.com/kim-em/hex-dev/pull/10667) is merged | -| Sections/sectors, original-model signs and joint ordinary-real realization | Complete root families and sample/sector contracts | Native sample API and exact sample families from merged [#10607](https://github.com/kim-em/hex-dev/pull/10607); `Specialize.realizeReplay` for one rational-function infinitesimal step | Local section/sector coverage, actual interpretation and sector sign constancy delivered. One-step realization assumes an ordered real embedding of the base; merged [#10888](https://github.com/kim-em/hex-dev/pull/10888) adds finite native reconstruction from retained owners and a validated infinitesimal base, with dependency discovery before witnesses and checked requested propositions/guards. Its `KernelReplay.NativeAssemblyUse.coordinate` consumer derives the original root equation and coefficient-zero addition equation at one returned interpretation/coordinate. General interleaved normalization, simultaneous realization and a successful multilevel native fixture remain with #10378 | +| Sections/sectors, original-model signs and joint ordinary-real realization | Complete root families and sample/sector contracts | Native sample API and exact sample families from merged [#10607](https://github.com/kim-em/hex-dev/pull/10607); `Specialize.realizeReplay` for one rational-function infinitesimal step | Local section/sector coverage, actual interpretation and sector sign constancy delivered. One-step realization assumes an ordered real embedding of the base; merged [#10888](https://github.com/kim-em/hex-dev/pull/10888) adds finite native reconstruction from retained owners and a validated infinitesimal base, with dependency discovery before witnesses and checked requested propositions/guards. Its `KernelReplay.NativeAssemblyUse.coordinate` consumer derives the original root equation and coefficient-zero addition equation at one returned interpretation/coordinate. Merged [#10979](https://github.com/kim-em/hex-dev/pull/10979) supplies a fixed two-level fixture with one coefficient interpretation and two ordinary-real points satisfying its original guards and computed product together; `GuardJointUse.coordinates` derives both original root equations and the native square equation at those witnesses. General interleaved normalization, direct `Sample.realizeReplay` and export for arbitrary live collections remain with #10378 | | Independent trivial-base fast path agreement | `Trivial.Rational.roots`; `Trivial.Rational.roots_eq`, `compare_eq` | `TrivialTests`, real-algebraic root/multiplicity/order conformance | Full native rational tower conversion, root/multiplicity/order, arithmetic and inverse agreement merged in [#10624](https://github.com/kim-em/hex-dev/pull/10624) with independent FLINT cases; merged [#10755](https://github.com/kim-em/hex-dev/pull/10755) retains original selected number-field coordinates through roots and samples. Broader registered-base coverage and the final evidence audit remain with #10378 | -| Reconstructible printing, registered constants and exploration/number-field integration | Base/context/element codecs, `FrameFormat`; `read_write`, `read_stale`, exact registry/signature bindings | `CodecTests`, `BaseCatalogTests`, `FrameFormatTests`; nested read/replay fixtures | Codec slices and original number-field integration (#10755) are delivered. The test-only [#10914](https://github.com/kim-em/hex-dev/pull/10914) fixture uses the existing Liouville test provider to reconstruct six packed/indexed expressions after algebraic enlargement over a second infinitesimal. Its [checks](../HexRealClosureTheory/ReprProviderTests.lean) observe element/coefficient signs and eight missing/changed-version refusals for the four packed kinds; indexed root/root-set cases check text roundtrip. This evidence is separate from joint ordinary-real realization. Merged [#10964](https://github.com/kim-em/hex-dev/pull/10964) supplies the public `Tower.contextCodec_encode_self`, `contextCodec_self` and `contextCodec_self_iff` parent-reference laws; the ordinary-import `HexRCF.PublicGraphCodec` checks parsed forms and a decoder bind with kernel axiom guards. Reading that reference validates neither its supplied signature nor its selected roots. Complete serialization/exploration acceptance and the final evidence audit remain with [#10378](https://github.com/kim-em/hex-dev/issues/10378). Registry names must resolve to the same caller-supplied source | +| Reconstructible printing, registered constants and exploration/number-field integration | Base/context/element codecs, `FrameFormat`; `read_write`, `read_stale`, exact registry/signature bindings | `CodecTests`, `BaseCatalogTests`, `FrameFormatTests`; nested read/replay fixtures | Codec slices and original number-field integration (#10755) are delivered. The test-only [#10914](https://github.com/kim-em/hex-dev/pull/10914) fixture uses the existing Liouville test provider to reconstruct six packed/indexed expressions after algebraic enlargement over a second infinitesimal. Its [checks](../HexRealClosureTheory/ReprProviderTests.lean) observe element/coefficient signs and eight missing/changed-version refusals for the four packed kinds; indexed root/root-set cases check text roundtrip. This evidence is separate from joint ordinary-real realization. Merged [#10964](https://github.com/kim-em/hex-dev/pull/10964) supplies the public `Tower.contextCodec_encode_self`, `contextCodec_self` and `contextCodec_self_iff` parent-reference laws; the ordinary-import `HexRCF.PublicGraphCodec` checks parsed forms and a decoder bind with kernel axiom guards. Reading that reference validates neither its supplied signature nor its selected roots. Merged [#10980](https://github.com/kim-em/hex-dev/pull/10980) separately provides `Signature.codec_encode` and `codec_literal` for the full structured identity, with ordinary-import `SignatureCodecTests` and exact axiom guards; identity decoding still does not validate selected roots. Complete serialization/exploration acceptance and the final evidence audit remain with [#10378](https://github.com/kim-em/hex-dev/issues/10378). Registry names must resolve to the same caller-supplied source | | Nested evidence and adversarial cases | Actual α²=2+ε₁, β²=α+ε₂ selected-sign fixture; selected inversion, shared prepared domain and literal context checks | `conformance/HexRealClosure/NestedReplay.lean`; changed consumers, cycles, stale contexts and zero/wrong denominators; isolation oracle | Functional evidence merged in [#10610](https://github.com/kim-em/hex-dev/issues/10610); no joint-realization or computational scaling attestation | | Corrected paper Example 3, tower8, MetiTarski, Rioboo/Strzeboński, clean/eager and representative attribution | Ordinary native tower/root algorithms | [arithmetic experiments](hex-real-closure/general-arithmetic.md), [isolation anchors](hex-real-closure/isolation-anchors.md), [storage experiment](real-closure-storage-experiments.md), owner conformance | The [Phase-4 report](real-closure-phase4.md) indexes retained clean/eager and MetiTarski evidence, including inconclusive results and remaining obligations. The [original source archive](bench-results/real-closure-cade24-inputs/README.md), recovered in merged [#10899](https://github.com/kim-em/hex-dev/pull/10899), supplies `basic.py`/`nlsat.py` provenance and resolves the tower8 coefficient/premise discrepancy: executed stage degrees are 4, 2, 4, 5, 5, the first constant is `4 − 2ε²`, and the third executed polynomial has degree four despite its label. Native and exact Z3 conformance cover the original [Rioboo](real-closure-rioboo.md) and real [Strzeboński](real-closure-strz.md) inputs. Tower8 execution and matched clean/eager outcomes require caller constant inputs; the unsupported-case versus required tower8 evidence decision remains open with #10378 below. Required counters, certificate-sharing/depth costs, remaining trivial-path families and the final audit are still required. Owner Phase-4 attestation remains open; functional and provenance checks do not replace it | @@ -332,7 +332,7 @@ witnesses and all eleven conjuncts, deriving the original root equation and coefficient-zero addition at the same returned interpretation and coordinate. Its context proofs retain the original descriptor and the actual adjoined context. This supplies a mathematical consumer rather than an acceptance claim -based only on native example output. CI names 32 `KernelReplay` module targets, +based only on native example output. That milestone named 32 `KernelReplay` CI module targets, 19 of them added by #10888. A twentieth new module, `FiniteThomWitness`, builds as a dependency of `FiniteThomJoint`; CI also names two existing replay executables. Build-time controls reject exhausted discovery, missing owners and @@ -343,13 +343,29 @@ nested, generated and collection probes; emission and byte replay of the serialized SignDet graph, including count and context mutations; and argument handling. None invokes the #10888 native reconstruction path. -The exercised path still does not establish general dependency-closed -interleaved normalization, successful multilevel native joint reconstruction or -the remaining specified conformance/performance evidence. Directly computed -coefficient operands and product-law requests have no successful end-to-end -fixture: the owning SPEC records dependency traversal exceeding the local -8 GiB experiment limit. This is a retained resource limitation, not a scaling -pass. Merged [#10899](https://github.com/kim-em/hex-dev/pull/10899) resolves +That single-extension path does not establish general dependency-closed +interleaved normalization or the remaining specified conformance/performance +evidence. Its earlier directly computed coefficient/product-law attempts +exceeded the local 8 GiB experiment limit; those failures remain retained. +Merged [#10979](https://github.com/kim-em/hex-dev/pull/10979) now supplies the +[original nested joint fixture](real-closure-joint-replay.md): one coefficient +interpretation and two ordinary real points satisfy the original ordered +agreement, inherited providers, both inventories, all 3773 guards and the +computed product together. The ordinary-import `GuardJointUse.coordinates` +derives both original raw defining equations and the native square equation +at those same witnesses. Its full dependency audit rejects the older cached +operand and whole-field reference construction. This is a successful fixed +multilevel example, not the recursive exporter for arbitrary live collections +or a computational scaling pass. + +Merged [#10982](https://github.com/kim-em/hex-dev/pull/10982) separately covers +all seven [original ex2 comparisons](real-closure-original-ex2/README.md), with +the exact `10^28` bound and actual live cubic context transported across the +second infinitesimal. The native output and exact Z3 oracle check the retained +roots and computed values; the π-dependent introductory cases remain +unsupported without caller providers. + +Merged [#10899](https://github.com/kim-em/hex-dev/pull/10899) resolves the original `tower8` source and premise correction through the [verified CADE-24 input inventory](bench-results/real-closure-cade24-inputs/README.md). The first executed polynomial is reducible, with constant `4 − 2ε²`; @@ -448,7 +464,7 @@ themselves establish the applicable phase obligations. - **[#10577](https://github.com/kim-em/hex-dev/issues/10577):** closed by merged [#10860](https://github.com/kim-em/hex-dev/pull/10860). All four Sturm/real-algebraic inputs reached Phase 4. The readiness matrix retains computational coverage, finding dispositions, source provenance and practical isolation costs. The [direct Sturm oracle](sturm-direct-conformance/README.md) supplies the owning SPECs' rational selected-root sign fixtures without treating inherited integer tests as independent frontend coverage. The Sturm [proof acceptance](sturm-proof-acceptance.md) records Phases 5–7 for both libraries, using the [individual API/manual assessment](sturm-declaration-review/README.md) and complete native comparison; real-algebraic Phases 5–7 remain outside the eight-library polishing scope. - **[#10377](https://github.com/kim-em/hex-dev/issues/10377):** closed by merged [#10861](https://github.com/kim-em/hex-dev/pull/10861). Both sign-determination libraries completed owner Phase 4; implementation, correspondence, certificate interfaces, direct examples, independent conformance and retained performance evidence are delivered. Their [proof acceptance](sign-det-proof-acceptance.md) records Phase 5. SignDet Phases 6–7 belong to #10575. -- **[#10378](https://github.com/kim-em/hex-dev/issues/10378):** general dependency-closed interleaved normalization and simultaneous ordinary-real realization; integration of constructed provider histories with generic interleaved reconstruction; the general direct `Sample.realizeReplay` theorem and composition with factory models/inclusions; automatic reached arithmetic, zero-packing and selected-sign inventory assembly; direct computed operand/product-law requests; successful multilevel native joint reconstruction; full serialization/exploration and specified conformance/performance evidence and acceptance. The finite reconstruction section supplies usable merged contracts; #10914 supplies native test evidence through the existing catalog APIs. The original CADE `tower8` and clean/eager obligations remain conditional on caller π/e procedures and laws; the required-evidence versus unsupported-case decision remains open. Neither reduced inputs nor reconstructed paper sources attest Phase 4. +- **[#10378](https://github.com/kim-em/hex-dev/issues/10378):** general dependency-closed interleaved normalization and simultaneous ordinary-real realization; integration of constructed provider histories with generic interleaved reconstruction; the general direct `Sample.realizeReplay` theorem and composition with factory models/inclusions; automatic reached arithmetic, zero-packing and selected-sign inventory assembly; general computed operand/product-law assembly and multilevel native reconstruction beyond the fixed nested joint fixture; full serialization/exploration and specified conformance/performance evidence and acceptance. The finite reconstruction section supplies usable merged contracts; #10914 supplies native test evidence through the existing catalog APIs. The original CADE `tower8` and clean/eager obligations remain conditional on caller π/e procedures and laws; the required-evidence versus unsupported-case decision remains open. Neither reduced inputs nor reconstructed paper sources attest Phase 4. - **[#10358](https://github.com/kim-em/hex-dev/issues/10358):** generic frontend source/provider/history certification, reached-data and all-live assembly, accepted general algebraic production and completeness, automatic common-field irreducibility certification, and complete consumption of nested/successive-infinitesimal joint realization. Supplied root-table, inverse/divisor and cell contracts from #10907/#10912/#10922 use explicit lawful-model and accepted-evidence hypotheses. Independent complete-packet replay from merged [#10942](https://github.com/kim-em/hex-dev/pull/10942) removes the supplied-`RootReplay.Result` premise but keeps the lawful parent model. Its `NumberField.cells_complete` additionally proves actual packet production and both original-coordinate verdicts for one selected number field, without a child-success premise. General frontend/provider assembly, automatic common-field certification and missing-predecessor reconstruction remain open; the delivered single-field producer must not be recorded as merely supplied-cell acceptance. The [#10858](https://github.com/kim-em/hex-dev/pull/10858) supplied inverse contract binds the original operand/source and divisor guards under a supplied lawful ordinary-real predecessor model. The [#10867](https://github.com/kim-em/hex-dev/pull/10867) `NativeFormula` evaluator is not identified with `Samples.run` or `Tower.Sample.signs`, and frozen context/history/reached-data assembly into the tactic path remains incomplete. `NativeSamples.row_converted` separately connects sample signs to `NativeSpecialize.row`; full native/infinitesimal root coverage remains open. Reconcile the owning RCF SPEC and root-replay report passages with the merged coverage/order and cell interfaces. External unshipped prototypes are not merged acceptance evidence. Reuse the owner's existing API/manual examples. - **[#10575](https://github.com/kim-em/hex-dev/issues/10575):** final integrated acceptance and all applicable Phases 5–7 for the eight family libraries. The separately limited [package-preparation result](real-closure-package-inventory.json) remains an open #10575 obligation.