# Sturm–Tarski source attribution The files in `LeanCanny/Algebra/Sturm/` and `LeanCanny/Algebra/PrincipalSubresultant/` adapt proofs by Kim Morrison and The Tau Ceti contributors from [TauCeti](https://github.com/TauCetiProject/TauCeti) at revision `034e577c895d28c058d92af4036f7ce0b03081cf`, inspected on 2026-10-19. The original copyright and Apache 2.0 notices are retained in each file; the [Apache 2.0 license](LICENSE) applies to this code. | Local file | Upstream source | | --- | --- | | [`SignVariations.lean`](LeanCanny/Algebra/Sturm/SignVariations.lean) | [`Data/List/SignVariations.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Data/List/SignVariations.lean) | | [`Jumps.lean`](LeanCanny/Algebra/Sturm/Jumps.lean) | [`Data/Finset/Jumps.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Data/Finset/Jumps.lean) | | [`RealSigns.lean`](LeanCanny/Algebra/Sturm/RealSigns.lean) | [`Algebra/Polynomial/RealClosed/Sign.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/RealClosed/Sign.lean) | | [`Signs.lean`](LeanCanny/Algebra/Sturm/Signs.lean) | [`Algebra/Polynomial/Sturm/Signs.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/Sturm/Signs.lean) | | [`Local.lean`](LeanCanny/Algebra/Sturm/Local.lean) | [`Algebra/Polynomial/Sturm/Local.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/Sturm/Local.lean) | | [`Sequence.lean`](LeanCanny/Algebra/Sturm/Sequence.lean) | [`Algebra/Polynomial/Sturm/Sequence.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/Sturm/Sequence.lean) | | [`SignedRemainders.lean`](LeanCanny/Algebra/Sturm/SignedRemainders.lean) | [`Algebra/Polynomial/Sturm/SignedRemainders.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/Sturm/SignedRemainders.lean) | | [`Sum.lean`](LeanCanny/Algebra/Sturm/Sum.lean) | [`Algebra/Polynomial/Sturm/Sum.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/Sturm/Sum.lean) | | [`Tarski.lean`](LeanCanny/Algebra/Sturm/Tarski.lean) | [`Algebra/Polynomial/Sturm/Tarski.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/Sturm/Tarski.lean) | | [`EvalInfinity.lean`](LeanCanny/Algebra/Sturm/EvalInfinity.lean) | [`Algebra/Polynomial/Eval/Infinity.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/Eval/Infinity.lean) | | [`Infinity.lean`](LeanCanny/Algebra/Sturm/Infinity.lean) | [`Algebra/Polynomial/Sturm/Infinity.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/Sturm/Infinity.lean) | | [`Sturm/Parity.lean`](LeanCanny/Algebra/Sturm/Parity.lean) | [`Data/SignType/Parity.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Data/SignType/Parity.lean) | | [`Sturm/Index.lean`](LeanCanny/Algebra/Sturm/Index.lean) | Recurrence proof adapted from [`Sturm/CauchyIndex/Sequence.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/Sturm/CauchyIndex/Sequence.lean) | | [`PrincipalSubresultant/Coeff.lean`](LeanCanny/Algebra/PrincipalSubresultant/Coeff.lean) | [`Algebra/Polynomial/Coeff/Basic.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/Coeff/Basic.lean) | | [`PrincipalSubresultant/Permutation.lean`](LeanCanny/Algebra/PrincipalSubresultant/Permutation.lean) | [`GroupTheory/Perm/Inversion.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/GroupTheory/Perm/Inversion.lean) | | [`PrincipalSubresultant/Basic.lean`](LeanCanny/Algebra/PrincipalSubresultant/Basic.lean) | [`RingTheory/Polynomial/Subresultant/Basic.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/RingTheory/Polynomial/Subresultant/Basic.lean) | | [`PrincipalSubresultant/Polynomial.lean`](LeanCanny/Algebra/PrincipalSubresultant/Polynomial.lean) | [`RingTheory/Polynomial/Subresultant/Polynomial.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/RingTheory/Polynomial/Subresultant/Polynomial.lean) | | [`PrincipalSubresultant/Corner.lean`](LeanCanny/Algebra/PrincipalSubresultant/Corner.lean) | [`LinearAlgebra/Matrix/CornerMinor.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/LinearAlgebra/Matrix/CornerMinor.lean) | | [`PrincipalSubresultant/DegreeDrop.lean`](LeanCanny/Algebra/PrincipalSubresultant/DegreeDrop.lean) | [`RingTheory/Polynomial/Subresultant/DegreeDrop/Basic.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/RingTheory/Polynomial/Subresultant/DegreeDrop/Basic.lean) | | [`PrincipalSubresultant/Choose.lean`](LeanCanny/Algebra/PrincipalSubresultant/Choose.lean) | [`Data/Nat/Choose/Basic.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Data/Nat/Choose/Basic.lean) | | [`PrincipalSubresultant/Signed.lean`](LeanCanny/Algebra/PrincipalSubresultant/Signed.lean) | [`RingTheory/Polynomial/Subresultant/Signed.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/RingTheory/Polynomial/Subresultant/Signed.lean) | | [`PrincipalSubresultant/OfFn.lean`](LeanCanny/Algebra/PrincipalSubresultant/OfFn.lean) | [`Algebra/Polynomial/OfFn.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Algebra/Polynomial/OfFn.lean) | | [`PrincipalSubresultant/Euclidean.lean`](LeanCanny/Algebra/PrincipalSubresultant/Euclidean.lean) | [`RingTheory/Polynomial/Subresultant/Euclidean.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/RingTheory/Polynomial/Subresultant/Euclidean.lean) | | [`PrincipalSubresultant/Permanences.lean`](LeanCanny/Algebra/PrincipalSubresultant/Permanences.lean) | [`Data/List/PermanencesMinusVariations.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Data/List/PermanencesMinusVariations.lean) | | [`PrincipalSubresultant/Range.lean`](LeanCanny/Algebra/PrincipalSubresultant/Range.lean) | [`Data/List/Range.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/Data/List/Range.lean) | | [`PrincipalSubresultant/Query.lean`](LeanCanny/Algebra/PrincipalSubresultant/Query.lean) | [`RingTheory/Polynomial/Subresultant/CauchyIndex.lean`](https://github.com/TauCetiProject/TauCeti/blob/034e577c895d28c058d92af4036f7ce0b03081cf/TauCeti/RingTheory/Polynomial/Subresultant/CauchyIndex.lean) | The adaptation uses the project's existing Lean and Mathlib pins rather than adding a TauCeti dependency. All adapted declarations live in `LeanCanny.Algebra.Sturm` or `LeanCanny.Algebra.PrincipalSubresultant`, so they are included in the project axiom audit. Changes include: - Keep the list-variation recurrence and scaling law, the finite jump-sum lemma, and only the second-entry lookup from the upstream sequence extensions. - Keep the constant-sign and simple-root-crossing lemmas. Prove constant signs over ℝ using Mathlib's intermediate value theorem, avoiding the abstract real-closed-field development and the one-sided endpoint API. - Specialize the analytic chain and Tarski theorems to ℝ. The signed remainder identities and the removal of common factors still work over ordered fields. - Prove the whole-line theorem directly from the finite-interval theorem by choosing endpoints beyond every chain root. Retain the leading-coefficient and degree-parity formulas at infinity; omit the half-line formulas. - Rename helper declarations into the project namespace and adapt imports and proofs to the pinned Mathlib. [`SturmQuery.lean`](LeanCanny/Algebra/SturmQuery.lean) is the project bridge: coefficient maps preserve signed remainder sequences and their sign variations, rational-input queries agree with the sum of signs at distinct real roots, and these formulas substitute into the scaled sign-pattern count. The signed-principal-coefficient slice additionally keeps the Euclidean reduction and degree-drop identities, the zero-gap permanences-minus-variations statistic, and their correctness formula. It omits reducta/specialization results, keeps only the needed corner-minor Laplace expansion and binomial identity, and avoids an analytic Cauchy-index dependency. `Sturm.remainderIndex` is defined directly by coefficient variations; its recurrence and the subresultant formula work over ordered fields. The local permanences-minus-variations module also exposes the zero-gap weight and a continuation recurrence. The project uses this API to prove the streaming accumulator in `SignStatistic.lean` and its encoded space bound in `SignStatisticSpace.lean`; these two modules are new project proofs. [`PrincipalSubresultant/Minor.lean`](LeanCanny/Algebra/PrincipalSubresultant/Minor.lean) is the project's convention bridge: each principal matrix equals the existing Sylvester minor, including terminal indices, and the signed integer coefficients inherit its bit budget. [`PrincipalQuery.lean`](LeanCanny/Algebra/PrincipalQuery.lean) connects the determinant formula to real-root Tarski queries and sign-pattern counts, with rational and integer input specializations. These are kernel-checked mathematical correctness results. The reference uses Mathlib's noncomputable polynomial operations. The project modules `PrincipalCoefficientSpace.lean` and `PrincipalCoefficientQuery.lean` supply an encoded principal-sign pipeline from polynomial coefficient readers and FP degree metadata. `TarskiQuerySpace.lean` composes it with computed actual degrees and the original head/query coefficient readers, with full space/clock certificates. The full ETR decision procedure and its critical-point correctness proof remain open.