feat: root identity, the deferred two-circle statement, and companion conformance#8753
Merged
Conversation
… conformance Add HexRealRootsMathlib/SimpleRealRoot.lean (theRoot, overlaps_iff_same_root, SimpleRealRoot.toReal/toReal_isRoot/toReal_injective, sameRoot_iff), HexRealRootsMathlib/TwoCircle.lean (the deferred isolateDescartes?_isSome behind the Obreshkoff two-circle prerequisite — the library's one intentional sorry), and conformance/HexRealRootsMathlib/Conformance.lean (the companion conformance module). Rename the M5 Sturm helpers, bump HexRealRootsMathlib done_through to 1, and wire the two new files into the umbrella. See progress/2026-07-11T19-27-49Z-real-roots-s8-wrapup.md. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NUB5EStJpJ8CPqMkNw7Qjz
SquareFreeRat 0 holds vacuously, so the nonzero hypothesis is required; matches the driver-completeness precedent. Per Codex review of #8753. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NUB5EStJpJ8CPqMkNw7Qjz
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR completes the HexRealRootsMathlib scaffold with the root-identity theorems, the deferred Descartes-termination statement, and the companion conformance module.
SimpleRealRoot.leanproves thatOverlapsclasses onRefinedRealIsolationare exactly the real roots:overlaps_iff_same_root(forward by the separation boundsepPrec_separates', backward by common-root interval containment),SimpleRealRoot.toRealwithtoReal_isRootandtoReal_injective, andsameRoot_iffdeciding equality in the quotient.theRootis the unique root fromRealRootIsolation.exists_unique_root.TwoCircle.leanstatesisolateDescartes?_isSomebehind its Obreshkoff two-circle prerequisite; this is the library's one intentionalsorry, and its docstring records the obligation that whichever PR discharges it must delete the Descartes stand-in assertions inconformance/HexRealRoots/Conformance.lean. The companion conformance module ties the executableHex.rootCountto Mathlibroots.cardon committed fixtures through the proven correspondence theorems, with a full formal tie onx - 5. It also renames the M5 Sturm helpers (exists_left_gap/exists_right_gap,chain_head_mem, privatecard_filter_Ioc_split), bumpsHexRealRootsMathlibdone_throughto 1, and wires the new files into the umbrella.The
SimpleRealRoottheorems match the SPEC signatures verbatim: they carry onlySquareFreeRat p, withp != 0derived internally from the isolation'scount_one(viadegree_pos_of_count_one), unlikeisolates/isolateSturm?_isSomewhich have no isolation on hand and so must assumep != 0.🤖 Prepared with Claude Code