diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md index 23c8a6443..0bea138fb 100644 --- a/ARCHITECTURE.md +++ b/ARCHITECTURE.md @@ -632,18 +632,15 @@ and its elementary endpoint consequences. The root-count transport first, then the finite-gap invariant, then the left/right Theorem 2.1 branch predicate. `Theorem21Statements.CommonRootDeletion` owns the independent shared-factor reduction, and `Theorem21Statements.Interfaces` -combines the two branches into the theorem-shaped targets and implication -wrappers. The historical `Theorem21Statements` path remains a compatibility +keeps only the refuted published forward direction beside its checked +negation. The historical `Theorem21Statements` path remains a compatibility facade, and consumers needing only the predicate import `NoCommonRoots` directly. -`LiuOppositeSigns.FactorReturnAssembly` is a compatibility facade over the -factor-return theorem route. `LeftDegreeCases` owns the translated and -x-subtraction realizations of the three left deletion branches; -`RightDegreeCases` obtains the symmetric right branches and their endpoint -specializations; `PredicateDegreeCases` combines both orientations under -lower-endpoint predicates; and `DegreeCaseAssembly` packages the final six-case -factor-return principle. +`LiuOppositeSigns.FactorReturnAssembly` proves the reverse direction of +Theorem 2.1. `FactorReturnLeft` and `FactorReturnTwoDegree` reduce the three +degree cases of a left deletion branch to the positive-split x-subtraction +pencils of `XSub.IntervalRootCount`; the right branch follows by symmetry. `LiuOppositeSigns.XSub.ProperPosition` is a narrow bridge from the ordinary positive-leading `StrictInterl` interface to Liu's positive root-count package. It diff --git a/RealRooted.lean b/RealRooted.lean index 8d14f8ff7..fe06696af 100644 --- a/RealRooted.lean +++ b/RealRooted.lean @@ -538,17 +538,11 @@ import RealRooted.LinearPowerFamily import RealRooted.LiuOppositeSigns import RealRooted.LiuOppositeSigns.BoundedIntervalContinuity import RealRooted.LiuOppositeSigns.CommonInterleaverConsequences -import RealRooted.LiuOppositeSigns.Corollary22 import RealRooted.LiuOppositeSigns.DeletionBranches import RealRooted.LiuOppositeSigns.DerivativeShiftRegularization import RealRooted.LiuOppositeSigns.DerivativeShiftSequenceRegularization import RealRooted.LiuOppositeSigns.FactorReturnAssembly -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.DegreeCaseAssembly -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.LeftDegreeCases -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.PredicateDegreeCases -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.RightDegreeCases import RealRooted.LiuOppositeSigns.FactorReturnLeft -import RealRooted.LiuOppositeSigns.FactorReturnStatements import RealRooted.LiuOppositeSigns.FactorReturnTwoDegree import RealRooted.LiuOppositeSigns.ForwardCubicLinear import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.Average @@ -571,7 +565,6 @@ import RealRooted.LiuOppositeSigns.RootCount import RealRooted.LiuOppositeSigns.RootCountClosure import RealRooted.LiuOppositeSigns.RootCountRelStability import RealRooted.LiuOppositeSigns.RootDeletion -import RealRooted.LiuOppositeSigns.Theorem21Assembly import RealRooted.LiuOppositeSigns.Theorem21Statements import RealRooted.LiuOppositeSigns.Theorem21Statements.CommonRootDeletion import RealRooted.LiuOppositeSigns.Theorem21Statements.Interfaces diff --git a/RealRooted/Challenges/LiuOppositeSigns.lean b/RealRooted/Challenges/LiuOppositeSigns.lean index f4855bd5d..950c92265 100644 --- a/RealRooted/Challenges/LiuOppositeSigns.lean +++ b/RealRooted/Challenges/LiuOppositeSigns.lean @@ -132,7 +132,7 @@ theorem compatible_iff_rootCount_of_noCommonRoots {f g : ℝ[X]} (hf : f.Splits) (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) : Compatible f g ↔ ∃ r s, LeftRootCountBranch f g r s ∨ RightRootCountBranch f g r s := - theorem21CompatibleRootCountNoCommonNonconstant f g hf hg hsgn hno hf_deg hg_deg + theorem21CompatibleRootCountNoCommonNonconstant hf hg hsgn hno hf_deg hg_deg /-- Without the common-root branch, the forward direction fails (for `X` and `-X ^ 2`). -/ @@ -147,7 +147,7 @@ differing by at most two. -/ theorem natDegree_diff_le_two {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 := - corollary22DegreeDiff_proof f g hf hg hsgn hcompat + corollary22DegreeDiff hf hg hsgn hcompat end LiuOppositeSigns end Challenges diff --git a/RealRooted/LiuOppositeSigns/CommonInterleaverConsequences.lean b/RealRooted/LiuOppositeSigns/CommonInterleaverConsequences.lean index 45d5b89b0..91ffe99ce 100644 --- a/RealRooted/LiuOppositeSigns/CommonInterleaverConsequences.lean +++ b/RealRooted/LiuOppositeSigns/CommonInterleaverConsequences.lean @@ -1,11 +1,11 @@ import RealRooted.CommonInterleaverTwo -import RealRooted.LiuOppositeSigns.Corollary22 +import RealRooted.LiuOppositeSigns.ForwardLowDegree /-! # Liu common-interleaver consequences This module contains the positive-deletion and branch-retaining -common-interleaver consequences derived from Liu Theorem 2.1 packages. +common-interleaver consequences of Liu's root-count branches. -/ open Polynomial @@ -59,82 +59,6 @@ theorem theorem21PositiveDeletionCompatibleBranches_of_theorem21RootCountBranche hsgn (theorem21DeletionPairCommonInterleaverBranches_of_theorem21RootCountBranches hf_splits hg_splits hsgn h) -/-- Projection form of the isolated branch-retaining deletion-pair -common-interleaver forward direction. -/ -theorem theorem21DeletionPairCommonInterleaverBranches_of_compatible_of_commonForward - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : - theorem21DeletionPairCommonInterleaverBranches f g := - hforward hf hg hsgn hcompat - -/-- The isolated branch-retaining deletion-pair common-interleaver forward -direction supplies normalized deletion compatibility branches. -/ -theorem theorem21PositiveDeletionCompatibleBranches_of_compatible_of_commonForward - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : - theorem21PositiveDeletionCompatibleBranches f g := - theorem21PositiveDeletionCompatibleBranches_of_deletionPairCommonInterleaverBranches - hsgn - (theorem21DeletionPairCommonInterleaverBranches_of_compatible_of_commonForward - hforward hf hg hsgn hcompat) - -/-- The isolated forward direction of Liu Theorem 2.1 supplies normalized -deletion compatibility branches. -/ -theorem theorem21PositiveDeletionCompatibleBranches_of_compatible_of_forward - (hforward : theorem21CompatibleToRootCountBranchesStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : - theorem21PositiveDeletionCompatibleBranches f g := - theorem21PositiveDeletionCompatibleBranches_of_compatible_of_commonForward - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - hf hg hsgn hcompat - -/-- The forward direction of Liu Theorem 2.1 supplies normalized deletion -compatibility branches. -/ -theorem theorem21PositiveDeletionCompatibleBranches_of_compatible - (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hcompat : Compatible f g) : - theorem21PositiveDeletionCompatibleBranches f g := - theorem21PositiveDeletionCompatibleBranches_of_compatible_of_forward - (theorem21CompatibleToRootCountBranches_of_theorem21CompatibleRootCount h) - hf hg hsgn hcompat - -/-- The isolated forward direction of Liu Theorem 2.1 supplies -branch-retaining common interleaver witnesses for the actual deletion pair. -/ -theorem theorem21DeletionPairCommonInterleaverBranches_of_compatible_of_forward - (hforward : theorem21CompatibleToRootCountBranchesStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : - theorem21DeletionPairCommonInterleaverBranches f g := - theorem21DeletionPairCommonInterleaverBranches_of_compatible_of_commonForward - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - hf hg hsgn hcompat - -/-- The forward direction of Liu Theorem 2.1 supplies branch-retaining common -interleaver witnesses for the actual deletion pair. -/ -theorem theorem21DeletionPairCommonInterleaverBranches_of_compatible - (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hcompat : Compatible f g) : - theorem21DeletionPairCommonInterleaverBranches f g := - theorem21DeletionPairCommonInterleaverBranches_of_compatible_of_forward - (theorem21CompatibleToRootCountBranches_of_theorem21CompatibleRootCount h) - hf hg hsgn hcompat - -/-- Liu Theorem 2.1, restated with branch-retaining deletion-pair -common-interleaver witnesses. -/ -theorem compatible_iff_theorem21DeletionPairCommonInterleaverBranches - (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) : - Compatible f g ↔ theorem21DeletionPairCommonInterleaverBranches f g := - (theorem21DeletionPairCommonInterleaverIff_of_theorem21CompatibleRootCount - h) f g hf hg hsgn - /-- The two positive-split root-count leaves supply the existing positive-leading compatibility-to-common-interleaver bridge. -/ theorem diff --git a/RealRooted/LiuOppositeSigns/Corollary22.lean b/RealRooted/LiuOppositeSigns/Corollary22.lean deleted file mode 100644 index 8605c5040..000000000 --- a/RealRooted/LiuOppositeSigns/Corollary22.lean +++ /dev/null @@ -1,290 +0,0 @@ -import RealRooted.LiuOppositeSigns.ForwardLowDegree - -/-! -# Liu bounded theorem packages - -This module contains bounded endpoint and low-degree theorem packages derived -from the reverse assembly for Liu Theorem 2.1. --/ - -open Polynomial Filter - -namespace RealRooted -namespace LiuOppositeSigns - -/-- Bounded Liu Theorem 2.1 package through endpoint degree two. The forward -direction is the ordinary Liu forward direction, while the reverse direction is -restricted to branch data whose selected lower-degree endpoint has degree at -most two. -/ -def theorem21CompatibleRootCountEndpointLeTwoStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - (Compatible f g → theorem21RootCountBranches f g) ∧ - (theorem21RootCountBranchesEndpointLeTwo f g → Compatible f g) - -/-- Nonconstant bounded Liu Theorem 2.1 package through endpoint degree two. --/ -def theorem21CompatibleRootCountEndpointLeTwoNonconstantStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - (Compatible f g → theorem21RootCountBranches f g) ∧ - (theorem21RootCountBranchesEndpointLeTwo f g → Compatible f g) - -/-- Bounded Liu Theorem 2.1 package through endpoint degree three. The forward -direction is the ordinary Liu forward direction, while the reverse direction is -restricted to branch data whose selected lower-degree endpoint has degree at -most three. -/ -def theorem21CompatibleRootCountEndpointLeThreeStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - (Compatible f g → theorem21RootCountBranches f g) ∧ - (theorem21RootCountBranchesEndpointLeThree f g → Compatible f g) - -/-- Nonconstant bounded Liu Theorem 2.1 package through endpoint degree three. --/ -def theorem21CompatibleRootCountEndpointLeThreeNonconstantStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - (Compatible f g → theorem21RootCountBranches f g) ∧ - (theorem21RootCountBranchesEndpointLeThree f g → Compatible f g) - -/-- Low-degree Liu Theorem 2.1 package through endpoint degree three, stated -with the ordinary branch predicate and explicit endpoint degree bounds. -/ -def theorem21CompatibleRootCountNatDegreeLeThreeStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≤ 3 → g.natDegree ≤ 3 → - (Compatible f g ↔ theorem21RootCountBranches f g) - -/-- Nonconstant low-degree Liu Theorem 2.1 package through endpoint degree -three, stated with the ordinary branch predicate and explicit endpoint degree -bounds. -/ -def theorem21CompatibleRootCountNatDegreeLeThreeNonconstantStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - f.natDegree ≤ 3 → g.natDegree ≤ 3 → - (Compatible f g ↔ theorem21RootCountBranches f g) - -/-- Low-degree Liu Theorem 2.1 package through endpoint degree two, stated -with the ordinary branch predicate and explicit endpoint degree bounds. -/ -def theorem21CompatibleRootCountNatDegreeLeTwoStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≤ 2 → g.natDegree ≤ 2 → - (Compatible f g ↔ theorem21RootCountBranches f g) - -/-- Nonconstant low-degree Liu Theorem 2.1 package through endpoint degree -two, stated with the ordinary branch predicate and explicit endpoint degree -bounds. -/ -def theorem21CompatibleRootCountNatDegreeLeTwoNonconstantStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - f.natDegree ≤ 2 → g.natDegree ≤ 2 → - (Compatible f g ↔ theorem21RootCountBranches f g) - -/-- Nonconstant no-common-root low-degree Liu Theorem 2.1 package through -endpoint degree two. -/ -def theorem21CompatibleRootCountNatDegreeLeTwoNoCommonNonconstantStatement : - Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - NoCommonRoots f g → f.natDegree ≠ 0 → g.natDegree ≠ 0 → - f.natDegree ≤ 2 → g.natDegree ≤ 2 → - (Compatible f g ↔ theorem21RootCountBranches f g) - -/-- Nonconstant no-common-root low-degree forward direction through endpoint -degree two. -/ -def theorem21CompatibleToRootCountBranchesNatDegreeLeTwoNoCommonNonconstantStatement : - Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - NoCommonRoots f g → f.natDegree ≠ 0 → g.natDegree ≠ 0 → - f.natDegree ≤ 2 → g.natDegree ≤ 2 → - Compatible f g → theorem21RootCountBranches f g - -/-- Corrected nonconstant low-degree Liu package through endpoint degree two, -using an explicit common-root deletion branch in the conclusion. -/ -def theorem21CompatibleRootCountWithCommonNatDegreeLeTwoNonconstantStatement : - Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - f.natDegree ≤ 2 → g.natDegree ≤ 2 → - (Compatible f g ↔ theorem21RootCountBranchesWithCommon f g) - -/-- Corrected nonconstant low-degree forward direction through endpoint degree -two, with an explicit common-root deletion branch. -/ -def - theorem21CompatibleToRootCountBranchesWithCommonNatDegreeLeTwoNonconstantStatement : - Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - f.natDegree ≤ 2 → g.natDegree ≤ 2 → - Compatible f g → theorem21RootCountBranchesWithCommon f g - -/-- Low-degree bounded Liu equivalence through endpoint degree two, assuming -the isolated forward direction. -/ -theorem theorem21CompatibleRootCountNatDegreeLeTwo_of_forward - (hforward : theorem21CompatibleToRootCountBranchesStatement) : - theorem21CompatibleRootCountNatDegreeLeTwoStatement := by - intro f g hf hg hsgn hfdeg hgdeg - constructor - · exact hforward hf hg hsgn - · intro hbranches - exact theorem21RootCountBranchesToCompatible_of_natDegree_le_two - hf hg hsgn hfdeg hgdeg hbranches - -/-- The nonconstant no-common-root low-degree forward direction through -endpoint degree two is checked directly. -/ -theorem theorem21CompatibleToRootCountBranchesNatDegreeLeTwoNoCommonNonconstant : - theorem21CompatibleToRootCountBranchesNatDegreeLeTwoNoCommonNonconstantStatement := - by - intro f g hf hg hsgn hno hfdeg_ne hgdeg_ne hfdeg hgdeg hcompat - exact theorem21RootCountBranches_of_compatible_natDegree_le_two_of_no_common - hf hg hsgn hcompat hno hfdeg_ne hgdeg_ne hfdeg hgdeg - -/-- The nonconstant no-common-root low-degree Liu equivalence through endpoint -degree two is fully checked. -/ -theorem theorem21CompatibleRootCountNatDegreeLeTwoNoCommonNonconstant : - theorem21CompatibleRootCountNatDegreeLeTwoNoCommonNonconstantStatement := by - intro f g hf hg hsgn hno hfdeg_ne hgdeg_ne hfdeg hgdeg - constructor - · exact - theorem21CompatibleToRootCountBranchesNatDegreeLeTwoNoCommonNonconstant - f g hf hg hsgn hno hfdeg_ne hgdeg_ne hfdeg hgdeg - · intro hbranches - exact theorem21RootCountBranchesToCompatibleNonconstant_of_natDegree_le_two - hf hg hsgn hfdeg_ne hgdeg_ne hfdeg hgdeg hbranches - -/-- The corrected nonconstant low-degree forward direction through endpoint -degree two follows from the no-common forward theorem and the automatic -common-root deletion branch. -/ -theorem - theorem21CompatibleToRootCountBranchesWithCommonNatDegreeLeTwoNonconstant : - theorem21CompatibleToRootCountBranchesWithCommonNatDegreeLeTwoNonconstantStatement := - by - intro f g hf hg hsgn hfdeg_ne hgdeg_ne hfdeg hgdeg hcompat - by_cases hno : NoCommonRoots f g - · exact Or.inl - (theorem21CompatibleToRootCountBranchesNatDegreeLeTwoNoCommonNonconstant - f g hf hg hsgn hno hfdeg_ne hgdeg_ne hfdeg hgdeg hcompat) - · exact Or.inr - (CommonRootDeletionCompatibleBranch.of_compatible_of_not_noCommonRoots - hcompat hno) - -/-- The corrected nonconstant low-degree Liu equivalence through endpoint -degree two is fully checked, with common roots handled by an explicit deletion -branch. -/ -theorem theorem21CompatibleRootCountWithCommonNatDegreeLeTwoNonconstant : - theorem21CompatibleRootCountWithCommonNatDegreeLeTwoNonconstantStatement := by - intro f g hf hg hsgn hfdeg_ne hgdeg_ne hfdeg hgdeg - constructor - · exact - theorem21CompatibleToRootCountBranchesWithCommonNatDegreeLeTwoNonconstant - f g hf hg hsgn hfdeg_ne hgdeg_ne hfdeg hgdeg - · intro hbranches - rcases hbranches with hbranches | hcommon - · exact theorem21RootCountBranchesToCompatibleNonconstant_of_natDegree_le_two - hf hg hsgn hfdeg_ne hgdeg_ne hfdeg hgdeg hbranches - · exact CommonRootDeletionCompatibleBranch.compatible hcommon - -/-- The bounded endpoint-degree-three package restricts to the ordinary -low-degree statement with explicit endpoint degree bounds. -/ -theorem theorem21CompatibleRootCountNatDegreeLeThree_of_endpointLeThree - (h : theorem21CompatibleRootCountEndpointLeThreeStatement) : - theorem21CompatibleRootCountNatDegreeLeThreeStatement := by - intro f g hf hg hsgn hfdeg hgdeg - constructor - · exact (h f g hf hg hsgn).1 - · intro hbranches - exact (h f g hf hg hsgn).2 - (theorem21RootCountBranchesEndpointLeThree_of_natDegree_le_three - hfdeg hgdeg hbranches) - -/-- The bounded endpoint-degree-three package restricts to the nonconstant -bounded endpoint-degree-three package. -/ -theorem theorem21CompatibleRootCountEndpointLeThreeNonconstant_of_endpointLeThree - (h : theorem21CompatibleRootCountEndpointLeThreeStatement) : - theorem21CompatibleRootCountEndpointLeThreeNonconstantStatement := by - intro f g hf hg hsgn _hfdeg_ne _hgdeg_ne - exact h f g hf hg hsgn - -/-- The ordinary low-degree Liu package restricts to its nonconstant form. -/ -theorem theorem21CompatibleRootCountNatDegreeLeThreeNonconstant_of_natDegreeLeThree - (h : theorem21CompatibleRootCountNatDegreeLeThreeStatement) : - theorem21CompatibleRootCountNatDegreeLeThreeNonconstantStatement := by - intro f g hf hg hsgn _hfdeg_ne _hgdeg_ne hfdeg hgdeg - exact h f g hf hg hsgn hfdeg hgdeg - -/-- The bounded endpoint-degree-three nonconstant package restricts to the -ordinary nonconstant low-degree statement with explicit endpoint degree bounds. --/ -theorem - theorem21CompatibleRootCountNatDegreeLeThreeNonconstant_of_endpointLeThreeNonconstant - (h : theorem21CompatibleRootCountEndpointLeThreeNonconstantStatement) : - theorem21CompatibleRootCountNatDegreeLeThreeNonconstantStatement := by - intro f g hf hg hsgn hfdeg_ne hgdeg_ne hfdeg hgdeg - constructor - · exact (h f g hf hg hsgn hfdeg_ne hgdeg_ne).1 - · intro hbranches - exact (h f g hf hg hsgn hfdeg_ne hgdeg_ne).2 - (theorem21RootCountBranchesEndpointLeThree_of_natDegree_le_three - hfdeg hgdeg hbranches) - -/-- The bounded endpoint-degree-three package restricts directly to the -ordinary nonconstant low-degree statement. -/ -theorem theorem21CompatibleRootCountNatDegreeLeThreeNonconstant_of_endpointLeThree - (h : theorem21CompatibleRootCountEndpointLeThreeStatement) : - theorem21CompatibleRootCountNatDegreeLeThreeNonconstantStatement := - theorem21CompatibleRootCountNatDegreeLeThreeNonconstant_of_natDegreeLeThree - (theorem21CompatibleRootCountNatDegreeLeThree_of_endpointLeThree h) - -/-- Liu Corollary 2.2: compatible real-rooted polynomials with opposite leading -signs have degree gap at most two. -/ -def corollary22DegreeDiffStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - Compatible f g → |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 - -/-- Low-degree form of Liu Corollary 2.2 through endpoint degree three. -/ -def corollary22DegreeDiffNatDegreeLeThreeStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≤ 3 → g.natDegree ≤ 3 → - Compatible f g → |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 - -/-- Nonconstant low-degree form of Liu Corollary 2.2 through endpoint degree -three. -/ -def corollary22DegreeDiffNatDegreeLeThreeNonconstantStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - f.natDegree ≤ 3 → g.natDegree ≤ 3 → - Compatible f g → |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 - -/-- Projection form of `corollary22DegreeDiffStatement`. -/ -theorem corollary22DegreeDiff - (h : corollary22DegreeDiffStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hcompat : Compatible f g) : - |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 := - h f g hf hg hsgn hcompat - -/-- Liu Corollary 2.2 follows from the isolated branch-retaining -common-interleaver forward direction. -/ -theorem corollary22DegreeDiff_of_commonForward - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) : - corollary22DegreeDiffStatement := - fun _ _ hf hg hsgn hcompat => - natDegree_abs_sub_le_two_of_theorem21RootCountBranches hf hg hsgn - (theorem21RootCountBranches_of_deletionPairCommonInterleaverBranches - (hforward hf hg hsgn hcompat)) - -/-- Liu Corollary 2.2 follows from the isolated forward direction of -Theorem 2.1. -/ -theorem corollary22DegreeDiff_of_forward - (hforward : theorem21CompatibleToRootCountBranchesStatement) : - corollary22DegreeDiffStatement := - corollary22DegreeDiff_of_commonForward - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - -/-- Liu Corollary 2.2 follows from the Theorem 2.1 compatibility criterion. -/ -theorem corollary22DegreeDiff_of_theorem21CompatibleRootCount - (h : theorem21CompatibleRootCountStatement) : - corollary22DegreeDiffStatement := - corollary22DegreeDiff_of_forward - (theorem21CompatibleToRootCountBranches_of_theorem21CompatibleRootCount h) - -end LiuOppositeSigns -end RealRooted diff --git a/RealRooted/LiuOppositeSigns/DeletionBranches.lean b/RealRooted/LiuOppositeSigns/DeletionBranches.lean index 26b86c7cf..a9d45d1a7 100644 --- a/RealRooted/LiuOppositeSigns/DeletionBranches.lean +++ b/RealRooted/LiuOppositeSigns/DeletionBranches.lean @@ -5,8 +5,8 @@ import RealRooted.LiuOppositeSigns.Theorem21Statements.Interfaces # Liu deletion-branch transport This module keeps Liu's left and right deletion branches together with -the branch-retaining common-interleaver package. The later factor-return -statement and assembly layers remain in `RealRooted.LiuOppositeSigns.Theorem`. +the branch-retaining common-interleaver package. The factor-return proof of +the reverse direction is in `RealRooted.LiuOppositeSigns.FactorReturnAssembly`. -/ open Polynomial Filter @@ -258,124 +258,5 @@ theorem theorem21DeletionPairCommonInterleaverBranches_iff_rootCountBranches theorem21DeletionPairCommonInterleaverBranches_of_theorem21RootCountBranches hf_splits hg_splits hsgn⟩ -/-- Forward half of Liu Theorem 2.1, restated with branch-retaining -deletion-pair common-interleaver witnesses. -/ -def theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement : - Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - Compatible f g → theorem21DeletionPairCommonInterleaverBranches f g - -/-- Nonconstant forward half of Liu Theorem 2.1, restated with -branch-retaining deletion-pair common-interleaver witnesses. -/ -def theorem21CompatibleToDeletionPairCommonInterleaverBranchesNonconstantStatement : - Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - Compatible f g → theorem21DeletionPairCommonInterleaverBranches f g - -/-- Reverse half of Liu Theorem 2.1, restated with branch-retaining -deletion-pair common-interleaver witnesses. -/ -def theorem21DeletionPairCommonInterleaverBranchesToCompatibleStatement : - Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - theorem21DeletionPairCommonInterleaverBranches f g → Compatible f g - -/-- Nonconstant reverse half of Liu Theorem 2.1, restated with -branch-retaining deletion-pair common-interleaver witnesses. -/ -def theorem21DeletionPairCommonInterleaverBranchesToCompatibleNonconstantStatement : - Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - theorem21DeletionPairCommonInterleaverBranches f g → Compatible f g - -/-- The isolated forward root-count direction supplies the branch-retaining -common-interleaver forward direction. -/ -theorem theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - (hforward : theorem21CompatibleToRootCountBranchesStatement) : - theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement := by - intro f g hf hg hsgn hcompat - exact theorem21DeletionPairCommonInterleaverBranches_of_theorem21RootCountBranches - hf hg hsgn (hforward hf hg hsgn hcompat) - -/-- The branch-retaining common-interleaver forward direction forgets back to -the root-count forward direction. -/ -theorem theorem21CompatibleToRootCountBranches_of_commonForward - (hforward : - theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) : - theorem21CompatibleToRootCountBranchesStatement := by - intro f g hf hg hsgn hcompat - exact theorem21RootCountBranches_of_deletionPairCommonInterleaverBranches - (hforward hf hg hsgn hcompat) - -/-- The isolated reverse root-count direction supplies the branch-retaining -common-interleaver reverse direction. -/ -theorem theorem21DeletionPairCommonInterleaverBranchesToCompatible_of_reverse - (hreverse : theorem21RootCountBranchesToCompatibleStatement) : - theorem21DeletionPairCommonInterleaverBranchesToCompatibleStatement := by - intro f g hf hg hsgn hbranches - exact hreverse hf hg hsgn - (theorem21RootCountBranches_of_deletionPairCommonInterleaverBranches - hbranches) - -/-- Liu Theorem 2.1 restated with branch-retaining deletion-pair -common-interleaver witnesses. -/ -def theorem21CompatibleDeletionPairCommonInterleaverBranchesStatement : - Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - (Compatible f g ↔ theorem21DeletionPairCommonInterleaverBranches f g) - -/-- Nonconstant Liu Theorem 2.1 restated with branch-retaining deletion-pair -common-interleaver witnesses. -/ -def theorem21CompatibleDeletionPairCommonInterleaverBranchesNonconstantStatement : - Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - (Compatible f g ↔ theorem21DeletionPairCommonInterleaverBranches f g) - -/-- Reassemble the branch-retaining common-interleaver theorem package from -its isolated forward and reverse directions. -/ -theorem theorem21CompatibleDeletionPairCommonInterleaverBranches_of_forward_and_reverse - (hforward : - theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - (hreverse : - theorem21DeletionPairCommonInterleaverBranchesToCompatibleStatement) : - theorem21CompatibleDeletionPairCommonInterleaverBranchesStatement := by - unfold theorem21CompatibleDeletionPairCommonInterleaverBranchesStatement - intro f g hf hg hsgn - exact ⟨hforward hf hg hsgn, hreverse hf hg hsgn⟩ - -/-- Liu's root-count theorem package gives the branch-retaining deletion-pair -common-interleaver iff package. -/ -theorem theorem21DeletionPairCommonInterleaverIff_of_theorem21CompatibleRootCount - (h : theorem21CompatibleRootCountStatement) : - theorem21CompatibleDeletionPairCommonInterleaverBranchesStatement := - theorem21CompatibleDeletionPairCommonInterleaverBranches_of_forward_and_reverse - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - (theorem21CompatibleToRootCountBranches_of_theorem21CompatibleRootCount - h)) - (theorem21DeletionPairCommonInterleaverBranchesToCompatible_of_reverse - (theorem21RootCountBranchesToCompatible_of_theorem21CompatibleRootCount - h)) - -/-- The branch-retaining deletion-pair common-interleaver iff implies Liu's -root-count theorem package. -/ -theorem theorem21CompatibleRootCount_of_deletionPairCommonInterleaverIff - (h : - theorem21CompatibleDeletionPairCommonInterleaverBranchesStatement) : - theorem21CompatibleRootCountStatement := by - intro f g hf hg hsgn - constructor - · intro hcompat - exact theorem21RootCountBranches_of_deletionPairCommonInterleaverBranches - ((h f g hf hg hsgn).1 hcompat) - · intro hbranches - exact (h f g hf hg hsgn).2 - (theorem21DeletionPairCommonInterleaverBranches_of_theorem21RootCountBranches - hf hg hsgn hbranches) - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/FactorReturnAssembly.lean b/RealRooted/LiuOppositeSigns/FactorReturnAssembly.lean index ba5138b40..94cbd2b6a 100644 --- a/RealRooted/LiuOppositeSigns/FactorReturnAssembly.lean +++ b/RealRooted/LiuOppositeSigns/FactorReturnAssembly.lean @@ -1,8 +1,59 @@ -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.DegreeCaseAssembly +import RealRooted.LiuOppositeSigns.FactorReturnLeft +import RealRooted.LiuOppositeSigns.FactorReturnTwoDegree +import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount /-! -# Liu factor-return case packages +# Liu reverse direction by factor return -Compatibility import for the left, right, predicate-restricted, and final -degree-case assembly layers. +A Liu root-count branch deletes the largest root of one endpoint. The deleted +pair then has degrees differing by at most one, so the restored pair falls in +one of three degree cases. In each case the translated positive right pencil +splits, which restores compatibility of the original pair. The right branch +follows from the left branch by symmetry. -/ + +open Polynomial Filter + +namespace RealRooted +namespace LiuOppositeSigns + +/-- A left Liu root-count branch gives compatibility. -/ +theorem LeftRootCountBranch.compatible {f g : ℝ[X]} {r s : ℝ} + (hleft : LeftRootCountBranch f g r s) + (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) : + Compatible f g := by + have hright : + ∀ μ : ℝ, 0 < μ → + (X * (deleteRootFactor f r).comp (X + C r) + + C μ * g.comp (X + C r)).Splits := by + rcases hleft.natDegree_eq_or_eq_succ_or_eq_succ_succ + hsgn.left_ne_zero hf hg with hdeg | hdeg | hdeg + · exact theorem21LeftFactorReturnSameDegreeTranslatedRightFamily + hf hg hsgn hleft hdeg + · exact theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily + hf hg hsgn hleft hdeg + · exact theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily + hf hg hsgn hleft hdeg + exact hleft.compatible_of_translated_restore + (theorem21LeftFactorReturnTranslatedCompatible_of_pointwiseRightFamily + hf hg hsgn hleft hright) + +/-- A right Liu root-count branch gives compatibility. -/ +theorem RightRootCountBranch.compatible {f g : ℝ[X]} {r s : ℝ} + (hright : RightRootCountBranch f g r s) + (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) : + Compatible f g := + (hright.toLeftBranch_symm.compatible hg hf hsgn.symm).comm + +/-- Reverse direction of Liu Theorem 2.1: either root-count branch gives +compatibility of an opposite-leading-sign pair of real-rooted polynomials. -/ +theorem compatible_of_theorem21RootCountBranches {f g : ℝ[X]} + (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) + (hbranches : theorem21RootCountBranches f g) : + Compatible f g := by + rcases hbranches with ⟨r, s, hleft | hright⟩ + · exact hleft.compatible hf hg hsgn + · exact hright.compatible hf hg hsgn + +end LiuOppositeSigns +end RealRooted diff --git a/RealRooted/LiuOppositeSigns/FactorReturnAssembly/DegreeCaseAssembly.lean b/RealRooted/LiuOppositeSigns/FactorReturnAssembly/DegreeCaseAssembly.lean deleted file mode 100644 index 1dace0793..000000000 --- a/RealRooted/LiuOppositeSigns/FactorReturnAssembly/DegreeCaseAssembly.lean +++ /dev/null @@ -1,197 +0,0 @@ -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.PredicateDegreeCases - -/-! -# Liu factor-return degree-case assembly - -This module assembles the six ordinary degree cases into the final deletion-pair -factor-return principle and its translated and x-subtraction consequences. --/ - -open Polynomial Filter - -namespace RealRooted -namespace LiuOppositeSigns - -/-- Degree-case split needed to prove the factor-return principle. -/ -def theorem21DeletionPairCommonInterleaverFactorReturnDegreeCasesStatement : - Prop := - theorem21LeftFactorReturnSameDegreeStatement ∧ - theorem21LeftFactorReturnSuccDegreeStatement ∧ - theorem21LeftFactorReturnTwoDegreeStatement ∧ - theorem21RightFactorReturnSameDegreeStatement ∧ - theorem21RightFactorReturnSuccDegreeStatement ∧ - theorem21RightFactorReturnTwoDegreeStatement - -/-- Left and right factor-return degree cases assemble into the full six-case -package. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturnDegreeCases_of_leftRightCases - (hleft : theorem21LeftFactorReturnDegreeCasesStatement) - (hright : theorem21RightFactorReturnDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnDegreeCasesStatement := - ⟨hleft.1, hleft.2.1, hleft.2.2, - hright.1, hright.2.1, hright.2.2⟩ - -/-- Left projection from a six-case ordinary factor-return package. -/ -theorem theorem21LeftFactorReturnDegreeCases_of_factorCases - (hcases : - theorem21DeletionPairCommonInterleaverFactorReturnDegreeCasesStatement) : - theorem21LeftFactorReturnDegreeCasesStatement := - ⟨hcases.1, hcases.2.1, hcases.2.2.1⟩ - -/-- Right projection from a six-case ordinary factor-return package. -/ -theorem theorem21RightFactorReturnDegreeCases_of_factorCases - (hcases : - theorem21DeletionPairCommonInterleaverFactorReturnDegreeCasesStatement) : - theorem21RightFactorReturnDegreeCasesStatement := - ⟨hcases.2.2.2.1, hcases.2.2.2.2.1, hcases.2.2.2.2.2⟩ - -/-- All-combinations factor-return degree cases give the corresponding -compatibility factor-return degree cases. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturnDegreeCases_of_allComboDegreeCases - (hcases : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnDegreeCasesStatement := - theorem21DeletionPairCommonInterleaverFactorReturnDegreeCases_of_leftRightCases - (theorem21LeftFactorReturnDegreeCases_of_allComboCases - (theorem21LeftFactorReturnAllComboDegreeCases_of_allComboFactorCases - hcases)) - (theorem21RightFactorReturnDegreeCases_of_allComboCases - (theorem21RightFactorReturnAllComboDegreeCases_of_allComboFactorCases - hcases)) - -/-- Left factor-return degree cases supply all six left/right cases by -symmetry. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturnDegreeCases_of_leftCases - (hcases : theorem21LeftFactorReturnDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnDegreeCasesStatement := - theorem21DeletionPairCommonInterleaverFactorReturnDegreeCases_of_leftRightCases - hcases - (theorem21RightFactorReturnDegreeCases_of_leftCases hcases) - -/-- The explicit factor-return principle follows from its six restored-degree -cases. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_degreeCases - (hcases : - theorem21DeletionPairCommonInterleaverFactorReturnDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := by - let hleftCases := theorem21LeftFactorReturnDegreeCases_of_factorCases hcases - let hrightCases := theorem21RightFactorReturnDegreeCases_of_factorCases hcases - intro f g r s hf hg hsgn - constructor - · intro hleft hcommon - rcases hleft.natDegree_eq_or_eq_succ_or_eq_succ_succ - hsgn.left_ne_zero hf hg with hdeg | hdeg | hdeg - · exact hleftCases.1 hf hg hsgn hleft hdeg hcommon - · exact hleftCases.2.1 hf hg hsgn hleft hdeg hcommon - · exact hleftCases.2.2 hf hg hsgn hleft hdeg hcommon - · intro hright hcommon - rcases hright.natDegree_eq_or_eq_succ_or_eq_succ_succ - hsgn.right_ne_zero hf hg with hdeg | hdeg | hdeg - · exact hrightCases.1 hf hg hsgn hright hdeg hcommon - · exact hrightCases.2.1 hf hg hsgn hright hdeg hcommon - · exact hrightCases.2.2 hf hg hsgn hright hdeg hcommon - -/-- It is enough to prove the left-branch factor-return cases; the right branch -is symmetric. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_leftCases - (hcases : theorem21LeftFactorReturnDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := - theorem21DeletionPairCommonInterleaverFactorReturn_of_degreeCases - (theorem21DeletionPairCommonInterleaverFactorReturnDegreeCases_of_leftCases - hcases) - -/-- All-combinations factor-return degree cases imply the compatibility -factor-return principle used by the reverse direction. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_allComboDegreeCases - (hcases : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := - theorem21DeletionPairCommonInterleaverFactorReturn_of_degreeCases - (theorem21DeletionPairCommonInterleaverFactorReturnDegreeCases_of_allComboDegreeCases - hcases) - -/-- Left all-combinations factor-return degree cases imply the compatibility -factor-return principle used by the reverse direction. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_leftAllComboCases - (hcases : theorem21LeftFactorReturnAllComboDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := - theorem21DeletionPairCommonInterleaverFactorReturn_of_leftCases - (theorem21LeftFactorReturnDegreeCases_of_allComboCases hcases) - -/-- A bundled sign-normalized positive-split x-subtraction case package -implies the factor-return principle used by the reverse direction. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_xSubCasePackage - (hcases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := - theorem21DeletionPairCommonInterleaverFactorReturn_of_leftCases - (theorem21LeftFactorReturnDegreeCases_of_xSubCasePackage - hcases) - -/-- Sign-normalized positive-split x-subtraction cases imply the -factor-return principle used by the reverse direction. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_xSubCases - (hrightSucc : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement) - (hsame : positiveSplitSameDegreeTranslatedXSubRightFamilyStatement) - (hleftSucc : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := - theorem21DeletionPairCommonInterleaverFactorReturn_of_xSubCasePackage - ⟨hrightSucc, hsame, hleftSucc⟩ - -/-- Since the same-degree and left-successor x-subtraction cases are proved, the -reverse factor-return principle only needs the remaining right-successor -x-subtraction leaf. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_rightSucc_xSub - (hrightSucc : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := - theorem21DeletionPairCommonInterleaverFactorReturn_of_xSubCases - hrightSucc positiveSplitSameDegreeTranslatedXSubRightFamily - positiveSplitLeftSuccDegreeTranslatedXSubRightFamily - -/-- The proved sign-normalized positive-split x-subtraction cases imply the -factor-return principle used by the reverse direction. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_xSub : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := - theorem21DeletionPairCommonInterleaverFactorReturn_of_xSubCasePackage - positiveSplitTranslatedXSubRightFamilyDegreeCases - -/-- The factor-return principle follows from same/succ left leaves and the -translated two-degree compatibility target. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_sameSucc_and_translatedTwo - (hsame : theorem21LeftFactorReturnSameDegreeStatement) - (hsucc : theorem21LeftFactorReturnSuccDegreeStatement) - (htwo : theorem21LeftFactorReturnTwoDegreeTranslatedCompatibleStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := - theorem21DeletionPairCommonInterleaverFactorReturn_of_leftCases - (theorem21LeftFactorReturnDegreeCases_of_sameSucc_and_translatedTwo - hsame hsucc htwo) - -/-- The factor-return principle follows from same/succ left leaves and the -translated right-family two-degree target. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_sameSucc_and_rightFamily - (hsame : theorem21LeftFactorReturnSameDegreeStatement) - (hsucc : theorem21LeftFactorReturnSuccDegreeStatement) - (hright : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := - theorem21DeletionPairCommonInterleaverFactorReturn_of_leftCases - (theorem21LeftFactorReturnDegreeCases_of_sameSucc_and_rightFamily - hsame hsucc hright) - -/-- The factor-return principle follows from same/succ left leaves and the -sign-normalized positive-split subtraction-family leaf. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_sameSucc_and_xSub - (hsame : theorem21LeftFactorReturnSameDegreeStatement) - (hsucc : theorem21LeftFactorReturnSuccDegreeStatement) - (hsub : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := - theorem21DeletionPairCommonInterleaverFactorReturn_of_sameSucc_and_rightFamily - hsame hsucc - (theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_xSub hsub) - -end LiuOppositeSigns -end RealRooted diff --git a/RealRooted/LiuOppositeSigns/FactorReturnAssembly/LeftDegreeCases.lean b/RealRooted/LiuOppositeSigns/FactorReturnAssembly/LeftDegreeCases.lean deleted file mode 100644 index 04b5943d5..000000000 --- a/RealRooted/LiuOppositeSigns/FactorReturnAssembly/LeftDegreeCases.lean +++ /dev/null @@ -1,166 +0,0 @@ -import RealRooted.LiuOppositeSigns.FactorReturnLeft -import RealRooted.LiuOppositeSigns.FactorReturnTwoDegree -import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount - -/-! -# Liu left factor-return degree cases - -This module assembles the translated compatibility, right-family, and -x-subtraction routes for the three left deletion-branch degree cases. --/ - -open Polynomial Filter - -namespace RealRooted -namespace LiuOppositeSigns - -/-- The three left-branch factor-return cases. The right-branch cases follow -by symmetry. -/ -def theorem21LeftFactorReturnDegreeCasesStatement : Prop := - theorem21LeftFactorReturnSameDegreeStatement ∧ - theorem21LeftFactorReturnSuccDegreeStatement ∧ - theorem21LeftFactorReturnTwoDegreeStatement - -/-- Sign-normalized positive-split x-subtraction cases for the three Liu -left-branch restored-degree cases. -/ -def positiveSplitTranslatedXSubRightFamilyDegreeCasesStatement : Prop := - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement ∧ - positiveSplitSameDegreeTranslatedXSubRightFamilyStatement ∧ - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement - -/-- Predicate-restricted sign-normalized positive-split x-subtraction cases -for the three Liu left-branch restored-degree cases. -/ -def positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement - (P : ℕ → Prop) : Prop := - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement P ∧ - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement P ∧ - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement P - -/-- Since the same-degree and left-successor x-subtraction cases are now proved, -the remaining unrestricted x-subtraction case package only needs the -right-successor leaf. -/ -theorem positiveSplitTranslatedXSubRightFamilyDegreeCases_of_rightSucc - (hrightSucc : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement) : - positiveSplitTranslatedXSubRightFamilyDegreeCasesStatement := - ⟨hrightSucc, positiveSplitSameDegreeTranslatedXSubRightFamily, - positiveSplitLeftSuccDegreeTranslatedXSubRightFamily⟩ - -/-- The three sign-normalized positive-split x-subtraction cases are proved. -/ -theorem positiveSplitTranslatedXSubRightFamilyDegreeCases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesStatement := - positiveSplitTranslatedXSubRightFamilyDegreeCases_of_rightSucc - positiveSplitRightSuccDegreeTranslatedXSubRightFamily - -/-- Since the same-degree and left-successor x-subtraction cases are now proved, -predicate-restricted x-subtraction case packages only need the right-successor -leaf. -/ -theorem positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate_of_rightSucc - {P : ℕ → Prop} - (hrightSucc : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) : - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement P := - ⟨hrightSucc, positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate P, - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate⟩ - -/-- The three sign-normalized positive-split x-subtraction cases are proved for -every endpoint predicate restriction. -/ -theorem positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate - {P : ℕ → Prop} : - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement P := - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate_of_rightSucc - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate - -/-- Endpoint cases through degree two as a bundled predicate-restricted -x-subtraction case package. -/ -theorem positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate_of_endpoint_le_two : - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement - (fun n => n ≤ 2) := - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate_of_rightSucc - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_two - -/-- Endpoint cases through degree three as a bundled predicate-restricted -x-subtraction case package, modulo the normalized monic quartic/cubic leaf. -/ -theorem - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate_of_endpoint_le_three_of_monic - (hmono : xSubQuarticCubicSplitsStatement) : - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement - (fun n => n ≤ 3) := - ⟨positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_three, - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_three, - positiveSplitLeftSuccXSubFamilyPredicate_of_right_natDegree_le_three_of_monic - hmono⟩ - -/-- Endpoint cases through degree three as a bundled predicate-restricted -x-subtraction case package. -/ -theorem positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate_of_endpoint_le_three : - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement - (fun n => n ≤ 3) := - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate_of_endpoint_le_three_of_monic - xSubQuarticCubicSplits - -/-- Left all-combinations factor-return degree cases give the corresponding -compatibility factor-return degree cases. -/ -theorem theorem21LeftFactorReturnDegreeCases_of_allComboCases - (hcases : theorem21LeftFactorReturnAllComboDegreeCasesStatement) : - theorem21LeftFactorReturnDegreeCasesStatement := - ⟨theorem21LeftFactorReturnSameDegree_of_allCombo hcases.1, - theorem21LeftFactorReturnSuccDegree_of_allCombo hcases.2.1, - theorem21LeftFactorReturnTwoDegree_of_allCombo hcases.2.2⟩ - -/-- Sign-normalized positive-split x-subtraction cases give the three original -left-branch factor-return cases directly. -/ -theorem theorem21LeftFactorReturnDegreeCases_of_xSubCases - (hrightSucc : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement) - (hsame : positiveSplitSameDegreeTranslatedXSubRightFamilyStatement) - (hleftSucc : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21LeftFactorReturnDegreeCasesStatement := - ⟨theorem21LeftFactorReturnSameDegree_of_xSub hrightSucc, - theorem21LeftFactorReturnSuccDegree_of_xSub hsame, - theorem21LeftFactorReturnTwoDegree_of_xSub hleftSucc⟩ - -/-- A bundled sign-normalized positive-split x-subtraction case package gives -the three original left-branch factor-return cases. -/ -theorem theorem21LeftFactorReturnDegreeCases_of_xSubCasePackage - (hcases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesStatement) : - theorem21LeftFactorReturnDegreeCasesStatement := - theorem21LeftFactorReturnDegreeCases_of_xSubCases - hcases.1 hcases.2.1 hcases.2.2 - -/-- Same-degree and succ-degree leaves plus the translated two-degree target -give the full left-branch factor-return case package. -/ -theorem theorem21LeftFactorReturnDegreeCases_of_sameSucc_and_translatedTwo - (hsame : theorem21LeftFactorReturnSameDegreeStatement) - (hsucc : theorem21LeftFactorReturnSuccDegreeStatement) - (htwo : theorem21LeftFactorReturnTwoDegreeTranslatedCompatibleStatement) : - theorem21LeftFactorReturnDegreeCasesStatement := - ⟨hsame, hsucc, - theorem21LeftFactorReturnTwoDegree_of_translatedCompatible htwo⟩ - -/-- Same-degree and succ-degree leaves plus the translated right-family -two-degree target give the full left-branch factor-return case package. -/ -theorem theorem21LeftFactorReturnDegreeCases_of_sameSucc_and_rightFamily - (hsame : theorem21LeftFactorReturnSameDegreeStatement) - (hsucc : theorem21LeftFactorReturnSuccDegreeStatement) - (hright : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyStatement) : - theorem21LeftFactorReturnDegreeCasesStatement := - ⟨hsame, hsucc, theorem21LeftFactorReturnTwoDegree_of_rightFamily hright⟩ - -/-- Same-degree and succ-degree leaves plus the positive-split subtraction -family leaf give the full left-branch factor-return case package. -/ -theorem theorem21LeftFactorReturnDegreeCases_of_sameSucc_and_xSub - (hsame : theorem21LeftFactorReturnSameDegreeStatement) - (hsucc : theorem21LeftFactorReturnSuccDegreeStatement) - (hsub : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21LeftFactorReturnDegreeCasesStatement := - theorem21LeftFactorReturnDegreeCases_of_sameSucc_and_rightFamily hsame hsucc - (theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_xSub hsub) - -end LiuOppositeSigns -end RealRooted diff --git a/RealRooted/LiuOppositeSigns/FactorReturnAssembly/PredicateDegreeCases.lean b/RealRooted/LiuOppositeSigns/FactorReturnAssembly/PredicateDegreeCases.lean deleted file mode 100644 index ed8946cc8..000000000 --- a/RealRooted/LiuOppositeSigns/FactorReturnAssembly/PredicateDegreeCases.lean +++ /dev/null @@ -1,254 +0,0 @@ -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.RightDegreeCases - -/-! -# Liu predicate-restricted factor-return degree cases - -This module combines the left and right degree cases under predicates on the -lower-degree endpoint and packages the low-degree x-subtraction routes. --/ - -open Polynomial Filter - -namespace RealRooted -namespace LiuOppositeSigns - -/-- Predicate-restricted factor-return principle for Liu deletion branches. -The predicate is imposed on the lower-degree endpoint only in the two-degree -branch: on `g.natDegree` in a left branch and on `f.natDegree` in a right -branch. -/ -def theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement - (P : ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - (LeftRootCountBranch f g r s → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - P g.natDegree → Compatible f g) ∧ - (RightRootCountBranch f g r s → - (∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) → - P f.natDegree → Compatible f g) - -/-- Predicate-restricted left factor-return degree cases. -/ -def theorem21LeftFactorReturnDegreeCasesPredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnSameDegreeStatement ∧ - theorem21LeftFactorReturnSuccDegreeStatement ∧ - theorem21LeftFactorReturnTwoDegreePredicateStatement P - -/-- Endpoint-predicate-restricted left factor-return degree cases. Unlike -`theorem21LeftFactorReturnDegreeCasesPredicateStatement`, the predicate is -available in all three degree branches. -/ -def theorem21LeftFactorReturnEndpointDegreeCasesPredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnSameDegreePredicateStatement P ∧ - theorem21LeftFactorReturnSuccDegreePredicateStatement P ∧ - theorem21LeftFactorReturnTwoDegreePredicateStatement P - -/-- Predicate-restricted right factor-return degree cases. -/ -def theorem21RightFactorReturnDegreeCasesPredicateStatement - (P : ℕ → Prop) : Prop := - theorem21RightFactorReturnSameDegreeStatement ∧ - theorem21RightFactorReturnSuccDegreeStatement ∧ - theorem21RightFactorReturnTwoDegreePredicateStatement P - -/-- Endpoint-predicate-restricted right factor-return degree cases. Unlike -`theorem21RightFactorReturnDegreeCasesPredicateStatement`, the predicate is -available in all three degree branches. -/ -def theorem21RightFactorReturnEndpointDegreeCasesPredicateStatement - (P : ℕ → Prop) : Prop := - theorem21RightFactorReturnSameDegreePredicateStatement P ∧ - theorem21RightFactorReturnSuccDegreePredicateStatement P ∧ - theorem21RightFactorReturnTwoDegreePredicateStatement P - -/-- Endpoint-predicate-restricted left and right factor-return degree cases. -/ -def theorem21EndpointFactorReturnPredicateDegreeCasesStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnSameDegreePredicateStatement P ∧ - theorem21LeftFactorReturnSuccDegreePredicateStatement P ∧ - theorem21LeftFactorReturnTwoDegreePredicateStatement P ∧ - theorem21RightFactorReturnSameDegreePredicateStatement P ∧ - theorem21RightFactorReturnSuccDegreePredicateStatement P ∧ - theorem21RightFactorReturnTwoDegreePredicateStatement P - -/-- Endpoint-predicate-restricted left and right factor-return degree cases -assemble into the full six-case package. -/ -theorem theorem21EndpointFactorReturnPredicateDegreeCases_of_leftRightCases - {P : ℕ → Prop} - (hleft : theorem21LeftFactorReturnEndpointDegreeCasesPredicateStatement P) - (hright : - theorem21RightFactorReturnEndpointDegreeCasesPredicateStatement P) : - theorem21EndpointFactorReturnPredicateDegreeCasesStatement P := - ⟨hleft.1, hleft.2.1, hleft.2.2, - hright.1, hright.2.1, hright.2.2⟩ - -/-- Left projection from a six-case endpoint-predicate factor-return package. -/ -theorem theorem21LeftFactorReturnEndpointDegreeCasesPredicate_of_endpointFactorCases - {P : ℕ → Prop} - (hcases : theorem21EndpointFactorReturnPredicateDegreeCasesStatement P) : - theorem21LeftFactorReturnEndpointDegreeCasesPredicateStatement P := - ⟨hcases.1, hcases.2.1, hcases.2.2.1⟩ - -/-- Right projection from a six-case endpoint-predicate factor-return package. -/ -theorem theorem21RightFactorReturnEndpointDegreeCasesPredicate_of_endpointFactorCases - {P : ℕ → Prop} - (hcases : theorem21EndpointFactorReturnPredicateDegreeCasesStatement P) : - theorem21RightFactorReturnEndpointDegreeCasesPredicateStatement P := - ⟨hcases.2.2.2.1, hcases.2.2.2.2.1, hcases.2.2.2.2.2⟩ - -/-- Predicate-restricted positive-split x-subtraction degree cases give -predicate-restricted original left factor-return degree cases. -/ -theorem theorem21LeftFactorReturnEndpointDegreeCasesPredicate_of_xSubCasesPredicate - {P : ℕ → Prop} - (hrightSucc : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) - (hsame : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement P) - (hleftSucc : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnEndpointDegreeCasesPredicateStatement P := - ⟨theorem21LeftFactorReturnSameDegreePredicate_of_xSubPredicate hrightSucc, - theorem21LeftFactorReturnSuccDegreePredicate_of_xSubPredicate hsame, - theorem21LeftFactorReturnTwoDegreePredicate_of_xSubPredicate hleftSucc⟩ - -/-- Bundled predicate-restricted positive-split x-subtraction cases give -predicate-restricted original left factor-return degree cases. -/ -theorem theorem21LeftFactorReturnEndpointDegreeCasesPredicate_of_xSubCasePackage - {P : ℕ → Prop} - (hcases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement P) : - theorem21LeftFactorReturnEndpointDegreeCasesPredicateStatement P := - theorem21LeftFactorReturnEndpointDegreeCasesPredicate_of_xSubCasesPredicate - hcases.1 hcases.2.1 hcases.2.2 - -/-- Endpoint-predicate-restricted left factor-return degree cases supply the -matching right cases by symmetry. -/ -theorem theorem21RightFactorReturnEndpointDegreeCasesPredicate_of_leftCases - {P : ℕ → Prop} - (hcases : - theorem21LeftFactorReturnEndpointDegreeCasesPredicateStatement P) : - theorem21RightFactorReturnEndpointDegreeCasesPredicateStatement P := - ⟨theorem21RightFactorReturnSameDegreePredicate_of_leftPredicate hcases.1, - theorem21RightFactorReturnSuccDegreePredicate_of_leftPredicate hcases.2.1, - theorem21RightFactorReturnTwoDegreePredicate_of_leftPredicate hcases.2.2⟩ - -/-- Endpoint-predicate-restricted left factor-return degree cases supply the -matching right cases by symmetry. -/ -theorem theorem21EndpointFactorReturnPredicateDegreeCases_of_leftCases - {P : ℕ → Prop} - (hcases : - theorem21LeftFactorReturnEndpointDegreeCasesPredicateStatement P) : - theorem21EndpointFactorReturnPredicateDegreeCasesStatement P := - theorem21EndpointFactorReturnPredicateDegreeCases_of_leftRightCases - hcases - (theorem21RightFactorReturnEndpointDegreeCasesPredicate_of_leftCases - hcases) - -/-- The predicate-restricted factor-return principle follows from endpoint- -predicate-restricted restored degree cases. -/ -theorem theorem21FactorReturnPredicate_of_endpointDegreeCases - {P : ℕ → Prop} - (hcases : - theorem21EndpointFactorReturnPredicateDegreeCasesStatement P) : - theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement P := by - let hleftCases := - theorem21LeftFactorReturnEndpointDegreeCasesPredicate_of_endpointFactorCases - hcases - let hrightCases := - theorem21RightFactorReturnEndpointDegreeCasesPredicate_of_endpointFactorCases - hcases - intro f g r s hf hg hsgn - constructor - · intro hleft hcommon hgdeg - rcases hleft.natDegree_eq_or_eq_succ_or_eq_succ_succ - hsgn.left_ne_zero hf hg with hdeg | hdeg | hdeg - · exact hleftCases.1 hf hg hsgn hleft hdeg hcommon hgdeg - · exact hleftCases.2.1 hf hg hsgn hleft hdeg hcommon hgdeg - · exact hleftCases.2.2 hf hg hsgn hleft hdeg hcommon hgdeg - · intro hright hcommon hfdeg - rcases hright.natDegree_eq_or_eq_succ_or_eq_succ_succ - hsgn.right_ne_zero hf hg with hdeg | hdeg | hdeg - · exact hrightCases.1 hf hg hsgn hright hdeg hcommon hfdeg - · exact hrightCases.2.1 hf hg hsgn hright hdeg hcommon hfdeg - · exact hrightCases.2.2 hf hg hsgn hright hdeg hcommon hfdeg - -/-- It is enough to prove endpoint-predicate-restricted left factor-return -degree cases; the right branch is symmetric. -/ -theorem theorem21FactorReturnPredicate_of_leftEndpointCases - {P : ℕ → Prop} - (hcases : - theorem21LeftFactorReturnEndpointDegreeCasesPredicateStatement P) : - theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement P := - theorem21FactorReturnPredicate_of_endpointDegreeCases - (theorem21EndpointFactorReturnPredicateDegreeCases_of_leftCases hcases) - -/-- Predicate-restricted positive-split x-subtraction degree cases imply the -predicate-restricted factor-return principle. -/ -theorem theorem21FactorReturnPredicate_of_xSubCasesPredicate - {P : ℕ → Prop} - (hrightSucc : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) - (hsame : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement P) - (hleftSucc : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) : - theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement P := - theorem21FactorReturnPredicate_of_leftEndpointCases - (theorem21LeftFactorReturnEndpointDegreeCasesPredicate_of_xSubCasesPredicate - hrightSucc hsame hleftSucc) - -/-- Since the same-degree and left-successor x-subtraction cases are proved, the -predicate-restricted factor-return principle only needs the remaining -right-successor x-subtraction leaf. -/ -theorem theorem21FactorReturnPredicate_of_rightSucc_xSubPredicate - {P : ℕ → Prop} - (hrightSucc : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) : - theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement P := - theorem21FactorReturnPredicate_of_xSubCasesPredicate - hrightSucc (positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate P) - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate - -/-- Bundled predicate-restricted positive-split x-subtraction cases imply the -predicate-restricted factor-return principle. -/ -theorem theorem21FactorReturnPredicate_of_xSubCasePackage - {P : ℕ → Prop} - (hcases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement P) : - theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement P := - theorem21FactorReturnPredicate_of_leftEndpointCases - (theorem21LeftFactorReturnEndpointDegreeCasesPredicate_of_xSubCasePackage - hcases) - -/-- A `P := True` restricted factor-return principle gives the unrestricted -factor-return principle. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_predicate_true - (hreturn : - theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement - (fun _ => True)) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := by - intro f g r s hf hg hsgn - constructor - · intro hleft hcommon - exact (hreturn hf hg hsgn).1 hleft hcommon trivial - · intro hright hcommon - exact (hreturn hf hg hsgn).2 hright hcommon trivial - -/-- The unrestricted factor-return principle proves every predicate-restricted -factor-return principle by forgetting the endpoint predicate. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturnPredicate_of_factorReturn - {P : ℕ → Prop} - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement P := by - intro f g r s hf hg hsgn - constructor - · intro hleft hcommon _hgdeg - exact (hreturn hf hg hsgn).1 hleft hcommon - · intro hright hcommon _hfdeg - exact (hreturn hf hg hsgn).2 hright hcommon - -end LiuOppositeSigns -end RealRooted diff --git a/RealRooted/LiuOppositeSigns/FactorReturnAssembly/RightDegreeCases.lean b/RealRooted/LiuOppositeSigns/FactorReturnAssembly/RightDegreeCases.lean deleted file mode 100644 index f0b6e9fec..000000000 --- a/RealRooted/LiuOppositeSigns/FactorReturnAssembly/RightDegreeCases.lean +++ /dev/null @@ -1,289 +0,0 @@ -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.LeftDegreeCases - -/-! -# Liu right factor-return degree cases - -This module obtains the right deletion-branch degree cases from the left cases -by symmetry and packages their endpoint-degree specializations. --/ - -open Polynomial Filter - -namespace RealRooted -namespace LiuOppositeSigns - -/-- Right-branch factor-return target for an arbitrary endpoint degree -relation. The relation is evaluated as `R g.natDegree f.natDegree`, matching -the right branch where `g` is the endpoint with the deleted root. -/ -def theorem21RightFactorReturnRelationStatement - (R : ℕ → ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - RightRootCountBranch f g r s → - R g.natDegree f.natDegree → - (∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) → - Compatible f g - -/-- Predicate-restricted right-branch factor-return target for an arbitrary -endpoint degree relation. The predicate records endpoint side conditions on -`f.natDegree`, the endpoint used by the right branch. -/ -def theorem21RightFactorReturnPredicateRelationStatement - (R : ℕ → ℕ → Prop) (P : ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - RightRootCountBranch f g r s → - R g.natDegree f.natDegree → - (∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) → - P f.natDegree → Compatible f g - -/-- A `P := True` right factor-return predicate relation target gives the -unrestricted relation target. -/ -theorem theorem21RightFactorReturnRelation_of_predicate_true - {R : ℕ → ℕ → Prop} - (hreturn : - theorem21RightFactorReturnPredicateRelationStatement R - (fun _ => True)) : - theorem21RightFactorReturnRelationStatement R := by - intro f g r s hf hg hsgn hright hdeg hcommon - exact hreturn hf hg hsgn hright hdeg hcommon trivial - -/-- Same-degree right-branch factor-return target. -/ -def theorem21RightFactorReturnSameDegreeStatement : Prop := - theorem21RightFactorReturnRelationStatement - (fun m n => m = n) - -/-- Succ-degree right-branch factor-return target. -/ -def theorem21RightFactorReturnSuccDegreeStatement : Prop := - theorem21RightFactorReturnRelationStatement - (fun m n => m = n + 1) - -/-- Two-degree-gap right-branch factor-return target. -/ -def theorem21RightFactorReturnTwoDegreeStatement : Prop := - theorem21RightFactorReturnRelationStatement - (fun m n => m = n + 2) - -/-- The three right-branch factor-return cases. -/ -def theorem21RightFactorReturnDegreeCasesStatement : Prop := - theorem21RightFactorReturnSameDegreeStatement ∧ - theorem21RightFactorReturnSuccDegreeStatement ∧ - theorem21RightFactorReturnTwoDegreeStatement - -/-- Predicate-restricted same-degree right-branch factor-return target. -The predicate records endpoint side conditions on `f.natDegree`, the endpoint -used by the right branch. -/ -def theorem21RightFactorReturnSameDegreePredicateStatement - (P : ℕ → Prop) : Prop := - theorem21RightFactorReturnPredicateRelationStatement - (fun m n => m = n) P - -/-- Predicate-restricted successor-degree right-branch factor-return target. -The predicate records endpoint side conditions on `f.natDegree`, the endpoint -used by the right branch. -/ -def theorem21RightFactorReturnSuccDegreePredicateStatement - (P : ℕ → Prop) : Prop := - theorem21RightFactorReturnPredicateRelationStatement - (fun m n => m = n + 1) P - -/-- A right all-combinations factor-return leaf for any degree relation gives -the corresponding compatibility factor-return leaf. -/ -theorem theorem21RightFactorReturn_of_allComboRelation - {R : ℕ → ℕ → Prop} - (hright : theorem21RightFactorReturnAllComboRelationStatement R) : - theorem21RightFactorReturnRelationStatement R := by - intro f g r s hf hg hsgn hbranch hdeg hcommon - exact Compatible.of_allComboRealRooted - (hright hf hg hsgn hbranch hdeg hcommon) - -/-- A same-degree all-combinations right leaf gives the corresponding -compatibility leaf. -/ -theorem theorem21RightFactorReturnSameDegree_of_allCombo - (hright : theorem21RightFactorReturnSameDegreeAllComboStatement) : - theorem21RightFactorReturnSameDegreeStatement := - theorem21RightFactorReturn_of_allComboRelation - (R := fun m n => m = n) hright - -/-- A successor-degree all-combinations right leaf gives the corresponding -compatibility leaf. -/ -theorem theorem21RightFactorReturnSuccDegree_of_allCombo - (hright : theorem21RightFactorReturnSuccDegreeAllComboStatement) : - theorem21RightFactorReturnSuccDegreeStatement := - theorem21RightFactorReturn_of_allComboRelation - (R := fun m n => m = n + 1) hright - -/-- A two-degree-gap all-combinations right leaf gives the corresponding -compatibility leaf. -/ -theorem theorem21RightFactorReturnTwoDegree_of_allCombo - (hright : theorem21RightFactorReturnTwoDegreeAllComboStatement) : - theorem21RightFactorReturnTwoDegreeStatement := - theorem21RightFactorReturn_of_allComboRelation - (R := fun m n => m = n + 2) hright - -/-- Right all-combinations factor-return degree cases give the corresponding -compatibility degree cases. -/ -theorem theorem21RightFactorReturnDegreeCases_of_allComboCases - (hcases : theorem21RightFactorReturnAllComboDegreeCasesStatement) : - theorem21RightFactorReturnDegreeCasesStatement := - ⟨theorem21RightFactorReturnSameDegree_of_allCombo hcases.1, - theorem21RightFactorReturnSuccDegree_of_allCombo hcases.2.1, - theorem21RightFactorReturnTwoDegree_of_allCombo hcases.2.2⟩ - -/-- Predicate-restricted two-degree-gap right-branch factor-return target. -The predicate records endpoint side conditions on `f.natDegree`, the -lower-degree endpoint in the right branch. -/ -def theorem21RightFactorReturnTwoDegreePredicateStatement - (P : ℕ → Prop) : Prop := - theorem21RightFactorReturnPredicateRelationStatement - (fun m n => m = n + 2) P - -/-- General symmetry bridge from a left-branch factor-return theorem to the -matching right-branch theorem with the degree relation reversed. -/ -theorem theorem21RightFactorReturn_of_leftDegreeRelation - {R : ℕ → ℕ → Prop} - (hleft : - ∀ {p q : ℝ[X]} {a b : ℝ}, - p.Splits → q.Splits → OppositeLeadingSigns p q → - LeftRootCountBranch p q a b → - R p.natDegree q.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor p a) k ∧ StrictInterl q k) → - Compatible p q) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hright : RightRootCountBranch f g r s) - (hdeg : R g.natDegree f.natDegree) - (hcommon : ∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) : - Compatible f g := - (hleft (p := g) (q := f) (a := s) (b := r) - hg hf hsgn.symm hright.toLeftBranch_symm hdeg - (rightDeletionPairCommonInterleaver_symm hcommon)).comm - -/-- The right same-degree factor-return case follows from the left same-degree -case by swapping the two polynomials. -/ -theorem theorem21RightFactorReturnSameDegree_of_leftSameDegree - (hleft : theorem21LeftFactorReturnSameDegreeStatement) : - theorem21RightFactorReturnSameDegreeStatement := by - intro f g r s hf hg hsgn hright hdeg hcommon - exact theorem21RightFactorReturn_of_leftDegreeRelation - (R := fun m n => m = n) hleft hf hg hsgn hright hdeg hcommon - -/-- Predicate-restricted same-degree left factor-return targets give the -corresponding right-branch predicate targets by symmetry. -/ -theorem theorem21RightFactorReturnSameDegreePredicate_of_leftPredicate - {P : ℕ → Prop} - (hleft : theorem21LeftFactorReturnSameDegreePredicateStatement P) : - theorem21RightFactorReturnSameDegreePredicateStatement P := by - intro f g r s hf hg hsgn hright hdeg hcommon hfdeg - exact theorem21RightFactorReturn_of_leftDegreeRelation - (R := fun m n => m = n ∧ P n) - (fun hp hq hsgn' hleft' hrel hcommon' => - hleft hp hq hsgn' hleft' hrel.1 hcommon' hrel.2) - hf hg hsgn hright ⟨hdeg, hfdeg⟩ hcommon - -/-- The right successor-degree factor-return case follows from the left -successor-degree case by swapping the two polynomials. -/ -theorem theorem21RightFactorReturnSuccDegree_of_leftSuccDegree - (hleft : theorem21LeftFactorReturnSuccDegreeStatement) : - theorem21RightFactorReturnSuccDegreeStatement := by - intro f g r s hf hg hsgn hright hdeg hcommon - exact theorem21RightFactorReturn_of_leftDegreeRelation - (R := fun m n => m = n + 1) hleft hf hg hsgn hright hdeg hcommon - -/-- Predicate-restricted successor-degree left factor-return targets give the -corresponding right-branch predicate targets by symmetry. -/ -theorem theorem21RightFactorReturnSuccDegreePredicate_of_leftPredicate - {P : ℕ → Prop} - (hleft : theorem21LeftFactorReturnSuccDegreePredicateStatement P) : - theorem21RightFactorReturnSuccDegreePredicateStatement P := by - intro f g r s hf hg hsgn hright hdeg hcommon hfdeg - exact theorem21RightFactorReturn_of_leftDegreeRelation - (R := fun m n => m = n + 1 ∧ P n) - (fun hp hq hsgn' hleft' hrel hcommon' => - hleft hp hq hsgn' hleft' hrel.1 hcommon' hrel.2) - hf hg hsgn hright ⟨hdeg, hfdeg⟩ hcommon - -/-- Predicate-parameterized symmetry bridge for right two-degree factor-return -cases. The predicate records endpoint restrictions such as degree `0`, degree -`1`, or degree `≤ 1` on the swapped right endpoint. -/ -theorem theorem21RightFactorReturnTwoDegree_of_leftPredicate - {P : ℕ → Prop} - (hleft : - ∀ {p q : ℝ[X]} {a b : ℝ}, - p.Splits → q.Splits → OppositeLeadingSigns p q → - LeftRootCountBranch p q a b → - p.natDegree = q.natDegree + 2 → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor p a) k ∧ StrictInterl q k) → - P q.natDegree → Compatible p q) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hright : RightRootCountBranch f g r s) - (hdeg : g.natDegree = f.natDegree + 2) - (hcommon : ∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) - (hfdeg : P f.natDegree) : - Compatible f g := - theorem21RightFactorReturn_of_leftDegreeRelation - (R := fun m n => m = n + 2 ∧ P n) - (fun hp hq hsgn' hleft' hrel hcommon' => - hleft hp hq hsgn' hleft' hrel.1 hcommon' hrel.2) - hf hg hsgn hright ⟨hdeg, hfdeg⟩ hcommon - -/-- Predicate-restricted left two-degree factor-return targets give the -corresponding right-branch predicate targets by symmetry. -/ -theorem theorem21RightFactorReturnTwoDegreePredicate_of_leftPredicate - {P : ℕ → Prop} - (hleft : theorem21LeftFactorReturnTwoDegreePredicateStatement P) : - theorem21RightFactorReturnTwoDegreePredicateStatement P := by - intro f g r s hf hg hsgn hright hdeg hcommon hfdeg - exact theorem21RightFactorReturnTwoDegree_of_leftPredicate - hleft hf hg hsgn hright hdeg hcommon hfdeg - -/-- A `P := True` right-branch factor-return predicate target gives the -unrestricted right two-degree factor-return target. -/ -theorem theorem21RightFactorReturnTwoDegree_of_predicate_true - (hright : - theorem21RightFactorReturnTwoDegreePredicateStatement - (fun _ => True)) : - theorem21RightFactorReturnTwoDegreeStatement := - theorem21RightFactorReturnRelation_of_predicate_true - (R := fun m n => m = n + 2) hright - -/-- The right two-degree-gap factor-return case follows from the left -two-degree-gap case by swapping the two polynomials. -/ -theorem theorem21RightFactorReturnTwoDegree_of_leftTwoDegree - (hleft : theorem21LeftFactorReturnTwoDegreeStatement) : - theorem21RightFactorReturnTwoDegreeStatement := - theorem21RightFactorReturnTwoDegree_of_predicate_true - (theorem21RightFactorReturnTwoDegreePredicate_of_leftPredicate - (P := fun _ => True) - (theorem21LeftFactorReturnTwoDegreePredicate_true_of_twoDegree hleft)) - -/-- Left factor-return degree cases give the matching right cases by symmetry. -/ -theorem theorem21RightFactorReturnDegreeCases_of_leftCases - (hcases : theorem21LeftFactorReturnDegreeCasesStatement) : - theorem21RightFactorReturnDegreeCasesStatement := - ⟨theorem21RightFactorReturnSameDegree_of_leftSameDegree hcases.1, - theorem21RightFactorReturnSuccDegree_of_leftSuccDegree hcases.2.1, - theorem21RightFactorReturnTwoDegree_of_leftTwoDegree hcases.2.2⟩ - -/-- Degree-two-left endpoint package for the right two-degree factor-return -target. -/ -theorem theorem21RightFactorReturnTwoDegreePredicate_of_left_natDegree_two : - theorem21RightFactorReturnTwoDegreePredicateStatement - (fun n => n = 2) := - theorem21RightFactorReturnTwoDegreePredicate_of_leftPredicate - (P := fun n => n = 2) - theorem21LeftFactorReturnTwoDegree_of_right_natDegree_two - -/-- Degree-two-left endpoint case for the right two-degree factor-return -leaf. -/ -theorem theorem21RightFactorReturnTwoDegree_of_left_natDegree_two - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hright : RightRootCountBranch f g r s) - (hdeg : g.natDegree = f.natDegree + 2) - (hcommon : ∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) - (hfdeg : f.natDegree = 2) : - Compatible f g := - theorem21RightFactorReturnTwoDegreePredicate_of_left_natDegree_two - hf hg hsgn hright hdeg hcommon hfdeg - -end LiuOppositeSigns -end RealRooted diff --git a/RealRooted/LiuOppositeSigns/FactorReturnLeft.lean b/RealRooted/LiuOppositeSigns/FactorReturnLeft.lean index 8cdc91a13..b957ad87e 100644 --- a/RealRooted/LiuOppositeSigns/FactorReturnLeft.lean +++ b/RealRooted/LiuOppositeSigns/FactorReturnLeft.lean @@ -1,12 +1,17 @@ -import RealRooted.LiuOppositeSigns.FactorReturnStatements +import RealRooted.LiuOppositeSigns.DeletionBranches import RealRooted.LiuOppositeSigns.XSub.QuadraticCubic import RealRooted.LiuOppositeSigns.XSub.CubicCubic +import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.RightSuccessor +import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.SameDegree /-! -# Liu left factor-return translated right-family wrappers +# Liu left factor return: same- and successor-degree cases -This module contains the same-degree and successor-degree translated -right-family wrappers for the left factor-return branch. +In a left Liu branch the largest root `r` of `f` is deleted. After translating +`r` to the origin and restoring the deleted factor as `X`, compatibility of the +restored pair follows once every positive right combination splits. In the +same-degree and successor-degree cases these combinations are the +positive-split x-subtraction pencils. -/ open Polynomial Filter @@ -14,19 +19,42 @@ open Polynomial Filter namespace RealRooted namespace LiuOppositeSigns -/-- A right-successor sign-normalized x-subtraction leaf gives the translated -right-family target for the same-degree Liu left branch. -/ -theorem theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_xSub_rightPredicate - {P : ℕ → Prop} - (hterminal : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) +/-- For a left Liu branch, if every positive right combination of the +translated restored pair splits, then that pair is compatible. -/ +theorem theorem21LeftFactorReturnTranslatedCompatible_of_pointwiseRightFamily {f g : ℝ[X]} {r s : ℝ} (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree) - (_hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : P g.natDegree) : + (hright : ∀ μ : ℝ, 0 < μ → + (X * (deleteRootFactor f r).comp (X + C r) + + C μ * g.comp (X + C r)).Splits) : + Compatible + (X * (deleteRootFactor f r).comp (X + C r)) + (g.comp (X + C r)) := by + have hdelete_rr : + deleteRootFactor f r ≠ 0 ∧ (deleteRootFactor f r).Splits := + hleft.delete_ne_zero_and_splits hsgn.left_ne_zero hf + have hdelete_shift_rr : + (deleteRootFactor f r).comp (X + C r) ≠ 0 ∧ + ((deleteRootFactor f r).comp (X + C r)).Splits := + isRealRooted_comp_X_add_C hdelete_rr.1 hdelete_rr.2 r + have hrestored_split : + (X * (deleteRootFactor f r).comp (X + C r)).Splits := + (isRealRooted_X_mul hdelete_shift_rr.1 hdelete_shift_rr.2).2 + have hg_shift_split : (g.comp (X + C r)).Splits := + (isRealRooted_comp_X_add_C hsgn.right_ne_zero hg r).2 + exact Compatible.of_splits_of_pos_right_family hrestored_split hg_shift_split + hright + +/-- Same-degree left Liu branch: after translating the deleted largest root of +`f` to the origin, every positive right combination of the restored pair +splits. The sign-normalized deletion pair has right endpoint one degree +higher, so this is the right-successor x-subtraction pencil. -/ +theorem theorem21LeftFactorReturnSameDegreeTranslatedRightFamily + {f g : ℝ[X]} {r s : ℝ} + (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) + (hleft : LeftRootCountBranch f g r s) + (hdeg : f.natDegree = g.natDegree) : ∀ μ : ℝ, 0 < μ → (X * (deleteRootFactor f r).comp (X + C r) + C μ * g.comp (X + C r)).Splits := by @@ -50,9 +78,9 @@ theorem theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_xSub_rightPr have hdeg_pos : (-g).natDegree = (deleteRootFactor f r).natDegree + 1 := by simpa [Polynomial.natDegree_neg] using hdelete_deg.symm - have hGdeg : P (-g).natDegree := by simpa [Polynomial.natDegree_neg] using hgdeg have hsplit := - hterminal r hpair hqnn hGnn hdeg_pos hGdeg μ hμ + positiveSplitRightSuccDegreeTranslatedXSubRightFamily r hpair hqnn hGnn + hdeg_pos μ hμ simpa [sub_eq_add_neg, mul_neg] using hsplit · have hQnn : HasNonnegCoeffs ((-(deleteRootFactor f r)).comp (X + C r)) := by @@ -67,34 +95,19 @@ theorem theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_xSub_rightPr g.natDegree = (-(deleteRootFactor f r)).natDegree + 1 := by simpa [Polynomial.natDegree_neg] using hdelete_deg.symm have hsplit := - hterminal r hpair hQnn hgnn hdeg_pos hgdeg μ hμ + positiveSplitRightSuccDegreeTranslatedXSubRightFamily r hpair hQnn hgnn + hdeg_pos μ hμ simpa [sub_eq_add_neg, mul_neg, neg_add_rev, add_comm] using hsplit.neg -/-- A right-successor positive-split subtraction-family leaf gives the -translated right-family target for the same-degree Liu left branch. -/ -theorem theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_xSub - (hsub : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyStatement := by - intro f g r s hf hg hsgn hleft hdeg hcommon - exact theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_xSub_rightPredicate - (P := fun _ => True) - (positiveSplitTranslatedXSubRightFamilyPredicateRelation_true_of_relation - hsub) - hf hg hsgn hleft hdeg hcommon trivial - -/-- A same-degree sign-normalized x-subtraction leaf gives the translated -right-family target for the successor-degree Liu left branch. -/ -theorem theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_xSub_rightPredicate - {P : ℕ → Prop} - (hterminal : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement P) +/-- Successor-degree left Liu branch: after translating the deleted largest +root of `f` to the origin, every positive right combination of the restored +pair splits. The sign-normalized deletion pair has equal endpoint degrees, so +this is the same-degree x-subtraction pencil. -/ +theorem theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily {f g : ℝ[X]} {r s : ℝ} (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (_hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : P g.natDegree) : + (hdeg : f.natDegree = g.natDegree + 1) : ∀ μ : ℝ, 0 < μ → (X * (deleteRootFactor f r).comp (X + C r) + C μ * g.comp (X + C r)).Splits := by @@ -117,9 +130,9 @@ theorem theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_xSub_rightPr have hdeg_pos : (deleteRootFactor f r).natDegree = (-g).natDegree := by simpa [Polynomial.natDegree_neg] using hdelete_deg - have hGdeg : P (-g).natDegree := by simpa [Polynomial.natDegree_neg] using hgdeg have hsplit := - hterminal r hpair hqnn hGnn hdeg_pos hGdeg μ hμ + positiveSplitSameDegreeTranslatedXSubRightFamily r hpair hqnn hGnn + hdeg_pos μ hμ simpa [sub_eq_add_neg, mul_neg] using hsplit · have hQnn : HasNonnegCoeffs ((-(deleteRootFactor f r)).comp (X + C r)) := by @@ -134,580 +147,9 @@ theorem theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_xSub_rightPr (-(deleteRootFactor f r)).natDegree = g.natDegree := by simpa [Polynomial.natDegree_neg] using hdelete_deg have hsplit := - hterminal r hpair hQnn hgnn hdeg_pos hgdeg μ hμ + positiveSplitSameDegreeTranslatedXSubRightFamily r hpair hQnn hgnn + hdeg_pos μ hμ simpa [sub_eq_add_neg, mul_neg, neg_add_rev, add_comm] using hsplit.neg -/-- A same-degree positive-split subtraction-family leaf gives the translated -right-family target for the successor-degree Liu left branch. -/ -theorem theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_xSub - (hsub : positiveSplitSameDegreeTranslatedXSubRightFamilyStatement) : - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyStatement := by - intro f g r s hf hg hsgn hleft hdeg hcommon - exact theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_xSub_rightPredicate - (P := fun _ => True) - (positiveSplitTranslatedXSubRightFamilyPredicateRelation_true_of_relation - hsub) - hf hg hsgn hleft hdeg hcommon trivial - -/-- Predicate-restricted right-successor sign-normalized x-subtraction leaves -give predicate-restricted translated right-family targets for the same-degree -Liu left branch. -/ -theorem theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - {P : ℕ → Prop} - (hterminal : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyPredicateStatement - P := by - intro f g r s hf hg hsgn hleft hdeg hcommon hgdeg - exact theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_xSub_rightPredicate - hterminal hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Predicate-restricted same-degree sign-normalized x-subtraction leaves give -predicate-restricted translated right-family targets for the successor-degree -Liu left branch. -/ -theorem theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - {P : ℕ → Prop} - (hterminal : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement P) : - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyPredicateStatement - P := by - intro f g r s hf hg hsgn hleft hdeg hcommon hgdeg - exact theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_xSub_rightPredicate - hterminal hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Degree-one right endpoint case for the translated same-degree Liu -right-family target. -/ -theorem theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_right_natDegree_one - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 1) : - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits := - theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_xSub_rightPredicate - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_one - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Endpoint cases through right degree three for the translated same-degree Liu -right-family target. -/ -theorem - theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_right_natDegree_le_three - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree ≤ 3) : - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits := - theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_xSub_rightPredicate - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_three - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Degree-zero right endpoint case for the translated successor-degree Liu -right-family target. -/ -theorem theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_right_natDegree_zero - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 0) : - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits := - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_xSub_rightPredicate - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_zero - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Degree-one right endpoint case for the translated successor-degree Liu -right-family target. -/ -theorem theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_right_natDegree_one - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 1) : - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits := - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_xSub_rightPredicate - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_one - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Endpoint cases through right degree three for the translated -successor-degree Liu right-family target, modulo the normalized monic -cubic/cubic x-subtraction leaf. -/ -theorem - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_right_natDegree_le_three_of_monic - (hmono : xSubCubicCubicSplitsStatement) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree ≤ 3) : - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits := - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_xSub_rightPredicate - (positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_three_of_monic - hmono) - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Endpoint cases through right degree three for the translated successor-degree -Liu right-family target. -/ -theorem - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_right_natDegree_le_three - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree ≤ 3) : - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits := - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_right_natDegree_le_three_of_monic - xSubCubicCubicSplits hf hg hsgn hleft hdeg hcommon hgdeg - -/-- The translated same-degree right-family leaf gives the translated -compatibility leaf by scaling an arbitrary nonnegative linear combination. -/ -theorem theorem21LeftFactorReturnSameDegreeTranslatedCompatible_of_rightFamily - (hright : - theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyStatement) : - theorem21LeftFactorReturnSameDegreeTranslatedCompatibleStatement := - theorem21LeftFactorReturnTranslatedCompatible_of_rightFamilyRelation - (R := fun m n => m = n) hright - -/-- The translated successor-degree right-family leaf gives the translated -compatibility leaf by scaling an arbitrary nonnegative linear combination. -/ -theorem theorem21LeftFactorReturnSuccDegreeTranslatedCompatible_of_rightFamily - (hright : - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyStatement) : - theorem21LeftFactorReturnSuccDegreeTranslatedCompatibleStatement := - theorem21LeftFactorReturnTranslatedCompatible_of_rightFamilyRelation - (R := fun m n => m = n + 1) hright - -/-- Predicate-restricted translated same-degree right-family targets give -predicate-restricted translated compatibility targets. -/ -theorem theorem21LeftFactorReturnSameDegreeTranslatedCompatiblePredicate_of_rightPredicate - {P : ℕ → Prop} - (hright : - theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnSameDegreeTranslatedCompatiblePredicateStatement - P := - theorem21LeftFactorReturnTranslatedCompatible_of_rightPredicateRelation - (R := fun m n => m = n) hright - -/-- Predicate-restricted translated successor-degree right-family targets give -predicate-restricted translated compatibility targets. -/ -theorem theorem21LeftFactorReturnSuccDegreeTranslatedCompatiblePredicate_of_rightPredicate - {P : ℕ → Prop} - (hright : - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnSuccDegreeTranslatedCompatiblePredicateStatement - P := - theorem21LeftFactorReturnTranslatedCompatible_of_rightPredicateRelation - (R := fun m n => m = n + 1) hright - -/-- Degree-one right endpoint case for the translated same-degree Liu -compatibility target. -/ -theorem theorem21LeftFactorReturnSameDegreeTranslatedCompatible_of_right_natDegree_one - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 1) : - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := - theorem21LeftFactorReturnTranslatedCompatible_of_pointwiseRightFamily - hf hg hsgn hleft - (theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_right_natDegree_one - hf hg hsgn hleft hdeg hcommon hgdeg) - -/-- Endpoint cases through right degree three for the translated same-degree Liu -compatibility target. -/ -theorem - theorem21LeftFactorReturnSameDegreeTranslatedCompatible_of_right_natDegree_le_three - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree ≤ 3) : - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := - theorem21LeftFactorReturnTranslatedCompatible_of_pointwiseRightFamily - hf hg hsgn hleft - (theorem21LeftFactorReturnSameDegreeTranslatedRightFamily_of_right_natDegree_le_three - hf hg hsgn hleft hdeg hcommon hgdeg) - -/-- Degree-zero right endpoint case for the translated successor-degree Liu -compatibility target. -/ -theorem theorem21LeftFactorReturnSuccDegreeTranslatedCompatible_of_right_natDegree_zero - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 0) : - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := - theorem21LeftFactorReturnTranslatedCompatible_of_pointwiseRightFamily - hf hg hsgn hleft - (theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_right_natDegree_zero - hf hg hsgn hleft hdeg hcommon hgdeg) - -/-- Degree-one right endpoint case for the translated successor-degree Liu -compatibility target. -/ -theorem theorem21LeftFactorReturnSuccDegreeTranslatedCompatible_of_right_natDegree_one - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 1) : - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := - theorem21LeftFactorReturnTranslatedCompatible_of_pointwiseRightFamily - hf hg hsgn hleft - (theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_right_natDegree_one - hf hg hsgn hleft hdeg hcommon hgdeg) - -/-- Endpoint cases through right degree three for the translated successor-degree -Liu compatibility target, modulo the normalized monic cubic/cubic x-subtraction -leaf. -/ -theorem - theorem21LeftFactorReturnSuccDegreeTranslatedCompatible_of_right_natDegree_le_three_of_monic - (hmono : xSubCubicCubicSplitsStatement) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree ≤ 3) : - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := - theorem21LeftFactorReturnTranslatedCompatible_of_pointwiseRightFamily - hf hg hsgn hleft - (theorem21LeftFactorReturnSuccDegreeTranslatedRightFamily_of_right_natDegree_le_three_of_monic - hmono hf hg hsgn hleft hdeg hcommon hgdeg) - -/-- Endpoint cases through right degree three for the translated successor-degree -Liu compatibility target. -/ -theorem theorem21LeftFactorReturnSuccDegreeTranslatedCompatible_of_right_natDegree_le_three - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree ≤ 3) : - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := - theorem21LeftFactorReturnSuccDegreeTranslatedCompatible_of_right_natDegree_le_three_of_monic - xSubCubicCubicSplits hf hg hsgn hleft hdeg hcommon hgdeg - -/-- The translated same-degree target gives the original same-degree -factor-return leaf by descending through the translation. -/ -theorem theorem21LeftFactorReturnSameDegree_of_translatedCompatible - (htranslated : - theorem21LeftFactorReturnSameDegreeTranslatedCompatibleStatement) : - theorem21LeftFactorReturnSameDegreeStatement := - theorem21LeftFactorReturn_of_translatedCompatibleRelation - (R := fun m n => m = n) htranslated - -/-- The translated successor-degree target gives the original successor-degree -factor-return leaf by descending through the translation. -/ -theorem theorem21LeftFactorReturnSuccDegree_of_translatedCompatible - (htranslated : - theorem21LeftFactorReturnSuccDegreeTranslatedCompatibleStatement) : - theorem21LeftFactorReturnSuccDegreeStatement := - theorem21LeftFactorReturn_of_translatedCompatibleRelation - (R := fun m n => m = n + 1) htranslated - -/-- Predicate-restricted translated same-degree compatibility targets give the -corresponding predicate-restricted original factor-return targets. -/ -theorem theorem21LeftFactorReturnSameDegreePredicate_of_translatedCompatiblePredicate - {P : ℕ → Prop} - (htranslated : - theorem21LeftFactorReturnSameDegreeTranslatedCompatiblePredicateStatement - P) : - theorem21LeftFactorReturnSameDegreePredicateStatement P := - theorem21LeftFactorReturnPredicate_of_translatedCompatibleRelation - (R := fun m n => m = n) htranslated - -/-- Predicate-restricted translated successor-degree compatibility targets -give the corresponding predicate-restricted original factor-return targets. -/ -theorem theorem21LeftFactorReturnSuccDegreePredicate_of_translatedCompatiblePredicate - {P : ℕ → Prop} - (htranslated : - theorem21LeftFactorReturnSuccDegreeTranslatedCompatiblePredicateStatement - P) : - theorem21LeftFactorReturnSuccDegreePredicateStatement P := - theorem21LeftFactorReturnPredicate_of_translatedCompatibleRelation - (R := fun m n => m = n + 1) htranslated - -/-- Predicate-restricted translated same-degree right-family targets give -predicate-restricted original factor-return targets. -/ -theorem theorem21LeftFactorReturnSameDegreePredicate_of_rightPredicate - {P : ℕ → Prop} - (hright : - theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnSameDegreePredicateStatement P := - theorem21LeftFactorReturnSameDegreePredicate_of_translatedCompatiblePredicate - (theorem21LeftFactorReturnSameDegreeTranslatedCompatiblePredicate_of_rightPredicate - hright) - -/-- Predicate-restricted translated successor-degree right-family targets give -predicate-restricted original factor-return targets. -/ -theorem theorem21LeftFactorReturnSuccDegreePredicate_of_rightPredicate - {P : ℕ → Prop} - (hright : - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnSuccDegreePredicateStatement P := - theorem21LeftFactorReturnSuccDegreePredicate_of_translatedCompatiblePredicate - (theorem21LeftFactorReturnSuccDegreeTranslatedCompatiblePredicate_of_rightPredicate - hright) - -/-- Predicate-restricted right-successor sign-normalized x-subtraction -families give predicate-restricted original same-degree factor-return targets. -/ -theorem theorem21LeftFactorReturnSameDegreePredicate_of_xSubPredicate - {P : ℕ → Prop} - (hsub : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnSameDegreePredicateStatement P := - theorem21LeftFactorReturnSameDegreePredicate_of_rightPredicate - (theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - hsub) - -/-- Predicate-restricted same-degree sign-normalized x-subtraction families -give predicate-restricted original successor-degree factor-return targets. -/ -theorem theorem21LeftFactorReturnSuccDegreePredicate_of_xSubPredicate - {P : ℕ → Prop} - (hsub : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement P) : - theorem21LeftFactorReturnSuccDegreePredicateStatement P := - theorem21LeftFactorReturnSuccDegreePredicate_of_rightPredicate - (theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - hsub) - -/-- Predicate-restricted translated right-family targets give pointwise -original same-degree factor-return targets. -/ -theorem theorem21LeftFactorReturnSameDegree_of_rightPredicate - {P : ℕ → Prop} - (hright : - theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyPredicateStatement - P) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : P g.natDegree) : - Compatible f g := - theorem21LeftFactorReturnSameDegreePredicate_of_rightPredicate hright - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Predicate-restricted translated right-family targets give pointwise -original successor-degree factor-return targets. -/ -theorem theorem21LeftFactorReturnSuccDegree_of_rightPredicate - {P : ℕ → Prop} - (hright : - theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyPredicateStatement - P) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : P g.natDegree) : - Compatible f g := - theorem21LeftFactorReturnSuccDegreePredicate_of_rightPredicate hright - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Predicate-restricted right-successor sign-normalized x-subtraction leaves -give pointwise original same-degree factor-return targets. -/ -theorem theorem21LeftFactorReturnSameDegree_of_xSubPredicate - {P : ℕ → Prop} - (hsub : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : P g.natDegree) : - Compatible f g := - theorem21LeftFactorReturnSameDegree_of_rightPredicate - (theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - hsub) - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Predicate-restricted same-degree sign-normalized x-subtraction leaves give -pointwise original successor-degree factor-return targets. -/ -theorem theorem21LeftFactorReturnSuccDegree_of_xSubPredicate - {P : ℕ → Prop} - (hsub : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement P) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : P g.natDegree) : - Compatible f g := - theorem21LeftFactorReturnSuccDegree_of_rightPredicate - (theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - hsub) - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- A right-successor sign-normalized x-subtraction leaf gives the original -same-degree factor-return target. -/ -theorem theorem21LeftFactorReturnSameDegree_of_xSub - (hsub : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21LeftFactorReturnSameDegreeStatement := by - intro f g r s hf hg hsgn hleft hdeg hcommon - exact theorem21LeftFactorReturnSameDegree_of_xSubPredicate - (P := fun _ => True) - (positiveSplitTranslatedXSubRightFamilyPredicateRelation_true_of_relation - hsub) - hf hg hsgn hleft hdeg hcommon trivial - -/-- A same-degree sign-normalized x-subtraction leaf gives the original -successor-degree factor-return target. -/ -theorem theorem21LeftFactorReturnSuccDegree_of_xSub - (hsub : positiveSplitSameDegreeTranslatedXSubRightFamilyStatement) : - theorem21LeftFactorReturnSuccDegreeStatement := by - intro f g r s hf hg hsgn hleft hdeg hcommon - exact theorem21LeftFactorReturnSuccDegree_of_xSubPredicate - (P := fun _ => True) - (positiveSplitTranslatedXSubRightFamilyPredicateRelation_true_of_relation - hsub) - hf hg hsgn hleft hdeg hcommon trivial - -/-- Degree-one right endpoint case for the original same-degree Liu -factor-return target. -/ -theorem theorem21LeftFactorReturnSameDegree_of_right_natDegree_one - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 1) : - Compatible f g := - theorem21LeftFactorReturnSameDegree_of_xSubPredicate - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_one - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Degree-one-right endpoint package for the original same-degree left -factor-return leaf. -/ -theorem theorem21LeftFactorReturnSameDegreePredicate_of_right_natDegree_one : - theorem21LeftFactorReturnSameDegreePredicateStatement - (fun n => n = 1) := - theorem21LeftFactorReturnSameDegreePredicate_of_xSubPredicate - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_one - -/-- Endpoint cases through right degree three for the original same-degree left -factor-return leaf, modulo the normalized monic quadratic/cubic leaf. -/ -theorem theorem21LeftFactorReturnSameDegreePredicate_of_right_natDegree_le_three_of_monic - (hmono : xSubQuadraticCubicSplitsStatement) : - theorem21LeftFactorReturnSameDegreePredicateStatement - (fun n => n ≤ 3) := - theorem21LeftFactorReturnSameDegreePredicate_of_xSubPredicate - (positiveSplitRightSuccXSubFamilyPredicate_of_right_natDegree_le_three_of_monic - hmono) - -/-- Endpoint cases through right degree three for the original same-degree left -factor-return leaf. -/ -theorem theorem21LeftFactorReturnSameDegreePredicate_of_right_natDegree_le_three : - theorem21LeftFactorReturnSameDegreePredicateStatement - (fun n => n ≤ 3) := - theorem21LeftFactorReturnSameDegreePredicate_of_right_natDegree_le_three_of_monic - xSubQuadraticCubicSplits - -/-- Degree-zero right endpoint case for the original successor-degree Liu -factor-return target. -/ -theorem theorem21LeftFactorReturnSuccDegree_of_right_natDegree_zero - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 0) : - Compatible f g := - theorem21LeftFactorReturnSuccDegree_of_xSubPredicate - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_zero - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Degree-one right endpoint case for the original successor-degree Liu -factor-return target. -/ -theorem theorem21LeftFactorReturnSuccDegree_of_right_natDegree_one - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 1) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 1) : - Compatible f g := - theorem21LeftFactorReturnSuccDegree_of_xSubPredicate - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_one - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Degree-zero-right endpoint package for the original successor-degree left -factor-return leaf. -/ -theorem theorem21LeftFactorReturnSuccDegreePredicate_of_right_natDegree_zero : - theorem21LeftFactorReturnSuccDegreePredicateStatement - (fun n => n = 0) := - theorem21LeftFactorReturnSuccDegreePredicate_of_xSubPredicate - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_zero - -/-- Degree-one-right endpoint package for the original successor-degree left -factor-return leaf. -/ -theorem theorem21LeftFactorReturnSuccDegreePredicate_of_right_natDegree_one : - theorem21LeftFactorReturnSuccDegreePredicateStatement - (fun n => n = 1) := - theorem21LeftFactorReturnSuccDegreePredicate_of_xSubPredicate - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_one - -/-- Endpoint cases through right degree three for the original successor-degree -left factor-return leaf, packaged as a predicate-restricted statement modulo the -normalized monic cubic/cubic x-subtraction leaf. -/ -theorem theorem21LeftFactorReturnSuccDegreePredicate_of_right_natDegree_le_three_of_monic - (hmono : xSubCubicCubicSplitsStatement) : - theorem21LeftFactorReturnSuccDegreePredicateStatement - (fun n => n ≤ 3) := - theorem21LeftFactorReturnSuccDegreePredicate_of_xSubPredicate - (positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_three_of_monic - hmono) - -/-- Endpoint cases through right degree three for the original successor-degree -left factor-return leaf, packaged as a predicate-restricted statement. -/ -theorem theorem21LeftFactorReturnSuccDegreePredicate_of_right_natDegree_le_three : - theorem21LeftFactorReturnSuccDegreePredicateStatement - (fun n => n ≤ 3) := - theorem21LeftFactorReturnSuccDegreePredicate_of_right_natDegree_le_three_of_monic - xSubCubicCubicSplits - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/FactorReturnStatements.lean b/RealRooted/LiuOppositeSigns/FactorReturnStatements.lean deleted file mode 100644 index e8e0cf4f4..000000000 --- a/RealRooted/LiuOppositeSigns/FactorReturnStatements.lean +++ /dev/null @@ -1,721 +0,0 @@ -import RealRooted.LiuOppositeSigns.DeletionBranches - -/-! -# Liu factor-return statement interface - -This module contains the statement-level factor-return packages, target -aliases, and left/right symmetry adapters used in the reverse direction of Liu -Theorem 2.1. -The proof-heavy degree branches and final theorem assembly remain in -`RealRooted.LiuOppositeSigns.Theorem`. --/ - -open Polynomial Filter - -namespace RealRooted -namespace LiuOppositeSigns - -/-- The remaining factor-return principle for the reverse direction of Liu -Theorem 2.1. It says that once the selected deletion pair has a common -right interleaver, the deleted largest linear factor can be put back to recover -compatibility of the original opposite-leading-sign pair. -/ -def theorem21DeletionPairCommonInterleaverFactorReturnStatement : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - (LeftRootCountBranch f g r s → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - Compatible f g) ∧ - (RightRootCountBranch f g r s → - (∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) → - Compatible f g) - -/-- The factor-return principle proves the branch-retaining -common-interleaver reverse direction. -/ -theorem theorem21DeletionPairCommonInterleaverBranchesToCompatible_of_factorReturn - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21DeletionPairCommonInterleaverBranchesToCompatibleStatement := by - intro f g hf hg hsgn hbranches - rcases hbranches with ⟨r, s, hleft | hright⟩ - · exact (hreturn hf hg hsgn).1 hleft.1 hleft.2 - · exact (hreturn hf hg hsgn).2 hright.1 hright.2 - -/-- The branch-retaining deletion-pair common-interleaver theorem package -follows from the isolated forward direction and factor-return principle. -/ -theorem - theorem21DeletionPairCommonInterleaverIff_of_commonForward_and_factorReturn - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21CompatibleDeletionPairCommonInterleaverBranchesStatement := - theorem21CompatibleDeletionPairCommonInterleaverBranches_of_forward_and_reverse - hforward - (theorem21DeletionPairCommonInterleaverBranchesToCompatible_of_factorReturn - hreturn) - -/-- Stronger all-real-combination version of the factor-return principle. -/ -def theorem21DeletionPairCommonInterleaverFactorReturnAllComboStatement : - Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - (LeftRootCountBranch f g r s → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - AllComboRealRooted f g) ∧ - (RightRootCountBranch f g r s → - (∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) → - AllComboRealRooted f g) - -/-- The all-real-combination factor-return target implies the existing -compatibility factor-return target. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturn_of_allCombo - (hreturn : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnStatement := by - intro f g r s hf hg hsgn - constructor - · intro hleft hcommon - exact Compatible.of_allComboRealRooted - ((hreturn hf hg hsgn).1 hleft hcommon) - · intro hright hcommon - exact Compatible.of_allComboRealRooted - ((hreturn hf hg hsgn).2 hright hcommon) - -/-- Swap the common-right-interleaver witness in a right deletion pair. -/ -theorem rightDeletionPairCommonInterleaver_symm {f g : ℝ[X]} {s : ℝ} - (hcommon : ∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) : - ∃ k : ℝ[X], StrictInterl (deleteRootFactor g s) k ∧ StrictInterl f k := by - rcases hcommon with ⟨k, hfk, hgk⟩ - exact ⟨k, hgk, hfk⟩ - -/-- Left-branch all-combinations factor-return target for an arbitrary endpoint -degree relation. -/ -def theorem21LeftFactorReturnAllComboRelationStatement - (R : ℕ → ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - AllComboRealRooted f g - -/-- Same-degree left-branch all-combinations factor-return target. -/ -def theorem21LeftFactorReturnSameDegreeAllComboStatement : Prop := - theorem21LeftFactorReturnAllComboRelationStatement - (fun m n => m = n) - -/-- Succ-degree left-branch all-combinations factor-return target. -/ -def theorem21LeftFactorReturnSuccDegreeAllComboStatement : Prop := - theorem21LeftFactorReturnAllComboRelationStatement - (fun m n => m = n + 1) - -/-- Two-degree-gap left-branch all-combinations factor-return target. -/ -def theorem21LeftFactorReturnTwoDegreeAllComboStatement : Prop := - theorem21LeftFactorReturnAllComboRelationStatement - (fun m n => m = n + 2) - -/-- The three left-branch all-combinations factor-return cases. The right -branch follows by symmetry. -/ -def theorem21LeftFactorReturnAllComboDegreeCasesStatement : Prop := - theorem21LeftFactorReturnSameDegreeAllComboStatement ∧ - theorem21LeftFactorReturnSuccDegreeAllComboStatement ∧ - theorem21LeftFactorReturnTwoDegreeAllComboStatement - -/-- Right-branch all-combinations factor-return target for an arbitrary endpoint -degree relation. The relation is evaluated as `R g.natDegree f.natDegree`, -matching the right branch where `g` is the endpoint with the deleted root. -/ -def theorem21RightFactorReturnAllComboRelationStatement - (R : ℕ → ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - RightRootCountBranch f g r s → - R g.natDegree f.natDegree → - (∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) → - AllComboRealRooted f g - -/-- Same-degree right-branch all-combinations factor-return target. -/ -def theorem21RightFactorReturnSameDegreeAllComboStatement : Prop := - theorem21RightFactorReturnAllComboRelationStatement - (fun m n => m = n) - -/-- Succ-degree right-branch all-combinations factor-return target. -/ -def theorem21RightFactorReturnSuccDegreeAllComboStatement : Prop := - theorem21RightFactorReturnAllComboRelationStatement - (fun m n => m = n + 1) - -/-- Two-degree-gap right-branch all-combinations factor-return target. -/ -def theorem21RightFactorReturnTwoDegreeAllComboStatement : Prop := - theorem21RightFactorReturnAllComboRelationStatement - (fun m n => m = n + 2) - -/-- The three right-branch all-combinations factor-return cases. -/ -def theorem21RightFactorReturnAllComboDegreeCasesStatement : Prop := - theorem21RightFactorReturnSameDegreeAllComboStatement ∧ - theorem21RightFactorReturnSuccDegreeAllComboStatement ∧ - theorem21RightFactorReturnTwoDegreeAllComboStatement - -/-- General symmetry bridge from a left-branch all-combinations factor-return -theorem to the matching right-branch theorem with the degree relation -reversed. -/ -theorem theorem21RightFactorReturnAllCombo_of_leftDegreeRelation - {R : ℕ → ℕ → Prop} - (hleft : theorem21LeftFactorReturnAllComboRelationStatement R) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hright : RightRootCountBranch f g r s) - (hdeg : R g.natDegree f.natDegree) - (hcommon : ∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl (deleteRootFactor g s) k) : - AllComboRealRooted f g := - allComboRealRooted_comm <| - hleft (f := g) (g := f) (r := s) (s := r) - hg hf hsgn.symm hright.toLeftBranch_symm hdeg - (rightDeletionPairCommonInterleaver_symm hcommon) - -/-- A left all-combinations relation theorem gives the matching right-branch -relation theorem by symmetry. -/ -theorem theorem21RightFactorReturnAllComboRelation_of_leftRelation - {R : ℕ → ℕ → Prop} - (hleft : theorem21LeftFactorReturnAllComboRelationStatement R) : - theorem21RightFactorReturnAllComboRelationStatement R := by - intro f g r s hf hg hsgn hright hdeg hcommon - exact theorem21RightFactorReturnAllCombo_of_leftDegreeRelation - hleft hf hg hsgn hright hdeg hcommon - -/-- The right same-degree all-combinations factor-return case follows from -the left same-degree case by swapping the two polynomials. -/ -theorem theorem21RightFactorReturnSameDegreeAllCombo_of_leftSameDegree - (hleft : theorem21LeftFactorReturnSameDegreeAllComboStatement) : - theorem21RightFactorReturnSameDegreeAllComboStatement := - theorem21RightFactorReturnAllComboRelation_of_leftRelation - (R := fun m n => m = n) hleft - -/-- The right successor-degree all-combinations factor-return case follows -from the left successor-degree case by swapping the two polynomials. -/ -theorem theorem21RightFactorReturnSuccDegreeAllCombo_of_leftSuccDegree - (hleft : theorem21LeftFactorReturnSuccDegreeAllComboStatement) : - theorem21RightFactorReturnSuccDegreeAllComboStatement := - theorem21RightFactorReturnAllComboRelation_of_leftRelation - (R := fun m n => m = n + 1) hleft - -/-- The right two-degree-gap all-combinations factor-return case follows -from the left two-degree-gap case by swapping the two polynomials. -/ -theorem theorem21RightFactorReturnTwoDegreeAllCombo_of_leftTwoDegree - (hleft : theorem21LeftFactorReturnTwoDegreeAllComboStatement) : - theorem21RightFactorReturnTwoDegreeAllComboStatement := - theorem21RightFactorReturnAllComboRelation_of_leftRelation - (R := fun m n => m = n + 2) hleft - -/-- Left all-combinations factor-return degree cases give the matching right -degree cases by symmetry. -/ -theorem theorem21RightFactorReturnAllComboDegreeCases_of_leftCases - (hcases : theorem21LeftFactorReturnAllComboDegreeCasesStatement) : - theorem21RightFactorReturnAllComboDegreeCasesStatement := - ⟨theorem21RightFactorReturnSameDegreeAllCombo_of_leftSameDegree hcases.1, - theorem21RightFactorReturnSuccDegreeAllCombo_of_leftSuccDegree hcases.2.1, - theorem21RightFactorReturnTwoDegreeAllCombo_of_leftTwoDegree hcases.2.2⟩ - -/-- Degree-case split needed to prove the all-combinations factor-return -principle. -/ -def theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCasesStatement : - Prop := - theorem21LeftFactorReturnSameDegreeAllComboStatement ∧ - theorem21LeftFactorReturnSuccDegreeAllComboStatement ∧ - theorem21LeftFactorReturnTwoDegreeAllComboStatement ∧ - theorem21RightFactorReturnSameDegreeAllComboStatement ∧ - theorem21RightFactorReturnSuccDegreeAllComboStatement ∧ - theorem21RightFactorReturnTwoDegreeAllComboStatement - -/-- Left and right all-combinations factor-return degree cases assemble into -the full six-case package. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCases_of_leftRightCases - (hleft : theorem21LeftFactorReturnAllComboDegreeCasesStatement) - (hright : theorem21RightFactorReturnAllComboDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCasesStatement := - ⟨hleft.1, hleft.2.1, hleft.2.2, - hright.1, hright.2.1, hright.2.2⟩ - -/-- Left projection from a six-case all-combinations factor-return package. -/ -theorem theorem21LeftFactorReturnAllComboDegreeCases_of_allComboFactorCases - (hcases : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCasesStatement) : - theorem21LeftFactorReturnAllComboDegreeCasesStatement := - ⟨hcases.1, hcases.2.1, hcases.2.2.1⟩ - -/-- Right projection from a six-case all-combinations factor-return package. -/ -theorem theorem21RightFactorReturnAllComboDegreeCases_of_allComboFactorCases - (hcases : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCasesStatement) : - theorem21RightFactorReturnAllComboDegreeCasesStatement := - ⟨hcases.2.2.2.1, hcases.2.2.2.2.1, hcases.2.2.2.2.2⟩ - -/-- Left all-combinations factor-return degree cases supply all six left/right -cases by symmetry. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCases_of_leftCases - (hcases : theorem21LeftFactorReturnAllComboDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCasesStatement := - theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCases_of_leftRightCases - hcases - (theorem21RightFactorReturnAllComboDegreeCases_of_leftCases hcases) - -/-- The explicit all-combinations factor-return principle follows from its -six restored-degree cases. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturnAllCombo_of_degreeCases - (hcases : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboStatement := by - let hleftCases := - theorem21LeftFactorReturnAllComboDegreeCases_of_allComboFactorCases hcases - let hrightCases := - theorem21RightFactorReturnAllComboDegreeCases_of_allComboFactorCases hcases - intro f g r s hf hg hsgn - constructor - · intro hleft hcommon - rcases hleft.natDegree_eq_or_eq_succ_or_eq_succ_succ - hsgn.left_ne_zero hf hg with hdeg | hdeg | hdeg - · exact hleftCases.1 hf hg hsgn hleft hdeg hcommon - · exact hleftCases.2.1 hf hg hsgn hleft hdeg hcommon - · exact hleftCases.2.2 hf hg hsgn hleft hdeg hcommon - · intro hright hcommon - rcases hright.natDegree_eq_or_eq_succ_or_eq_succ_succ - hsgn.right_ne_zero hf hg with hdeg | hdeg | hdeg - · exact hrightCases.1 hf hg hsgn hright hdeg hcommon - · exact hrightCases.2.1 hf hg hsgn hright hdeg hcommon - · exact hrightCases.2.2 hf hg hsgn hright hdeg hcommon - -/-- It is enough to prove the left-branch all-combinations factor-return -cases; the right branch is symmetric. -/ -theorem theorem21DeletionPairCommonInterleaverFactorReturnAllCombo_of_leftCases - (hcases : theorem21LeftFactorReturnAllComboDegreeCasesStatement) : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboStatement := - theorem21DeletionPairCommonInterleaverFactorReturnAllCombo_of_degreeCases - (theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCases_of_leftCases - hcases) - -/-- Left-branch factor-return target for an arbitrary endpoint degree -relation. -/ -def theorem21LeftFactorReturnRelationStatement - (R : ℕ → ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - Compatible f g - -/-- Predicate-restricted left-branch factor-return target for an arbitrary -endpoint degree relation. The predicate records endpoint side conditions on -`g.natDegree`. -/ -def theorem21LeftFactorReturnPredicateRelationStatement - (R : ℕ → ℕ → Prop) (P : ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - P g.natDegree → Compatible f g - -/-- The unrestricted left factor-return relation target is the `P := True` -case of the predicate-restricted relation target. -/ -theorem theorem21LeftFactorReturnPredicateRelation_true_of_relation - {R : ℕ → ℕ → Prop} - (hreturn : theorem21LeftFactorReturnRelationStatement R) : - theorem21LeftFactorReturnPredicateRelationStatement R - (fun _ => True) := by - intro f g r s hf hg hsgn hleft hdeg hcommon _ - exact hreturn hf hg hsgn hleft hdeg hcommon - -/-- A `P := True` left factor-return predicate relation target gives the -unrestricted relation target. -/ -theorem theorem21LeftFactorReturnRelation_of_predicate_true - {R : ℕ → ℕ → Prop} - (hreturn : - theorem21LeftFactorReturnPredicateRelationStatement R - (fun _ => True)) : - theorem21LeftFactorReturnRelationStatement R := by - intro f g r s hf hg hsgn hleft hdeg hcommon - exact hreturn hf hg hsgn hleft hdeg hcommon trivial - -/-- Same-degree left-branch factor-return target. -/ -def theorem21LeftFactorReturnSameDegreeStatement : Prop := - theorem21LeftFactorReturnRelationStatement - (fun m n => m = n) - -/-- Succ-degree left-branch factor-return target. -/ -def theorem21LeftFactorReturnSuccDegreeStatement : Prop := - theorem21LeftFactorReturnRelationStatement - (fun m n => m = n + 1) - -/-- Predicate-restricted same-degree left-branch factor-return target. -The predicate records endpoint side conditions on `g.natDegree`. -/ -def theorem21LeftFactorReturnSameDegreePredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnPredicateRelationStatement - (fun m n => m = n) P - -/-- Predicate-restricted successor-degree left-branch factor-return target. -The predicate records endpoint side conditions on `g.natDegree`. -/ -def theorem21LeftFactorReturnSuccDegreePredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnPredicateRelationStatement - (fun m n => m = n + 1) P - -/-- Two-degree-gap left-branch factor-return target. -/ -def theorem21LeftFactorReturnTwoDegreeStatement : Prop := - theorem21LeftFactorReturnRelationStatement - (fun m n => m = n + 2) - -/-- Predicate-restricted two-degree-gap left-branch factor-return target. -The predicate records endpoint side conditions on `g.natDegree`. -/ -def theorem21LeftFactorReturnTwoDegreePredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnPredicateRelationStatement - (fun m n => m = n + 2) P - -/-- A left all-combinations factor-return leaf for any degree relation gives -the corresponding compatibility factor-return leaf. -/ -theorem theorem21LeftFactorReturn_of_allComboRelation - {R : ℕ → ℕ → Prop} - (hleft : theorem21LeftFactorReturnAllComboRelationStatement R) : - theorem21LeftFactorReturnRelationStatement R := by - intro f g r s hf hg hsgn hbranch hdeg hcommon - exact Compatible.of_allComboRealRooted - (hleft hf hg hsgn hbranch hdeg hcommon) - -/-- A same-degree all-combinations left leaf gives the corresponding -compatibility leaf. -/ -theorem theorem21LeftFactorReturnSameDegree_of_allCombo - (hleft : theorem21LeftFactorReturnSameDegreeAllComboStatement) : - theorem21LeftFactorReturnSameDegreeStatement := - theorem21LeftFactorReturn_of_allComboRelation - (R := fun m n => m = n) hleft - -/-- A successor-degree all-combinations left leaf gives the corresponding -compatibility leaf. -/ -theorem theorem21LeftFactorReturnSuccDegree_of_allCombo - (hleft : theorem21LeftFactorReturnSuccDegreeAllComboStatement) : - theorem21LeftFactorReturnSuccDegreeStatement := - theorem21LeftFactorReturn_of_allComboRelation - (R := fun m n => m = n + 1) hleft - -/-- A two-degree-gap all-combinations left leaf gives the corresponding -compatibility leaf. -/ -theorem theorem21LeftFactorReturnTwoDegree_of_allCombo - (hleft : theorem21LeftFactorReturnTwoDegreeAllComboStatement) : - theorem21LeftFactorReturnTwoDegreeStatement := - theorem21LeftFactorReturn_of_allComboRelation - (R := fun m n => m = n + 2) hleft - -/-- Translated compatibility target for a Liu left-branch factor-return route -with an arbitrary endpoint degree relation. This isolates the common final -step of restoring the deleted largest root after translating it to the origin. -/ -def theorem21LeftFactorReturnTranslatedCompatibleRelationStatement - (R : ℕ → ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) - -/-- Predicate-restricted translated compatibility target for an arbitrary -endpoint degree relation. The predicate records endpoint side conditions on -`g.natDegree`. -/ -def theorem21LeftFactorReturnTranslatedCompatiblePredicateRelationStatement - (R : ℕ → ℕ → Prop) (P : ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - P g.natDegree → - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) - -/-- A `P := True` translated compatibility predicate relation target gives the -unrestricted translated compatibility relation target. -/ -theorem theorem21LeftFactorReturnTranslatedCompatibleRelation_of_predicate_true - {R : ℕ → ℕ → Prop} - (htranslated : - theorem21LeftFactorReturnTranslatedCompatiblePredicateRelationStatement - R (fun _ => True)) : - theorem21LeftFactorReturnTranslatedCompatibleRelationStatement R := by - intro f g r s hf hg hsgn hleft hdeg hcommon - exact htranslated hf hg hsgn hleft hdeg hcommon trivial - -/-- Pointwise translated compatibility descent for a Liu left-branch -factor-return route. -/ -theorem theorem21LeftFactorReturn_of_pointwiseTranslatedCompatible - {f g : ℝ[X]} {r s : ℝ} - (hleft : LeftRootCountBranch f g r s) - (htranslated : - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r))) : - Compatible f g := - hleft.compatible_of_translated_restore htranslated - -/-- A translated compatibility proof for any degree relation gives the -corresponding original left-branch factor-return proof. This is the common -descent step behind the same-, successor-, and two-degree wrappers. -/ -theorem theorem21LeftFactorReturn_of_translatedCompatibleRelation - {R : ℕ → ℕ → Prop} - (htranslated : - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r))) : - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - Compatible f g := by - intro f g r s hf hg hsgn hleft hdeg hcommon - exact theorem21LeftFactorReturn_of_pointwiseTranslatedCompatible hleft - (htranslated hf hg hsgn hleft hdeg hcommon) - -/-- Predicate-restricted translated compatibility targets give the -corresponding predicate-restricted original factor-return targets. -/ -theorem theorem21LeftFactorReturnPredicate_of_translatedCompatibleRelation - {R : ℕ → ℕ → Prop} {P : ℕ → Prop} - (htranslated : - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - P g.natDegree → - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r))) : - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - P g.natDegree → Compatible f g := by - intro f g r s hf hg hsgn hleft hdeg hcommon hgdeg - exact theorem21LeftFactorReturn_of_pointwiseTranslatedCompatible hleft - (htranslated hf hg hsgn hleft hdeg hcommon hgdeg) - -/-- Translated same-degree left-branch factor-return target. -/ -def theorem21LeftFactorReturnSameDegreeTranslatedCompatibleStatement : - Prop := - theorem21LeftFactorReturnTranslatedCompatibleRelationStatement - (fun m n => m = n) - -/-- Translated successor-degree left-branch factor-return target. -/ -def theorem21LeftFactorReturnSuccDegreeTranslatedCompatibleStatement : - Prop := - theorem21LeftFactorReturnTranslatedCompatibleRelationStatement - (fun m n => m = n + 1) - -/-- Predicate-restricted translated same-degree left-branch factor-return -target. The predicate records endpoint side conditions on `g.natDegree`. -/ -def theorem21LeftFactorReturnSameDegreeTranslatedCompatiblePredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnTranslatedCompatiblePredicateRelationStatement - (fun m n => m = n) P - -/-- Predicate-restricted translated successor-degree left-branch factor-return -target. The predicate records endpoint side conditions on `g.natDegree`. -/ -def theorem21LeftFactorReturnSuccDegreeTranslatedCompatiblePredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnTranslatedCompatiblePredicateRelationStatement - (fun m n => m = n + 1) P - -/-- Translated two-degree left-branch factor-return target. This keeps the -original sign of `g` and asks only for compatibility, avoiding the false -all-combinations strengthening. -/ -def theorem21LeftFactorReturnTwoDegreeTranslatedCompatibleStatement : Prop := - theorem21LeftFactorReturnTranslatedCompatibleRelationStatement - (fun m n => m = n + 2) - -/-- Predicate-restricted translated two-degree compatibility target. The -predicate records endpoint side conditions on `g.natDegree`. -/ -def theorem21LeftFactorReturnTwoDegreeTranslatedCompatiblePredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnTranslatedCompatiblePredicateRelationStatement - (fun m n => m = n + 2) P - -/-- One-parameter positive right-pencil version of a translated Liu -left-branch target for an arbitrary endpoint degree relation. -/ -def theorem21LeftFactorReturnTranslatedRightFamilyRelationStatement - (R : ℕ → ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits - -/-- Predicate-restricted translated right-family target for an arbitrary -endpoint degree relation. The predicate records endpoint side conditions such -as fixed right degree or a low-degree bound. -/ -def theorem21LeftFactorReturnTranslatedRightFamilyPredicateRelationStatement - (R : ℕ → ℕ → Prop) (P : ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - P g.natDegree → - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits - -/-- The unrestricted translated right-family relation target is the `P := True` -case of the predicate-restricted relation target. -/ -theorem theorem21LeftFactorReturnTranslatedRightFamilyPredicateRelation_true_of_relation - {R : ℕ → ℕ → Prop} - (hright : - theorem21LeftFactorReturnTranslatedRightFamilyRelationStatement R) : - theorem21LeftFactorReturnTranslatedRightFamilyPredicateRelationStatement - R (fun _ => True) := by - intro f g r s hf hg hsgn hleft hdeg hcommon _ μ hμ - exact hright hf hg hsgn hleft hdeg hcommon μ hμ - -/-- A `P := True` translated right-family predicate relation target gives the -unrestricted translated right-family relation target. -/ -theorem theorem21LeftFactorReturnTranslatedRightFamilyRelation_of_predicate_true - {R : ℕ → ℕ → Prop} - (hright : - theorem21LeftFactorReturnTranslatedRightFamilyPredicateRelationStatement - R (fun _ => True)) : - theorem21LeftFactorReturnTranslatedRightFamilyRelationStatement R := by - intro f g r s hf hg hsgn hleft hdeg hcommon μ hμ - exact hright hf hg hsgn hleft hdeg hcommon trivial μ hμ - -/-- Pointwise right-family form of a translated left-branch Liu compatibility -target. This separates endpoint splitting and coefficient scaling from the -degree-specific right-family leaves. -/ -theorem theorem21LeftFactorReturnTranslatedCompatible_of_pointwiseRightFamily - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hright : ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits) : - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := by - have hdelete_rr : - deleteRootFactor f r ≠ 0 ∧ (deleteRootFactor f r).Splits := - hleft.delete_ne_zero_and_splits hsgn.left_ne_zero hf - have hdelete_shift_rr : - (deleteRootFactor f r).comp (X + C r) ≠ 0 ∧ - ((deleteRootFactor f r).comp (X + C r)).Splits := - isRealRooted_comp_X_add_C hdelete_rr.1 hdelete_rr.2 r - have hrestored_split : - (X * (deleteRootFactor f r).comp (X + C r)).Splits := - (isRealRooted_X_mul hdelete_shift_rr.1 hdelete_shift_rr.2).2 - have hg_shift_split : (g.comp (X + C r)).Splits := - (isRealRooted_comp_X_add_C hsgn.right_ne_zero hg r).2 - exact Compatible.of_splits_of_pos_right_family hrestored_split hg_shift_split - hright - -/-- A translated positive right-family leaf for any degree relation gives the -corresponding translated compatibility target by scaling an arbitrary -nonnegative linear combination. -/ -theorem theorem21LeftFactorReturnTranslatedCompatible_of_rightFamilyRelation - {R : ℕ → ℕ → Prop} - (hright : - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits) : - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := by - intro f g r s hf hg hsgn hleft hdeg hcommon - exact theorem21LeftFactorReturnTranslatedCompatible_of_pointwiseRightFamily - hf hg hsgn hleft (hright hf hg hsgn hleft hdeg hcommon) - -/-- Predicate-restricted translated positive right-family leaves for any -degree relation give the corresponding pointwise translated compatibility -target. -/ -theorem theorem21LeftFactorReturnTranslatedCompatible_of_rightPredicateRelation - {R : ℕ → ℕ → Prop} {P : ℕ → Prop} - (hright : - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - P g.natDegree → - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits) : - ∀ {f g : ℝ[X]} {r s : ℝ}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - LeftRootCountBranch f g r s → - R f.natDegree g.natDegree → - (∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) → - P g.natDegree → - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := by - intro f g r s hf hg hsgn hleft hdeg hcommon hgdeg - exact theorem21LeftFactorReturnTranslatedCompatible_of_pointwiseRightFamily - hf hg hsgn hleft (hright hf hg hsgn hleft hdeg hcommon hgdeg) - -/-- One-parameter positive right-pencil version of the translated same-degree -target. After deleting the largest left root, the sign-normalized deletion -pair has the right endpoint one degree higher. -/ -def theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyStatement : - Prop := - theorem21LeftFactorReturnTranslatedRightFamilyRelationStatement - (fun m n => m = n) - -/-- One-parameter positive right-pencil version of the translated -successor-degree target. After deleting the largest left root, the -sign-normalized deletion pair has equal endpoint degrees. -/ -def theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyStatement : - Prop := - theorem21LeftFactorReturnTranslatedRightFamilyRelationStatement - (fun m n => m = n + 1) - -/-- Predicate-restricted translated same-degree right-family target. -/ -def theorem21LeftFactorReturnSameDegreeTranslatedRightFamilyPredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnTranslatedRightFamilyPredicateRelationStatement - (fun m n => m = n) P - -/-- Predicate-restricted translated successor-degree right-family target. -/ -def theorem21LeftFactorReturnSuccDegreeTranslatedRightFamilyPredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnTranslatedRightFamilyPredicateRelationStatement - (fun m n => m = n + 1) P - -/-- One-parameter positive right-pencil version of the translated two-degree -target. This is the remaining genuinely mathematical leaf after endpoint -splitting and coefficient scaling have been separated out. -/ -def theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyStatement : Prop := - theorem21LeftFactorReturnTranslatedRightFamilyRelationStatement - (fun m n => m = n + 2) - -/-- Predicate-restricted form of the translated two-degree right-family -target. The predicate records endpoint side conditions such as `natDegree = 0`, -`natDegree = 1`, or `natDegree ≤ 1`. -/ -def theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicateStatement - (P : ℕ → Prop) : Prop := - theorem21LeftFactorReturnTranslatedRightFamilyPredicateRelationStatement - (fun m n => m = n + 2) P - -end LiuOppositeSigns -end RealRooted diff --git a/RealRooted/LiuOppositeSigns/FactorReturnTwoDegree.lean b/RealRooted/LiuOppositeSigns/FactorReturnTwoDegree.lean index 6838ff586..d4c6f655e 100644 --- a/RealRooted/LiuOppositeSigns/FactorReturnTwoDegree.lean +++ b/RealRooted/LiuOppositeSigns/FactorReturnTwoDegree.lean @@ -1,12 +1,14 @@ -import RealRooted.LiuOppositeSigns.FactorReturnStatements +import RealRooted.LiuOppositeSigns.DeletionBranches import RealRooted.LiuOppositeSigns.XSub.LeftSuccDegreeThree +import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.LeftSuccessor /-! -# Liu two-degree factor-return translated right-family bridge +# Liu left factor return: two-degree case -This module contains the translated right-family bridge, translated-compatible -wrappers, and original factor-return wrappers for the two-degree left -factor-return branch. Degree-case packaging and symmetry live downstream. +In a left Liu branch where `f` has degree two more than `g`, the +sign-normalized deletion pair has left endpoint one degree higher. After +translating the deleted largest root to the origin, the positive right +combinations of the restored pair are left-successor x-subtraction pencils. -/ open Polynomial Filter @@ -14,46 +16,14 @@ open Polynomial Filter namespace RealRooted namespace LiuOppositeSigns -/-- A `P := True` translated right-family predicate target gives the -unrestricted translated right-family target. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_predicate_true - (hright : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicateStatement - (fun _ => True)) : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyStatement := - theorem21LeftFactorReturnTranslatedRightFamilyRelation_of_predicate_true - (R := fun m n => m = n + 2) hright - -/-- The unrestricted translated right-family target is the `P := True` case of -the predicate-restricted target. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_true_of_rightFamily - (hright : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyStatement) : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicateStatement - (fun _ => True) := - theorem21LeftFactorReturnTranslatedRightFamilyPredicateRelation_true_of_relation - (R := fun m n => m = n + 2) hright - -/-- A degree-specific sign-normalized x-subtraction leaf gives the translated -right-family target after the Liu sign normalization. The predicate records -endpoint restrictions such as a fixed degree or a low-degree bound. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_xSub_rightPredicate - {P : ℕ → Prop} - (hterminal : - ∀ {p q : ℝ[X]} {a : ℝ}, - PositiveSplitRootCountPair p q → - HasNonnegCoeffs (p.comp (X + C a)) → - HasNonnegCoeffs (q.comp (X + C a)) → - p.natDegree = q.natDegree + 1 → - P q.natDegree → - ∀ μ : ℝ, 0 < μ → - (X * p.comp (X + C a) - C μ * q.comp (X + C a)).Splits) +/-- Two-degree left Liu branch: after translating the deleted largest root of +`f` to the origin, every positive right combination of the restored pair +splits. -/ +theorem theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily {f g : ℝ[X]} {r s : ℝ} (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 2) - (_hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : P g.natDegree) : + (hdeg : f.natDegree = g.natDegree + 2) : ∀ μ : ℝ, 0 < μ → (X * (deleteRootFactor f r).comp (X + C r) + C μ * g.comp (X + C r)).Splits := by @@ -76,9 +46,9 @@ theorem theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_xSub_rightPre have hdeg_pos : (deleteRootFactor f r).natDegree = (-g).natDegree + 1 := by simpa [Polynomial.natDegree_neg] using hdelete_deg - have hGdeg : P (-g).natDegree := by simpa [Polynomial.natDegree_neg] using hgdeg have hsplit := - hterminal hpair hqnn hGnn hdeg_pos hGdeg μ hμ + positiveSplitLeftSuccDegreeTranslatedXSubRightFamily r hpair hqnn hGnn + hdeg_pos μ hμ simpa [sub_eq_add_neg, mul_neg] using hsplit · have hQnn : HasNonnegCoeffs ((-(deleteRootFactor f r)).comp (X + C r)) := by @@ -93,323 +63,9 @@ theorem theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_xSub_rightPre (-(deleteRootFactor f r)).natDegree = g.natDegree + 1 := by simpa [Polynomial.natDegree_neg] using hdelete_deg have hsplit := - hterminal hpair hQnn hgnn hdeg_pos hgdeg μ hμ + positiveSplitLeftSuccDegreeTranslatedXSubRightFamily r hpair hQnn hgnn + hdeg_pos μ hμ simpa [sub_eq_add_neg, mul_neg, neg_add_rev, add_comm] using hsplit.neg -/-- Predicate-restricted positive-split x-subtraction families give the -corresponding translated two-degree right-family predicate target after the -Liu sign normalization. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - {P : ℕ → Prop} - (hterminal : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicateStatement - P := by - intro f g r s hf hg hsgn hleft hdeg hcommon hgdeg - exact theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_xSub_rightPredicate - (fun {p} {q} {a} hpair hpnn hqnn hpqdeg hp μ hμ => - hterminal a hpair hpnn hqnn hpqdeg hp μ hμ) - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Pack the degree-three-right endpoint terminal as a predicate-restricted -translated right-family target. -/ -theorem - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_rightDeg_three : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicateStatement - (fun n => n = 3) := - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_three - -/-- Pack the endpoint cases through right degree three as a predicate-restricted -translated right-family target. -/ -theorem - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_rightDeg_le_three : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicateStatement - (fun n => n ≤ 3) := - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - positiveSplitLeftSuccXSubFamilyPredicate_of_right_natDegree_le_three - -/-- A fixed right-degree sign-normalized x-subtraction leaf gives the translated -right-family target after the Liu sign normalization. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_xSub_rightDegree - {n : ℕ} - (hterminal : - ∀ {p q : ℝ[X]} {a : ℝ}, - PositiveSplitRootCountPair p q → - HasNonnegCoeffs (p.comp (X + C a)) → - HasNonnegCoeffs (q.comp (X + C a)) → - p.natDegree = q.natDegree + 1 → - q.natDegree = n → - ∀ μ : ℝ, 0 < μ → - (X * p.comp (X + C a) - C μ * q.comp (X + C a)).Splits) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 2) - (_hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = n) : - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits := - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - (P := fun m => m = n) - (fun {p} {q} a hpair hpnn hqnn hpqdeg hqdeg μ hμ => - hterminal (p := p) (q := q) (a := a) - hpair hpnn hqnn hpqdeg hqdeg μ hμ) - hf hg hsgn hleft hdeg _hcommon hgdeg - -/-- The sign-normalized positive-split subtraction-family leaf gives the -translated one-parameter target for the two-degree Liu left branch. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_xSub - (hsub : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyStatement := - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_predicate_true - (theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - (positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_true_of_xSub - hsub)) - -/-- Endpoint cases through right degree three for the translated two-degree Liu -right-family target. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedRightFamily_of_rightDeg_le_three - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 2) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree ≤ 3) : - ∀ μ : ℝ, 0 < μ → - (X * (deleteRootFactor f r).comp (X + C r) + - C μ * g.comp (X + C r)).Splits := by - exact - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_rightDeg_le_three - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- The positive right-pencil translated leaf gives the translated -compatibility leaf by scaling an arbitrary nonnegative linear combination. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedCompatible_of_rightFamily - (hright : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyStatement) : - theorem21LeftFactorReturnTwoDegreeTranslatedCompatibleStatement := - theorem21LeftFactorReturnTranslatedCompatible_of_rightFamilyRelation - (R := fun m n => m = n + 2) hright - -/-- Predicate-restricted translated right-family targets give the corresponding -pointwise translated compatibility target. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedCompatible_of_rightPredicate - {P : ℕ → Prop} - (hright : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicateStatement - P) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 2) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : P g.natDegree) : - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := - theorem21LeftFactorReturnTranslatedCompatible_of_rightPredicateRelation - (R := fun m n => m = n + 2) hright - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Predicate-restricted translated right-family targets give -predicate-restricted translated compatibility targets. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedCompatiblePredicate_of_rightPredicate - {P : ℕ → Prop} - (hright : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnTwoDegreeTranslatedCompatiblePredicateStatement - P := by - intro f g r s hf hg hsgn hleft hdeg hcommon hgdeg - exact theorem21LeftFactorReturnTwoDegreeTranslatedCompatible_of_rightPredicate - hright hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Pack the degree-three-right endpoint terminal as a predicate-restricted -translated compatibility target. -/ -theorem - theorem21LeftFactorReturnTwoDegreeTranslatedCompatiblePredicate_of_rightDeg_three : - theorem21LeftFactorReturnTwoDegreeTranslatedCompatiblePredicateStatement - (fun n => n = 3) := - theorem21LeftFactorReturnTwoDegreeTranslatedCompatiblePredicate_of_rightPredicate - (P := fun n => n = 3) - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_rightDeg_three - -/-- A `P := True` translated compatibility predicate target gives the -unrestricted translated compatibility target. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedCompatible_of_predicate_true - (htranslated : - theorem21LeftFactorReturnTwoDegreeTranslatedCompatiblePredicateStatement - (fun _ => True)) : - theorem21LeftFactorReturnTwoDegreeTranslatedCompatibleStatement := - theorem21LeftFactorReturnTranslatedCompatibleRelation_of_predicate_true - (R := fun m n => m = n + 2) htranslated - -/-- Degree-three-right-endpoint case for the translated two-degree Liu -compatibility target. -/ -theorem theorem21LeftFactorReturnTwoDegreeTranslatedCompatible_of_rightDeg_three - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 2) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 3) : - Compatible - (X * (deleteRootFactor f r).comp (X + C r)) - (g.comp (X + C r)) := by - exact - theorem21LeftFactorReturnTwoDegreeTranslatedCompatiblePredicate_of_rightDeg_three - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Predicate-restricted translated compatibility targets give the -corresponding predicate-restricted original two-degree factor-return targets. -/ -theorem theorem21LeftFactorReturnTwoDegreePredicate_of_translatedCompatiblePredicate - {P : ℕ → Prop} - (htranslated : - theorem21LeftFactorReturnTwoDegreeTranslatedCompatiblePredicateStatement - P) : - theorem21LeftFactorReturnTwoDegreePredicateStatement P := - theorem21LeftFactorReturnPredicate_of_translatedCompatibleRelation - (R := fun m n => m = n + 2) htranslated - -/-- The translated compatibility target gives the original two-degree -factor-return leaf by descending through the translation. -/ -theorem theorem21LeftFactorReturnTwoDegree_of_translatedCompatible - (htranslated : - theorem21LeftFactorReturnTwoDegreeTranslatedCompatibleStatement) : - theorem21LeftFactorReturnTwoDegreeStatement := - theorem21LeftFactorReturn_of_translatedCompatibleRelation - (R := fun m n => m = n + 2) htranslated - -/-- A translated positive right-family leaf gives the original two-degree -factor-return leaf. -/ -theorem theorem21LeftFactorReturnTwoDegree_of_rightFamily - (hright : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyStatement) : - theorem21LeftFactorReturnTwoDegreeStatement := - theorem21LeftFactorReturnTwoDegree_of_translatedCompatible - (theorem21LeftFactorReturnTwoDegreeTranslatedCompatible_of_rightFamily - hright) - -/-- Predicate-restricted translated right-family targets give the corresponding -original two-degree factor-return target. -/ -theorem theorem21LeftFactorReturnTwoDegree_of_rightPredicate - {P : ℕ → Prop} - (hright : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicateStatement - P) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 2) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : P g.natDegree) : - Compatible f g := - LiuOppositeSigns.theorem21LeftFactorReturn_of_pointwiseTranslatedCompatible hleft - (theorem21LeftFactorReturnTwoDegreeTranslatedCompatible_of_rightPredicate - hright hf hg hsgn hleft hdeg hcommon hgdeg) - -/-- Predicate-restricted left-successor sign-normalized x-subtraction leaves -give pointwise original two-degree factor-return targets. -/ -theorem theorem21LeftFactorReturnTwoDegree_of_xSubPredicate - {P : ℕ → Prop} - (hsub : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 2) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : P g.natDegree) : - Compatible f g := - theorem21LeftFactorReturnTwoDegree_of_rightPredicate - (theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - hsub) - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Predicate-restricted translated right-family targets give -predicate-restricted original factor-return targets. -/ -theorem theorem21LeftFactorReturnTwoDegreePredicate_of_rightPredicate - {P : ℕ → Prop} - (hright : - theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnTwoDegreePredicateStatement P := - theorem21LeftFactorReturnTwoDegreePredicate_of_translatedCompatiblePredicate - (theorem21LeftFactorReturnTwoDegreeTranslatedCompatiblePredicate_of_rightPredicate - hright) - -/-- Predicate-restricted positive-split x-subtraction families give -predicate-restricted original factor-return targets. -/ -theorem theorem21LeftFactorReturnTwoDegreePredicate_of_xSubPredicate - {P : ℕ → Prop} - (hsub : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P) : - theorem21LeftFactorReturnTwoDegreePredicateStatement P := - theorem21LeftFactorReturnTwoDegreePredicate_of_rightPredicate - (theorem21LeftFactorReturnTwoDegreeTranslatedRightFamilyPredicate_of_xSubPredicate - hsub) - -/-- A `P := True` original factor-return predicate target gives the -unrestricted two-degree factor-return target. -/ -theorem theorem21LeftFactorReturnTwoDegree_of_predicate_true - (htwo : - theorem21LeftFactorReturnTwoDegreePredicateStatement - (fun _ => True)) : - theorem21LeftFactorReturnTwoDegreeStatement := - theorem21LeftFactorReturnRelation_of_predicate_true - (R := fun m n => m = n + 2) htwo - -/-- The unrestricted two-degree factor-return target is the `P := True` case -of the predicate-restricted target. -/ -theorem theorem21LeftFactorReturnTwoDegreePredicate_true_of_twoDegree - (htwo : theorem21LeftFactorReturnTwoDegreeStatement) : - theorem21LeftFactorReturnTwoDegreePredicateStatement (fun _ => True) := - theorem21LeftFactorReturnPredicateRelation_true_of_relation - (R := fun m n => m = n + 2) htwo - -/-- The sign-normalized positive-split subtraction-family leaf gives the -original two-degree factor-return leaf. -/ -theorem theorem21LeftFactorReturnTwoDegree_of_xSub - (hsub : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21LeftFactorReturnTwoDegreeStatement := - theorem21LeftFactorReturnTwoDegree_of_predicate_true - (theorem21LeftFactorReturnTwoDegreePredicate_of_xSubPredicate - (positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_true_of_xSub - hsub)) - -/-- Degree-two-right endpoint case for the original two-degree left -factor-return leaf. -/ -theorem theorem21LeftFactorReturnTwoDegree_of_right_natDegree_two - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 2) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree = 2) : - Compatible f g := - theorem21LeftFactorReturnTwoDegree_of_xSubPredicate - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_two - hf hg hsgn hleft hdeg hcommon hgdeg - -/-- Endpoint cases through right degree three for the original two-degree left -factor-return leaf. -/ -theorem theorem21LeftFactorReturnTwoDegree_of_right_natDegree_le_three - {f g : ℝ[X]} {r s : ℝ} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hleft : LeftRootCountBranch f g r s) - (hdeg : f.natDegree = g.natDegree + 2) - (hcommon : ∃ k : ℝ[X], StrictInterl (deleteRootFactor f r) k ∧ StrictInterl g k) - (hgdeg : g.natDegree ≤ 3) : - Compatible f g := - theorem21LeftFactorReturnTwoDegree_of_xSubPredicate - positiveSplitLeftSuccXSubFamilyPredicate_of_right_natDegree_le_three - hf hg hsgn hleft hdeg hcommon hgdeg end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/ForwardLowDegree.lean b/RealRooted/LiuOppositeSigns/ForwardLowDegree.lean index 50c3c474d..bd7dfbb75 100644 --- a/RealRooted/LiuOppositeSigns/ForwardLowDegree.lean +++ b/RealRooted/LiuOppositeSigns/ForwardLowDegree.lean @@ -1,4 +1,4 @@ -import RealRooted.LiuOppositeSigns.Theorem21Assembly +import RealRooted.LiuOppositeSigns.FactorReturnAssembly /-! # Liu low-degree forward branch lemmas diff --git a/RealRooted/LiuOppositeSigns/Theorem.lean b/RealRooted/LiuOppositeSigns/Theorem.lean index a04e2ff70..1b5921c9e 100644 --- a/RealRooted/LiuOppositeSigns/Theorem.lean +++ b/RealRooted/LiuOppositeSigns/Theorem.lean @@ -1,22 +1,22 @@ import RealRooted.LiuOppositeSigns.BoundedIntervalContinuity import RealRooted.LiuOppositeSigns.CommonInterleaverConsequences -import RealRooted.LiuOppositeSigns.Corollary22 +import RealRooted.LiuOppositeSigns.ForwardLowDegree import RealRooted.LiuOppositeSigns.DerivativeShiftSequenceRegularization import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderAssembly import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderLower import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderUpper import RealRooted.LiuOppositeSigns.RootCountClosure -import RealRooted.LiuOppositeSigns.Theorem21Assembly +import RealRooted.LiuOppositeSigns.FactorReturnAssembly import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount import RealRooted.ObreschkoffConverse /-! # Liu opposite-sign compatibility theorem -This module contains the low-degree and analytic proof machinery for the -Liu opposite-sign compatibility theorem. The theorem statement and -projection interface live in -`RealRooted.LiuOppositeSigns.Theorem21Statements`. +This module proves the no-common-root forward direction of Liu's +opposite-sign compatibility theorem by derivative-shift regularization, +combines it with the factor-return reverse direction and common-root deletion +into the corrected Theorem 2.1, and proves Corollary 2.2. -/ open Polynomial Filter @@ -29,9 +29,12 @@ namespace LiuOppositeSigns The derivative-shift regularization repairs the source's invalid inference from no common roots to simple roots. The simple-root argument is applied to arbitrarily close regularizations, and root matching closes the result. -/ -theorem theorem21CompatibleToRootCountBranchesNoCommonNonconstant : - theorem21CompatibleToRootCountBranchesNoCommonNonconstantStatement := by - intro f g hf hg hsgn hno hf_deg hg_deg hcompat +theorem theorem21CompatibleToRootCountBranchesNoCommonNonconstant + {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) + (hsgn : OppositeLeadingSigns f g) (hno : NoCommonRoots f g) + (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) + (hcompat : Compatible f g) : + theorem21RootCountBranches f g := by apply theorem21RootCountBranches_of_forall_pos_exists_roots_rel hsgn.left_ne_zero hsgn.right_ne_zero hf hg hno hf_deg hg_deg intro ρ hρ @@ -76,14 +79,14 @@ theorem theorem21CompatibleToRootCountBranchesNoCommonNonconstant : · simpa [g'] using hgrel /-- The nonconstant no-common-root form of Liu Theorem 2.1. -/ -theorem theorem21CompatibleRootCountNoCommonNonconstant : - theorem21CompatibleRootCountNoCommonNonconstantStatement := by - intro f g hf hg hsgn hno hf_deg hg_deg - exact - ⟨theorem21CompatibleToRootCountBranchesNoCommonNonconstant - hf hg hsgn hno hf_deg hg_deg, - theorem21RootCountBranchesToCompatibleNonconstant_of_xSub - hf hg hsgn hf_deg hg_deg⟩ +theorem theorem21CompatibleRootCountNoCommonNonconstant + {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) + (hsgn : OppositeLeadingSigns f g) (hno : NoCommonRoots f g) + (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) : + Compatible f g ↔ theorem21RootCountBranches f g := + ⟨theorem21CompatibleToRootCountBranchesNoCommonNonconstant + hf hg hsgn hno hf_deg hg_deg, + compatible_of_theorem21RootCountBranches hf hg hsgn⟩ /-- Compatible no-common nonconstant opposite-sign pairs have degree gap at most two. -/ @@ -122,8 +125,7 @@ theorem compatible_iff_theorem21RootCountBranchesReduced_nonconstant hcompat hno) · intro hbranches rcases hbranches with hbranches | hcommon - · exact theorem21RootCountBranchesToCompatibleNonconstant_of_xSub - hf hg hsgn hf_deg hg_deg hbranches.2 + · exact compatible_of_theorem21RootCountBranches hf hg hsgn hbranches.2 · exact hcommon.compatible /-- Public-facing correct nonconstant Liu equivalence. Compared with the @@ -141,35 +143,9 @@ theorem compatible_iff_theorem21RootCountBranchesWithCommon_nonconstant hf hg hsgn hf_deg hg_deg).mp hcompat) · intro hbranches rcases hbranches with hbranches | hcommon - · exact theorem21RootCountBranchesToCompatibleNonconstant_of_xSub - hf hg hsgn hf_deg hg_deg hbranches + · exact compatible_of_theorem21RootCountBranches hf hg hsgn hbranches · exact hcommon.compatible -/-- The isolated forward direction of Liu Theorem 2.1 gives the oriented -branch-wise pointwise root-count bounds. -/ -theorem rootCountAtOrAbove_branch_bounds_of_compatible_of_forward - (hforward : theorem21CompatibleToRootCountBranchesStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : - (∀ x : ℝ, - ((rootCountAtOrAbove f x : ℤ) - (rootCountAtOrAbove g x : ℤ)) ≤ 2 ∧ - ((rootCountAtOrAbove g x : ℤ) - (rootCountAtOrAbove f x : ℤ)) ≤ 1) ∨ - (∀ x : ℝ, - ((rootCountAtOrAbove f x : ℤ) - (rootCountAtOrAbove g x : ℤ)) ≤ 1 ∧ - ((rootCountAtOrAbove g x : ℤ) - (rootCountAtOrAbove f x : ℤ)) ≤ 2) := - rootCountAtOrAbove_branch_bounds_of_theorem21RootCountBranches hsgn - (hforward hf hg hsgn hcompat) - -/-- The isolated forward direction of Liu Theorem 2.1 gives the normalized -positive-deletion count branches. -/ -theorem theorem21PositiveDeletionCountBranches_of_compatible_of_forward - (hforward : theorem21CompatibleToRootCountBranchesStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : - theorem21PositiveDeletionCountBranches f g := - theorem21PositiveDeletionCountBranches_of_theorem21RootCountBranches hf hg hsgn - (hforward hf hg hsgn hcompat) - /-- Guardrail for the factor-return route: multiplying the higher-degree member of a simple quadratic/linear interlacing pair by `X` need not preserve all-combinations real-rootedness. Thus the Liu factor-return proof cannot use @@ -289,13 +265,13 @@ lemma natDegree_abs_sub_le_two_of_compatible_of_right_natDegree_eq_zero /-- Liu's Corollary 2.2: compatible real-rooted polynomials with opposite leading signs have degrees differing by at most two. -/ -theorem corollary22DegreeDiff_proof : corollary22DegreeDiffStatement := by - unfold corollary22DegreeDiffStatement +theorem corollary22DegreeDiff {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) + (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : + |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 := by suffices h : ∀ n : ℕ, ∀ f g : ℝ[X], f.natDegree + g.natDegree = n → f.Splits → g.Splits → OppositeLeadingSigns f g → Compatible f g → |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 by - intro f g hf hg hsgn hcompat exact h _ f g rfl hf hg hsgn hcompat intro n induction n using Nat.strong_induction_on with @@ -342,6 +318,5 @@ theorem corollary22DegreeDiff_proof : corollary22DegreeDiffStatement := by norm_num at hrec simpa only [sub_sub_sub_cancel_right] using hrec - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/Theorem21Assembly.lean b/RealRooted/LiuOppositeSigns/Theorem21Assembly.lean deleted file mode 100644 index 56652578e..000000000 --- a/RealRooted/LiuOppositeSigns/Theorem21Assembly.lean +++ /dev/null @@ -1,695 +0,0 @@ -import RealRooted.LiuOppositeSigns.FactorReturnAssembly - -/-! -# Liu theorem reverse root-count assembly - -This module contains the reverse root-count assembly layer for Liu Theorem 2.1, -including predicate-restricted branch packages and the current low-endpoint -reverse routes. --/ - -open Polynomial Filter - -namespace RealRooted -namespace LiuOppositeSigns - -/-- Predicate-restricted Liu root-count branch data. The predicate is imposed -on the lower-degree endpoint selected by the branch. -/ -def theorem21RootCountBranchesPredicate (P : ℕ → Prop) (f g : ℝ[X]) : - Prop := - ∃ r s, - (LeftRootCountBranch f g r s ∧ P g.natDegree) ∨ - (RightRootCountBranch f g r s ∧ P f.natDegree) - -theorem theorem21RootCountBranchesPredicate_of_left - {P : ℕ → Prop} {f g : ℝ[X]} {r s : ℝ} - (hleft : LeftRootCountBranch f g r s) (hP : P g.natDegree) : - theorem21RootCountBranchesPredicate P f g := - ⟨r, s, Or.inl ⟨hleft, hP⟩⟩ - -theorem theorem21RootCountBranchesPredicate_of_right - {P : ℕ → Prop} {f g : ℝ[X]} {r s : ℝ} - (hright : RightRootCountBranch f g r s) (hP : P f.natDegree) : - theorem21RootCountBranchesPredicate P f g := - ⟨r, s, Or.inr ⟨hright, hP⟩⟩ - -/-- Predicate-restricted Liu branch data transports along endpoint predicate -implications. -/ -theorem theorem21RootCountBranchesPredicate_of_imp - {P Q : ℕ → Prop} (hPQ : ∀ n, P n → Q n) {f g : ℝ[X]} - (hbranches : theorem21RootCountBranchesPredicate P f g) : - theorem21RootCountBranchesPredicate Q f g := by - rcases hbranches with ⟨r, s, hleft | hright⟩ - · exact theorem21RootCountBranchesPredicate_of_left hleft.1 - (hPQ _ hleft.2) - · exact theorem21RootCountBranchesPredicate_of_right hright.1 - (hPQ _ hright.2) - -/-- Predicate-restricted Liu root-count branch data forgets to the ordinary -branch statement. -/ -theorem theorem21RootCountBranches_of_predicate - {P : ℕ → Prop} {f g : ℝ[X]} - (h : theorem21RootCountBranchesPredicate P f g) : - theorem21RootCountBranches f g := by - rcases h with ⟨r, s, hleft | hright⟩ - · exact theorem21RootCountBranches_of_left hleft.1 - · exact theorem21RootCountBranches_of_right hright.1 - -/-- The unrestricted branch statement is the `P := True` case of the -predicate-restricted branch statement. -/ -theorem theorem21RootCountBranchesPredicate_true_iff {f g : ℝ[X]} : - theorem21RootCountBranchesPredicate (fun _ => True) f g ↔ - theorem21RootCountBranches f g := by - constructor - · exact theorem21RootCountBranches_of_predicate - · intro h - rcases h with ⟨r, s, hleft | hright⟩ - · exact theorem21RootCountBranchesPredicate_of_left hleft trivial - · exact theorem21RootCountBranchesPredicate_of_right hright trivial - -/-- Predicate-restricted reverse half of Liu Theorem 2.1. The predicate is -attached to the lower-degree endpoint in the selected branch. -/ -def theorem21RootCountBranchesToCompatiblePredicateStatement - (P : ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - theorem21RootCountBranchesPredicate P f g → Compatible f g - -/-- Reassemble Liu Theorem 2.1 from separately proved forward and reverse -directions. -/ -theorem theorem21CompatibleRootCount_of_forward_and_reverse - (hforward : theorem21CompatibleToRootCountBranchesStatement) - (hreverse : theorem21RootCountBranchesToCompatibleStatement) : - theorem21CompatibleRootCountStatement := by - intro f g hf hg hsgn - exact ⟨hforward hf hg hsgn, hreverse hf hg hsgn⟩ - -/-- Predicate-restricted nonconstant reverse half of Liu Theorem 2.1. -/ -def theorem21RootCountBranchesToCompatiblePredicateNonconstantStatement - (P : ℕ → Prop) : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - theorem21RootCountBranchesPredicate P f g → Compatible f g - -/-- The branch-retaining deletion-pair package reduces the reverse direction -of Liu Theorem 2.1 to the explicit factor-return principle. -/ -theorem theorem21RootCountBranchesToCompatible_of_deletionPairFactorReturn - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21RootCountBranchesToCompatibleStatement := by - intro f g hf hg hsgn hbranches - exact theorem21DeletionPairCommonInterleaverBranchesToCompatible_of_factorReturn - hreturn hf hg hsgn - (theorem21DeletionPairCommonInterleaverBranches_of_theorem21RootCountBranches - hf hg hsgn hbranches) - -/-- The factor-return principle proves the no-common-root reverse root-count -direction. -/ -theorem - theorem21RootCountBranchesToCompatibleNoCommon_of_deletionPairFactorReturn - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21RootCountBranchesToCompatibleNoCommonStatement := - theorem21RootCountBranchesToCompatibleNoCommon_of_reverse - (theorem21RootCountBranchesToCompatible_of_deletionPairFactorReturn - hreturn) - -/-- The factor-return principle proves the reduced common-root reverse -direction. -/ -theorem theorem21RootCountBranchesReducedToCompatible_of_factorReturn - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21RootCountBranchesReducedToCompatibleStatement := - theorem21RootCountBranchesReducedToCompatible_of_noCommonReverse - (theorem21RootCountBranchesToCompatibleNoCommon_of_deletionPairFactorReturn - hreturn) - -/-- The no-common forward direction and factor-return principle assemble the -reduced common-root Liu target. -/ -theorem theorem21CompatibleRootCountReduced_of_noCommonForward_and_factorReturn - (hforward : theorem21CompatibleToRootCountBranchesNoCommonStatement) - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21CompatibleRootCountReducedStatement := - theorem21CompatibleRootCountReduced_of_forward_and_reverse - (theorem21CompatibleToRootCountBranchesReduced_of_noCommonForward hforward) - (theorem21RootCountBranchesReducedToCompatible_of_factorReturn hreturn) - -/-- A bundled sign-normalized positive-split x-subtraction case package proves -the reverse root-count direction. -/ -theorem theorem21RootCountBranchesToCompatible_of_xSubCasePackage - (hcases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesStatement) : - theorem21RootCountBranchesToCompatibleStatement := - theorem21RootCountBranchesToCompatible_of_deletionPairFactorReturn - (theorem21DeletionPairCommonInterleaverFactorReturn_of_xSubCasePackage - hcases) - -/-- The proved sign-normalized positive-split x-subtraction cases prove the -reverse root-count direction. -/ -theorem theorem21RootCountBranchesToCompatible_of_xSub : - theorem21RootCountBranchesToCompatibleStatement := - theorem21RootCountBranchesToCompatible_of_xSubCasePackage - positiveSplitTranslatedXSubRightFamilyDegreeCases - -/-- Any reverse root-count direction restricts to endpoint predicate -subfamilies. -/ -theorem theorem21RootCountBranchesToCompatiblePredicate_of_reverse - {P : ℕ → Prop} - (hreverse : theorem21RootCountBranchesToCompatibleStatement) : - theorem21RootCountBranchesToCompatiblePredicateStatement P := by - intro f g hf hg hsgn hbranches - exact hreverse hf hg hsgn - (theorem21RootCountBranches_of_predicate hbranches) - -/-- Predicate-restricted factor-return proves the predicate-restricted reverse -root-count direction. -/ -theorem - theorem21RootCountBranchesToCompatiblePredicate_of_deletionPairFactorReturnPredicate - {P : ℕ → Prop} - (hreturn : - theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement P) : - theorem21RootCountBranchesToCompatiblePredicateStatement P := by - intro f g hf hg hsgn hbranches - rcases hbranches with ⟨r, s, hleft | hright⟩ - · exact (hreturn hf hg hsgn).1 hleft.1 - (hleft.1.deletePairHasCommonInterleaver hsgn hf hg) hleft.2 - · exact (hreturn hf hg hsgn).2 hright.1 - (hright.1.deletePairHasCommonInterleaver hsgn hf hg) hright.2 - -/-- Bundled predicate-restricted positive-split x-subtraction case packages -prove the corresponding predicate-restricted reverse root-count direction. -/ -theorem theorem21RootCountBranchesToCompatiblePredicate_of_xSubCasePackage - {P : ℕ → Prop} - (hcases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement P) : - theorem21RootCountBranchesToCompatiblePredicateStatement P := - theorem21RootCountBranchesToCompatiblePredicate_of_deletionPairFactorReturnPredicate - (theorem21FactorReturnPredicate_of_xSubCasePackage hcases) - -/-- The proved sign-normalized positive-split x-subtraction cases prove every -predicate-restricted reverse root-count direction. -/ -theorem theorem21RootCountBranchesToCompatiblePredicate_of_xSub - {P : ℕ → Prop} : - theorem21RootCountBranchesToCompatiblePredicateStatement P := - theorem21RootCountBranchesToCompatiblePredicate_of_xSubCasePackage - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate - -/-- The unrestricted factor-return principle proves every predicate-restricted -reverse root-count direction by forgetting the endpoint predicate. -/ -theorem theorem21RootCountBranchesToCompatiblePredicate_of_deletionPairFactorReturn - {P : ℕ → Prop} - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21RootCountBranchesToCompatiblePredicateStatement P := - theorem21RootCountBranchesToCompatiblePredicate_of_deletionPairFactorReturnPredicate - (theorem21DeletionPairCommonInterleaverFactorReturnPredicate_of_factorReturn - hreturn) - -/-- A `P := True` predicate-restricted reverse direction gives the ordinary -reverse root-count direction. -/ -theorem theorem21RootCountBranchesToCompatible_of_predicate_true - (hreverse : - theorem21RootCountBranchesToCompatiblePredicateStatement - (fun _ => True)) : - theorem21RootCountBranchesToCompatibleStatement := by - intro f g hf hg hsgn hbranches - exact hreverse hf hg hsgn - (theorem21RootCountBranchesPredicate_true_iff.mpr hbranches) - -/-- Predicate-`True` reverse root-count direction is equivalent to the -ordinary reverse root-count direction. -/ -theorem theorem21RootCountBranchesToCompatiblePredicate_true_iff : - theorem21RootCountBranchesToCompatiblePredicateStatement - (fun _ => True) ↔ theorem21RootCountBranchesToCompatibleStatement := - ⟨theorem21RootCountBranchesToCompatible_of_predicate_true, - theorem21RootCountBranchesToCompatiblePredicate_of_reverse⟩ - -/-- A predicate-restricted reverse direction also gives the corresponding -nonconstant predicate-restricted reverse direction. -/ -theorem - theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_predicate - {P : ℕ → Prop} - (hreverse : theorem21RootCountBranchesToCompatiblePredicateStatement P) : - theorem21RootCountBranchesToCompatiblePredicateNonconstantStatement P := by - intro f g hf hg hsgn _hf_deg _hg_deg hbranches - exact hreverse hf hg hsgn hbranches - -/-- Bundled predicate-restricted positive-split x-subtraction case packages -prove the corresponding nonconstant predicate-restricted reverse root-count -direction. -/ -theorem - theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_xSubCasePackage - {P : ℕ → Prop} - (hcases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement P) : - theorem21RootCountBranchesToCompatiblePredicateNonconstantStatement P := - theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_predicate - (theorem21RootCountBranchesToCompatiblePredicate_of_xSubCasePackage - hcases) - -/-- The proved sign-normalized positive-split x-subtraction cases prove every -nonconstant predicate-restricted reverse root-count direction. -/ -theorem theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_xSub - {P : ℕ → Prop} : - theorem21RootCountBranchesToCompatiblePredicateNonconstantStatement P := - theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_xSubCasePackage - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate - -/-- The unrestricted factor-return principle proves every nonconstant -predicate-restricted reverse root-count direction by forgetting the endpoint -predicate. -/ -theorem - theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_deletionPairFactorReturn - {P : ℕ → Prop} - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21RootCountBranchesToCompatiblePredicateNonconstantStatement P := - theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_predicate - (theorem21RootCountBranchesToCompatiblePredicate_of_deletionPairFactorReturn - hreturn) - -/-- A `P := True` predicate-restricted nonconstant reverse direction gives the -ordinary nonconstant reverse root-count direction. -/ -theorem theorem21RootCountBranchesToCompatibleNonconstant_of_predicate_true - (hreverse : - theorem21RootCountBranchesToCompatiblePredicateNonconstantStatement - (fun _ => True)) : - theorem21RootCountBranchesToCompatibleNonconstantStatement := by - intro f g hf hg hsgn hf_deg hg_deg hbranches - exact hreverse hf hg hsgn hf_deg hg_deg - (theorem21RootCountBranchesPredicate_true_iff.mpr hbranches) - -/-- The proved sign-normalized positive-split x-subtraction cases prove the -nonconstant reverse root-count direction. -/ -theorem theorem21RootCountBranchesToCompatibleNonconstant_of_xSub : - theorem21RootCountBranchesToCompatibleNonconstantStatement := - theorem21RootCountBranchesToCompatibleNonconstant_of_predicate_true - theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_xSub - -/-- The isolated forward direction plus the proved x-subtraction reverse route -give Liu Theorem 2.1 in root-count form. -/ -theorem theorem21CompatibleRootCount_of_forward_and_xSub - (hforward : theorem21CompatibleToRootCountBranchesStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_forward_and_reverse hforward - theorem21RootCountBranchesToCompatible_of_xSub - -/-- The no-common forward direction plus the proved x-subtraction reverse route -give the reduced common-root Liu Theorem 2.1 statement in root-count form. -/ -theorem theorem21CompatibleRootCountReduced_of_noCommonForward_and_xSub - (hforward : theorem21CompatibleToRootCountBranchesNoCommonStatement) : - theorem21CompatibleRootCountReducedStatement := - theorem21CompatibleRootCountReduced_of_noCommon_forward_and_reverse hforward - (theorem21RootCountBranchesToCompatibleNoCommon_of_reverse - theorem21RootCountBranchesToCompatible_of_xSub) - -/-- The no-common forward direction plus the proved x-subtraction reverse route -give the corrected common-root-branch Liu Theorem 2.1 statement in root-count -form. -/ -theorem theorem21CompatibleRootCountWithCommon_of_noCommonForward_and_xSub - (hforward : theorem21CompatibleToRootCountBranchesNoCommonStatement) : - theorem21CompatibleRootCountWithCommonStatement := - theorem21CompatibleRootCountWithCommon_of_noCommonForward_and_reverse hforward - theorem21RootCountBranchesToCompatible_of_xSub - -/-- Liu Theorem 2.1 follows from the isolated forward direction and a -predicate-`True` reverse direction. -/ -theorem theorem21CompatibleRootCount_of_commonForward_and_predicate_true - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - (hreverse : - theorem21RootCountBranchesToCompatiblePredicateStatement - (fun _ => True)) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_forward_and_reverse - (theorem21CompatibleToRootCountBranches_of_commonForward hforward) - (theorem21RootCountBranchesToCompatible_of_predicate_true hreverse) - -/-- Liu Theorem 2.1 follows from the isolated root-count forward direction and -a predicate-`True` reverse direction. -/ -theorem theorem21CompatibleRootCount_of_forward_and_predicate_true - (hforward : theorem21CompatibleToRootCountBranchesStatement) - (hreverse : - theorem21RootCountBranchesToCompatiblePredicateStatement - (fun _ => True)) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_predicate_true - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - hreverse - -/-- Liu Theorem 2.1 follows from the isolated forward root-count direction and -the deletion-pair factor-return principle. -/ -theorem theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturn - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_deletionPairCommonInterleaverIff - (theorem21DeletionPairCommonInterleaverIff_of_commonForward_and_factorReturn - hforward hreturn) - -/-- Liu Theorem 2.1 follows from the isolated root-count forward direction and -the deletion-pair factor-return principle. -/ -theorem theorem21CompatibleRootCount_of_forward_and_deletionPairFactorReturn - (hforward : theorem21CompatibleToRootCountBranchesStatement) - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturn - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - hreturn - -/-- Liu Theorem 2.1 follows from the isolated forward direction and an -all-combinations factor-return principle. -/ -theorem - theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturnAllCombo - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - (hreturn : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturn - hforward - (theorem21DeletionPairCommonInterleaverFactorReturn_of_allCombo hreturn) - -/-- Liu Theorem 2.1 follows from the isolated root-count forward direction and -an all-combinations factor-return principle. -/ -theorem - theorem21CompatibleRootCount_of_forward_and_deletionPairFactorReturnAllCombo - (hforward : theorem21CompatibleToRootCountBranchesStatement) - (hreturn : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturnAllCombo - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - hreturn - -/-- Liu Theorem 2.1 follows from the isolated forward direction and -all-combinations factor-return degree cases. -/ -theorem theorem21CompatibleRootCount_of_commonForward_and_allComboDegreeCases - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - (hcases : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCasesStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturn - hforward - (theorem21DeletionPairCommonInterleaverFactorReturn_of_allComboDegreeCases - hcases) - -/-- Liu Theorem 2.1 follows from the isolated root-count forward direction and -all-combinations factor-return degree cases. -/ -theorem theorem21CompatibleRootCount_of_forward_and_allComboDegreeCases - (hforward : theorem21CompatibleToRootCountBranchesStatement) - (hcases : - theorem21DeletionPairCommonInterleaverFactorReturnAllComboDegreeCasesStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_allComboDegreeCases - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - hcases - -/-- Liu Theorem 2.1 follows from the isolated forward direction and left -all-combinations factor-return degree cases, with right cases supplied by -symmetry. -/ -theorem theorem21CompatibleRootCount_of_commonForward_and_leftAllComboCases - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - (hcases : theorem21LeftFactorReturnAllComboDegreeCasesStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturn - hforward - (theorem21DeletionPairCommonInterleaverFactorReturn_of_leftAllComboCases - hcases) - -/-- Liu Theorem 2.1 follows from the isolated root-count forward direction and -left all-combinations factor-return degree cases, with right cases supplied by -symmetry. -/ -theorem theorem21CompatibleRootCount_of_forward_and_leftAllComboCases - (hforward : theorem21CompatibleToRootCountBranchesStatement) - (hcases : theorem21LeftFactorReturnAllComboDegreeCasesStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_leftAllComboCases - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - hcases - -/-- Liu Theorem 2.1 follows from the isolated forward direction and a bundled -sign-normalized positive-split x-subtraction case package. -/ -theorem theorem21CompatibleRootCount_of_commonForward_and_xSubCasePackage - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - (hcases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturn - hforward - (theorem21DeletionPairCommonInterleaverFactorReturn_of_xSubCasePackage - hcases) - -/-- Liu Theorem 2.1 follows from the isolated root-count forward direction and -a bundled sign-normalized positive-split x-subtraction case package. -/ -theorem theorem21CompatibleRootCount_of_forward_and_xSubCasePackage - (hforward : theorem21CompatibleToRootCountBranchesStatement) - (hcases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_xSubCasePackage - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - hcases - -/-- Liu Theorem 2.1 follows from the isolated forward direction and -sign-normalized positive-split x-subtraction cases. -/ -theorem theorem21CompatibleRootCount_of_commonForward_and_xSubCases - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - (hrightSucc : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement) - (hsame : positiveSplitSameDegreeTranslatedXSubRightFamilyStatement) - (hleftSucc : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_xSubCasePackage - hforward ⟨hrightSucc, hsame, hleftSucc⟩ - -/-- Liu Theorem 2.1 follows from the isolated root-count forward direction and -sign-normalized positive-split x-subtraction cases. -/ -theorem theorem21CompatibleRootCount_of_forward_and_xSubCases - (hforward : theorem21CompatibleToRootCountBranchesStatement) - (hrightSucc : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement) - (hsame : positiveSplitSameDegreeTranslatedXSubRightFamilyStatement) - (hleftSucc : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_xSubCases - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - hrightSucc hsame hleftSucc - -/-- Liu Theorem 2.1 follows from the isolated forward direction and a -predicate-`True` factor-return principle. -/ -theorem - theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturnPredicate_true - (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement) - (hreturn : - theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement - (fun _ => True)) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturn - hforward - (theorem21DeletionPairCommonInterleaverFactorReturn_of_predicate_true - hreturn) - -/-- Liu Theorem 2.1 follows from the isolated root-count forward direction and -a predicate-`True` factor-return principle. -/ -theorem - theorem21CompatibleRootCount_of_forward_and_deletionPairFactorReturnPredicate_true - (hforward : theorem21CompatibleToRootCountBranchesStatement) - (hreturn : - theorem21DeletionPairCommonInterleaverFactorReturnPredicateStatement - (fun _ => True)) : - theorem21CompatibleRootCountStatement := - theorem21CompatibleRootCount_of_commonForward_and_deletionPairFactorReturnPredicate_true - (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward - hforward) - hreturn - -/-- The deletion-pair factor-return principle also reduces the nonconstant -reverse direction of Liu Theorem 2.1. -/ -theorem theorem21RootCountBranchesToCompatibleNonconstant_of_deletionPairFactorReturn - (hreturn : theorem21DeletionPairCommonInterleaverFactorReturnStatement) : - theorem21RootCountBranchesToCompatibleNonconstantStatement := - theorem21RootCountBranchesToCompatibleNonconstant_of_predicate_true - (theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_deletionPairFactorReturn - hreturn) - -/-- Current low-endpoint reverse route: Liu's reverse direction holds for -branches whose lower-degree endpoint has degree at most two. -/ -theorem theorem21RootCountBranchesToCompatiblePredicate_of_endpoint_le_two : - theorem21RootCountBranchesToCompatiblePredicateStatement - (fun n => n ≤ 2) := - theorem21RootCountBranchesToCompatiblePredicate_of_xSubCasePackage - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate_of_endpoint_le_two - -/-- Endpoint-degree-two branch data for the current bounded Liu reverse route. -This is the predicate-restricted branch statement with predicate `n ≤ 2` on the -lower-degree endpoint. -/ -def theorem21RootCountBranchesEndpointLeTwo (f g : ℝ[X]) : Prop := - theorem21RootCountBranchesPredicate (fun n => n ≤ 2) f g - -/-- Left-branch constructor for endpoint-degree-two branch data. -/ -theorem theorem21RootCountBranchesEndpointLeTwo_of_left - {f g : ℝ[X]} {r s : ℝ} (hleft : LeftRootCountBranch f g r s) - (hgdeg : g.natDegree ≤ 2) : - theorem21RootCountBranchesEndpointLeTwo f g := - theorem21RootCountBranchesPredicate_of_left hleft hgdeg - -/-- Right-branch constructor for endpoint-degree-two branch data. -/ -theorem theorem21RootCountBranchesEndpointLeTwo_of_right - {f g : ℝ[X]} {r s : ℝ} (hright : RightRootCountBranch f g r s) - (hfdeg : f.natDegree ≤ 2) : - theorem21RootCountBranchesEndpointLeTwo f g := - theorem21RootCountBranchesPredicate_of_right hright hfdeg - -/-- Ordinary branch data becomes endpoint-degree-two branch data when both -endpoints have degree at most two. -/ -theorem theorem21RootCountBranchesEndpointLeTwo_of_natDegree_le_two - {f g : ℝ[X]} (hfdeg : f.natDegree ≤ 2) (hgdeg : g.natDegree ≤ 2) - (hbranches : theorem21RootCountBranches f g) : - theorem21RootCountBranchesEndpointLeTwo f g := by - rcases hbranches with ⟨r, s, hleft | hright⟩ - · exact theorem21RootCountBranchesEndpointLeTwo_of_left hleft hgdeg - · exact theorem21RootCountBranchesEndpointLeTwo_of_right hright hfdeg - -/-- Low-endpoint reverse route: Liu's reverse direction holds for branches whose -lower-degree endpoint has degree at most two. -/ -theorem theorem21RootCountBranchesToCompatible_of_endpoint_le_two : - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - theorem21RootCountBranchesEndpointLeTwo f g → Compatible f g := by - intro f g hf hg hsgn hbranches - exact theorem21RootCountBranchesToCompatiblePredicate_of_endpoint_le_two - hf hg hsgn hbranches - -/-- Low-degree endpoints turn the endpoint-degree-two reverse route into an -ordinary reverse implication. -/ -theorem theorem21RootCountBranchesToCompatible_of_natDegree_le_two - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) - (hfdeg : f.natDegree ≤ 2) (hgdeg : g.natDegree ≤ 2) - (hbranches : theorem21RootCountBranches f g) : - Compatible f g := - theorem21RootCountBranchesToCompatible_of_endpoint_le_two hf hg hsgn - (theorem21RootCountBranchesEndpointLeTwo_of_natDegree_le_two - hfdeg hgdeg hbranches) - -/-- Endpoint-degree-three branch data for the current bounded Liu reverse -route. This is just the predicate-restricted branch statement with predicate -`n ≤ 3` on the lower-degree endpoint. -/ -def theorem21RootCountBranchesEndpointLeThree (f g : ℝ[X]) : Prop := - theorem21RootCountBranchesPredicate (fun n => n ≤ 3) f g - -/-- Left-branch constructor for endpoint-degree-three branch data. -/ -theorem theorem21RootCountBranchesEndpointLeThree_of_left - {f g : ℝ[X]} {r s : ℝ} (hleft : LeftRootCountBranch f g r s) - (hgdeg : g.natDegree ≤ 3) : - theorem21RootCountBranchesEndpointLeThree f g := - theorem21RootCountBranchesPredicate_of_left hleft hgdeg - -/-- Right-branch constructor for endpoint-degree-three branch data. -/ -theorem theorem21RootCountBranchesEndpointLeThree_of_right - {f g : ℝ[X]} {r s : ℝ} (hright : RightRootCountBranch f g r s) - (hfdeg : f.natDegree ≤ 3) : - theorem21RootCountBranchesEndpointLeThree f g := - theorem21RootCountBranchesPredicate_of_right hright hfdeg - -/-- Ordinary branch data becomes endpoint-degree-three branch data when both -endpoints have degree at most three. -/ -theorem theorem21RootCountBranchesEndpointLeThree_of_natDegree_le_three - {f g : ℝ[X]} (hfdeg : f.natDegree ≤ 3) (hgdeg : g.natDegree ≤ 3) - (hbranches : theorem21RootCountBranches f g) : - theorem21RootCountBranchesEndpointLeThree f g := by - rcases hbranches with ⟨r, s, hleft | hright⟩ - · exact theorem21RootCountBranchesEndpointLeThree_of_left hleft hgdeg - · exact theorem21RootCountBranchesEndpointLeThree_of_right hright hfdeg - -/-- Endpoint-degree-two branch data is a subcase of endpoint-degree-three branch -data. -/ -theorem theorem21RootCountBranchesEndpointLeThree_of_endpoint_le_two - {f g : ℝ[X]} : - theorem21RootCountBranchesEndpointLeTwo f g → - theorem21RootCountBranchesEndpointLeThree f g := - theorem21RootCountBranchesPredicate_of_imp fun _ hn => - hn.trans (by norm_num) - -/-- Bundled predicate-restricted x-subtraction cases prove the nonconstant -endpoint-degree-three reverse route. -/ -theorem - theorem21RootCountBranchesToCompatibleNonconstant_of_endpoint_le_three_xSubCasePackage - (hcases : - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicateStatement - (fun n => n ≤ 3)) : - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - theorem21RootCountBranchesEndpointLeThree f g → Compatible f g := by - intro f g hf hg hsgn hf_deg hg_deg hbranches - exact theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_xSubCasePackage - hcases hf hg hsgn hf_deg hg_deg hbranches - -/-- Nonconstant wrapper for the endpoint-degree-three reverse route. -/ -theorem theorem21RootCountBranchesToCompatibleNonconstant_of_endpoint_le_three : - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - theorem21RootCountBranchesEndpointLeThree f g → Compatible f g := by - intro f g hf hg hsgn _hf_deg _hg_deg hbranches - exact - theorem21RootCountBranchesToCompatibleNonconstant_of_endpoint_le_three_xSubCasePackage - positiveSplitTranslatedXSubRightFamilyDegreeCasesPredicate_of_endpoint_le_three - hf hg hsgn _hf_deg _hg_deg hbranches - -/-- Degree-case-aware low-endpoint branch data for the current reverse Liu route. -The same-degree and successor-degree branches are available through endpoint -degree three, while the two-degree-gap branch is available through endpoint -degree two. -/ -def theorem21RootCountBranchesEndpointLeThreeTwo (f g : ℝ[X]) : - Prop := - ∃ r s, - (LeftRootCountBranch f g r s ∧ - ((f.natDegree = g.natDegree ∧ g.natDegree ≤ 3) ∨ - (f.natDegree = g.natDegree + 1 ∧ g.natDegree ≤ 3) ∨ - (f.natDegree = g.natDegree + 2 ∧ g.natDegree ≤ 2))) ∨ - (RightRootCountBranch f g r s ∧ - ((g.natDegree = f.natDegree ∧ f.natDegree ≤ 3) ∨ - (g.natDegree = f.natDegree + 1 ∧ f.natDegree ≤ 3) ∨ - (g.natDegree = f.natDegree + 2 ∧ f.natDegree ≤ 2))) - -/-- Current low-endpoint nonconstant reverse route, with all degree branches -closed through endpoint degree two. -/ -theorem - theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_endpoint_le_two : - theorem21RootCountBranchesToCompatiblePredicateNonconstantStatement - (fun n => n ≤ 2) := - theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_predicate - theorem21RootCountBranchesToCompatiblePredicate_of_endpoint_le_two - -/-- Nonconstant wrapper for the endpoint-degree-two reverse route. -/ -theorem theorem21RootCountBranchesToCompatibleNonconstant_of_endpoint_le_two : - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - theorem21RootCountBranchesEndpointLeTwo f g → Compatible f g := by - intro f g hf hg hsgn hf_deg hg_deg hbranches - exact theorem21RootCountBranchesToCompatiblePredicateNonconstant_of_endpoint_le_two - hf hg hsgn hf_deg hg_deg hbranches - -/-- Nonconstant wrapper for the low-degree endpoint-degree-two reverse -implication. -/ -theorem theorem21RootCountBranchesToCompatibleNonconstant_of_natDegree_le_two - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) - (hfdeg_ne : f.natDegree ≠ 0) (hgdeg_ne : g.natDegree ≠ 0) - (hfdeg_le : f.natDegree ≤ 2) (hgdeg_le : g.natDegree ≤ 2) - (hbranches : theorem21RootCountBranches f g) : - Compatible f g := - theorem21RootCountBranchesToCompatibleNonconstant_of_endpoint_le_two - hf hg hsgn hfdeg_ne hgdeg_ne - (theorem21RootCountBranchesEndpointLeTwo_of_natDegree_le_two - hfdeg_le hgdeg_le hbranches) - -end LiuOppositeSigns -end RealRooted diff --git a/RealRooted/LiuOppositeSigns/Theorem21Statements/Interfaces.lean b/RealRooted/LiuOppositeSigns/Theorem21Statements/Interfaces.lean index c3e66ba33..82a4a17a3 100644 --- a/RealRooted/LiuOppositeSigns/Theorem21Statements/Interfaces.lean +++ b/RealRooted/LiuOppositeSigns/Theorem21Statements/Interfaces.lean @@ -2,10 +2,12 @@ import RealRooted.LiuOppositeSigns.Theorem21Statements.CommonRootDeletion import RealRooted.LiuOppositeSigns.Theorem21Statements.NoCommonCrossing /-! -# Liu opposite-sign compatibility theorem interfaces +# The published forward direction of Liu Theorem 2.1 is false -This module packages the theorem-shaped targets, corrected common-root branch, -and implication wrappers over the separate no-common and common-root engines. +The published statement of Liu Theorem 2.1 omits the common-root branch. Its +forward direction fails already for `X` and `-(X ^ 2)`. The refuted +proposition is kept here only beside its checked negation; the corrected +theorem is `compatible_iff_theorem21RootCountBranchesWithCommon_nonconstant`. -/ open Polynomial Filter @@ -13,37 +15,9 @@ open Polynomial Filter namespace RealRooted namespace LiuOppositeSigns -/-- Full unreduced target for Liu Theorem 2.1, stated against the project's -`Compatible` predicate. The two branch predicate below is the no-common -largest-root case split, so proving this full statement also requires a -common-root reduction outside the branch predicate. For the theorem shape -matching Liu's reduced proof stage, use -`theorem21CompatibleRootCountNoCommonStatement`. For an explicit tracker for -the missing common-root interface, see GitHub issue #98. - -for two real-rooted polynomials with opposite leading signs, compatibility is -equivalent to the appropriate largest-root deletion branch satisfying Liu's -closed-at-or-above root-count condition. -/ -def theorem21CompatibleRootCountStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - (Compatible f g ↔ theorem21RootCountBranches f g) - -/-- Nonconstant form of Liu Theorem 2.1. This is the induction-friendly -version of the statement because the root-count branches delete a largest root -from each polynomial. -/ -def theorem21CompatibleRootCountNonconstantStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - (Compatible f g ↔ theorem21RootCountBranches f g) - -/-- Forward half of Liu Theorem 2.1, isolated as a statement target. -/ -def theorem21CompatibleToRootCountBranchesStatement : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - Compatible f g → theorem21RootCountBranches f g - -/-- Nonconstant forward half of Liu Theorem 2.1, isolated as a statement -target. -/ +/-- Refuted: the nonconstant forward half of the published Liu Theorem 2.1, +without the common-root branch. See +`not_theorem21CompatibleToRootCountBranchesNonconstantStatement`. -/ def theorem21CompatibleToRootCountBranchesNonconstantStatement : Prop := ∀ {f g : ℝ[X]}, f.Splits → g.Splits → OppositeLeadingSigns f g → @@ -88,364 +62,5 @@ theorem not_theorem21CompatibleToRootCountBranchesNonconstantStatement : have hfalse : (0 : ℝ) < 0 := by simpa [hr, hs] using hright.largest_lt exact (lt_irrefl 0) hfalse -/-- Reverse half of Liu Theorem 2.1, isolated as a statement target. -/ -def theorem21RootCountBranchesToCompatibleStatement : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - theorem21RootCountBranches f g → Compatible f g - -/-- Nonconstant reverse half of Liu Theorem 2.1, isolated as a statement -target. -/ -def theorem21RootCountBranchesToCompatibleNonconstantStatement : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - f.natDegree ≠ 0 → g.natDegree ≠ 0 → - theorem21RootCountBranches f g → Compatible f g - -/-- No-common-root form of Liu Theorem 2.1, matching the reduced case in the -paper's proof. -/ -def theorem21CompatibleRootCountNoCommonStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - NoCommonRoots f g → (Compatible f g ↔ theorem21RootCountBranches f g) - -/-- Nonconstant no-common-root form of Liu Theorem 2.1. -/ -def theorem21CompatibleRootCountNoCommonNonconstantStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - NoCommonRoots f g → f.natDegree ≠ 0 → g.natDegree ≠ 0 → - (Compatible f g ↔ theorem21RootCountBranches f g) - -/-- Forward half of the no-common-root form of Liu Theorem 2.1. -/ -def theorem21CompatibleToRootCountBranchesNoCommonStatement : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - NoCommonRoots f g → Compatible f g → theorem21RootCountBranches f g - -/-- Nonconstant forward half of the no-common-root form of Liu Theorem 2.1. -/ -def theorem21CompatibleToRootCountBranchesNoCommonNonconstantStatement : - Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - NoCommonRoots f g → f.natDegree ≠ 0 → g.natDegree ≠ 0 → - Compatible f g → theorem21RootCountBranches f g - -/-- Reverse half of the no-common-root form of Liu Theorem 2.1. -/ -def theorem21RootCountBranchesToCompatibleNoCommonStatement : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - NoCommonRoots f g → theorem21RootCountBranches f g → Compatible f g - -/-- Nonconstant reverse half of the no-common-root form of Liu Theorem 2.1. -/ -def theorem21RootCountBranchesToCompatibleNoCommonNonconstantStatement : - Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - NoCommonRoots f g → f.natDegree ≠ 0 → g.natDegree ≠ 0 → - theorem21RootCountBranches f g → Compatible f g - -/-- Reduced common-root Liu target. The ordinary branch keeps the -no-common-root witness needed by no-common reverse theorems. -/ -def theorem21CompatibleRootCountReducedStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - (Compatible f g ↔ theorem21RootCountBranchesReduced f g) - -/-- Forward half of the reduced common-root target. -/ -def theorem21CompatibleToRootCountBranchesReducedStatement : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - Compatible f g → theorem21RootCountBranchesReduced f g - -/-- Reverse half of the reduced common-root target. -/ -def theorem21RootCountBranchesReducedToCompatibleStatement : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - theorem21RootCountBranchesReduced f g → Compatible f g - -/-- Unreduced theorem target with an explicit common-root branch. This is the -safe full-statement interface; the older `theorem21CompatibleRootCountStatement` -remains the branch-only target used by existing conditional wrappers. -/ -def theorem21CompatibleRootCountWithCommonStatement : Prop := - ∀ f g : ℝ[X], f.Splits → g.Splits → OppositeLeadingSigns f g → - (Compatible f g ↔ theorem21RootCountBranchesWithCommon f g) - -/-- Forward half of the corrected common-root-branch target. -/ -def theorem21CompatibleToRootCountBranchesWithCommonStatement : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - Compatible f g → theorem21RootCountBranchesWithCommon f g - -/-- Reverse half of the corrected common-root-branch target. -/ -def theorem21RootCountBranchesWithCommonToCompatibleStatement : Prop := - ∀ {f g : ℝ[X]}, - f.Splits → g.Splits → OppositeLeadingSigns f g → - theorem21RootCountBranchesWithCommon f g → Compatible f g - -/-- Projection form of the nonconstant Liu Theorem 2.1 statement. -/ -theorem compatible_iff_theorem21RootCountBranches_nonconstant - (h : theorem21CompatibleRootCountNonconstantStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) : - Compatible f g ↔ theorem21RootCountBranches f g := - h f g hf hg hsgn hf_deg hg_deg - -/-- Projection form of the no-common-root Liu Theorem 2.1 statement. -/ -theorem compatible_iff_theorem21RootCountBranches_noCommon - (h : theorem21CompatibleRootCountNoCommonStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hno : NoCommonRoots f g) : - Compatible f g ↔ theorem21RootCountBranches f g := - h f g hf hg hsgn hno - -/-- Forward half extracted from the paper-shaped Liu Theorem 2.1 statement. -/ -theorem theorem21CompatibleToRootCountBranches_of_theorem21CompatibleRootCount - (h : theorem21CompatibleRootCountStatement) : - theorem21CompatibleToRootCountBranchesStatement := by - intro f g hf hg hsgn - exact (h f g hf hg hsgn).1 - -/-- Reverse half extracted from the paper-shaped Liu Theorem 2.1 statement. -/ -theorem theorem21RootCountBranchesToCompatible_of_theorem21CompatibleRootCount - (h : theorem21CompatibleRootCountStatement) : - theorem21RootCountBranchesToCompatibleStatement := by - intro f g hf hg hsgn - exact (h f g hf hg hsgn).2 - -/-- Reverse half extracted from the nonconstant Liu Theorem 2.1 statement. -/ -theorem theorem21RootCountBranchesToCompatibleNonconstant_of_theorem21CompatibleRootCount - (h : theorem21CompatibleRootCountNonconstantStatement) : - theorem21RootCountBranchesToCompatibleNonconstantStatement := by - intro f g hf hg hsgn hf_deg hg_deg - exact (h f g hf hg hsgn hf_deg hg_deg).2 - -/-- The ordinary reverse half implies the no-common-root reverse half. -/ -theorem theorem21RootCountBranchesToCompatibleNoCommon_of_reverse - (hreverse : theorem21RootCountBranchesToCompatibleStatement) : - theorem21RootCountBranchesToCompatibleNoCommonStatement := by - intro f g hf hg hsgn _hno hbranches - exact hreverse hf hg hsgn hbranches - -/-- Projection form of the isolated forward direction of Liu Theorem 2.1. -/ -theorem theorem21RootCountBranches_of_compatible_of_forward - (hforward : theorem21CompatibleToRootCountBranchesStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : - theorem21RootCountBranches f g := - hforward hf hg hsgn hcompat - -/-- Projection form of the isolated no-common-root forward direction of -Liu Theorem 2.1. -/ -theorem theorem21RootCountBranches_of_compatible_of_forward_noCommon - (hforward : theorem21CompatibleToRootCountBranchesNoCommonStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hno : NoCommonRoots f g) - (hcompat : Compatible f g) : - theorem21RootCountBranches f g := - hforward hf hg hsgn hno hcompat - -/-- Projection form of the isolated nonconstant no-common-root forward -direction of Liu Theorem 2.1. -/ -theorem theorem21RootCountBranches_of_compatible_of_forward_noCommon_nonconstant - (hforward : - theorem21CompatibleToRootCountBranchesNoCommonNonconstantStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hno : NoCommonRoots f g) - (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) - (hcompat : Compatible f g) : - theorem21RootCountBranches f g := - hforward hf hg hsgn hno hf_deg hg_deg hcompat - -/-- Forward direction of Liu Theorem 2.1 as a reusable projection. -/ -theorem theorem21RootCountBranches_of_compatible - (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hcompat : Compatible f g) : - theorem21RootCountBranches f g := - theorem21RootCountBranches_of_compatible_of_forward - (theorem21CompatibleToRootCountBranches_of_theorem21CompatibleRootCount h) - hf hg hsgn hcompat - -/-- The no-common-root forward direction plus common-root deletion gives the -reduced common-root branch predicate. -/ -theorem theorem21RootCountBranchesReduced_of_compatible_of_noCommonForward - (hforward : theorem21CompatibleToRootCountBranchesNoCommonStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : - theorem21RootCountBranchesReduced f g := by - by_cases hno : NoCommonRoots f g - · exact Or.inl ⟨hno, hforward hf hg hsgn hno hcompat⟩ - · exact Or.inr - (CommonRootDeletionCompatibleBranch.of_compatible_of_not_noCommonRoots - hcompat hno) - -/-- The corrected reduced forward direction follows from the no-common forward -direction and the automatic common-root deletion branch. -/ -theorem theorem21CompatibleToRootCountBranchesReduced_of_noCommonForward - (hforward : theorem21CompatibleToRootCountBranchesNoCommonStatement) : - theorem21CompatibleToRootCountBranchesReducedStatement := by - intro f g hf hg hsgn hcompat - exact theorem21RootCountBranchesReduced_of_compatible_of_noCommonForward - hforward hf hg hsgn hcompat - -/-- The reduced common-root branch predicate forgets to the existing -with-common branch predicate. -/ -theorem theorem21CompatibleToRootCountBranchesWithCommon_of_reduced - (hreduced : theorem21CompatibleToRootCountBranchesReducedStatement) : - theorem21CompatibleToRootCountBranchesWithCommonStatement := by - intro f g hf hg hsgn hcompat - exact theorem21RootCountBranchesReduced.withCommon - (hreduced hf hg hsgn hcompat) - -/-- No-common-root reverse direction plus factor multiplication proves the -reduced common-root-branch reverse direction. -/ -theorem theorem21RootCountBranchesReducedToCompatible_of_noCommonReverse - (hreverse : theorem21RootCountBranchesToCompatibleNoCommonStatement) : - theorem21RootCountBranchesReducedToCompatibleStatement := by - intro f g hf hg hsgn hbranches - rcases hbranches with hbranches | hcommon - · exact hreverse hf hg hsgn hbranches.1 hbranches.2 - · exact CommonRootDeletionCompatibleBranch.compatible hcommon - -/-- Reassemble the reduced common-root Liu target from separately proved -reduced forward and reverse directions. -/ -theorem theorem21CompatibleRootCountReduced_of_forward_and_reverse - (hforward : theorem21CompatibleToRootCountBranchesReducedStatement) - (hreverse : theorem21RootCountBranchesReducedToCompatibleStatement) : - theorem21CompatibleRootCountReducedStatement := by - intro f g hf hg hsgn - exact ⟨hforward hf hg hsgn, hreverse hf hg hsgn⟩ - -/-- Reassemble the reduced common-root Liu target from the no-common forward -and no-common reverse directions. -/ -theorem theorem21CompatibleRootCountReduced_of_noCommon_forward_and_reverse - (hforward : theorem21CompatibleToRootCountBranchesNoCommonStatement) - (hreverse : theorem21RootCountBranchesToCompatibleNoCommonStatement) : - theorem21CompatibleRootCountReducedStatement := - theorem21CompatibleRootCountReduced_of_forward_and_reverse - (theorem21CompatibleToRootCountBranchesReduced_of_noCommonForward - hforward) - (theorem21RootCountBranchesReducedToCompatible_of_noCommonReverse - hreverse) - -/-- The corrected full forward direction follows from the no-common forward -direction and the automatic common-root deletion branch. -/ -theorem theorem21CompatibleToRootCountBranchesWithCommon_of_noCommonForward - (hforward : theorem21CompatibleToRootCountBranchesNoCommonStatement) : - theorem21CompatibleToRootCountBranchesWithCommonStatement := - theorem21CompatibleToRootCountBranchesWithCommon_of_reduced - (theorem21CompatibleToRootCountBranchesReduced_of_noCommonForward hforward) - -/-- Branch-only reverse direction plus factor multiplication proves the -corrected common-root-branch reverse direction. -/ -theorem theorem21RootCountBranchesWithCommonToCompatible_of_reverse - (hreverse : theorem21RootCountBranchesToCompatibleStatement) : - theorem21RootCountBranchesWithCommonToCompatibleStatement := by - intro f g hf hg hsgn hbranches - rcases hbranches with hbranches | hcommon - · exact hreverse hf hg hsgn hbranches - · exact CommonRootDeletionCompatibleBranch.compatible hcommon - -/-- Reassemble the corrected common-root-branch Liu target from the -no-common-root forward direction and the branch-only reverse direction. -/ -theorem theorem21CompatibleRootCountWithCommon_of_noCommonForward_and_reverse - (hforward : theorem21CompatibleToRootCountBranchesNoCommonStatement) - (hreverse : theorem21RootCountBranchesToCompatibleStatement) : - theorem21CompatibleRootCountWithCommonStatement := by - intro f g hf hg hsgn - constructor - · exact - theorem21CompatibleToRootCountBranchesWithCommon_of_noCommonForward - hforward hf hg hsgn - · exact - theorem21RootCountBranchesWithCommonToCompatible_of_reverse - hreverse hf hg hsgn - -/-- Projection form of the isolated reverse direction of Liu Theorem 2.1. -/ -theorem compatible_of_theorem21RootCountBranches_of_reverse - (hreverse : theorem21RootCountBranchesToCompatibleStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) - (hbranches : theorem21RootCountBranches f g) : - Compatible f g := - hreverse hf hg hsgn hbranches - -/-- Projection form of the isolated nonconstant reverse direction of -Liu Theorem 2.1. -/ -theorem compatible_of_theorem21RootCountBranches_of_reverse_nonconstant - (hreverse : theorem21RootCountBranchesToCompatibleNonconstantStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) - (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) - (hbranches : theorem21RootCountBranches f g) : - Compatible f g := - hreverse hf hg hsgn hf_deg hg_deg hbranches - -/-- Reverse direction of Liu Theorem 2.1 as a reusable projection. -/ -theorem compatible_of_theorem21RootCountBranches - (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hbranches : theorem21RootCountBranches f g) : - Compatible f g := - compatible_of_theorem21RootCountBranches_of_reverse - (theorem21RootCountBranchesToCompatible_of_theorem21CompatibleRootCount h) - hf hg hsgn hbranches - -/-- Reverse direction of the nonconstant Liu Theorem 2.1 statement. -/ -theorem compatible_of_theorem21RootCountBranches_nonconstant - (h : theorem21CompatibleRootCountNonconstantStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) - (hbranches : theorem21RootCountBranches f g) : - Compatible f g := - compatible_of_theorem21RootCountBranches_of_reverse_nonconstant - (theorem21RootCountBranchesToCompatibleNonconstant_of_theorem21CompatibleRootCount - h) - hf hg hsgn hf_deg hg_deg hbranches - -/-- Isolated forward direction with the branch predicate swapped. -/ -theorem theorem21RootCountBranches_symm_of_compatible_of_forward - (hforward : theorem21CompatibleToRootCountBranchesStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) : - theorem21RootCountBranches g f := - theorem21RootCountBranches_of_compatible_of_forward hforward - hg hf hsgn.symm hcompat.comm - -/-- Forward direction of Liu Theorem 2.1 with the branch predicate swapped. -/ -theorem theorem21RootCountBranches_symm_of_compatible - (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hcompat : Compatible f g) : - theorem21RootCountBranches g f := - theorem21RootCountBranches_symm_of_compatible_of_forward - (theorem21CompatibleToRootCountBranches_of_theorem21CompatibleRootCount h) - hf hg hsgn hcompat - -/-- Isolated reverse direction with the branch predicate swapped. -/ -theorem compatible_of_theorem21RootCountBranches_symm_of_reverse - (hreverse : theorem21RootCountBranchesToCompatibleStatement) - {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits) - (hsgn : OppositeLeadingSigns f g) - (hbranches : theorem21RootCountBranches g f) : - Compatible f g := - (compatible_of_theorem21RootCountBranches_of_reverse hreverse - hg hf hsgn.symm hbranches).comm - -/-- Reverse direction of Liu Theorem 2.1 with the branch predicate swapped. -/ -theorem compatible_of_theorem21RootCountBranches_symm - (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) - (hbranches : theorem21RootCountBranches g f) : - Compatible f g := - compatible_of_theorem21RootCountBranches_symm_of_reverse - (theorem21RootCountBranchesToCompatible_of_theorem21CompatibleRootCount h) - hf hg hsgn hbranches - -/-- Projection form of Liu Theorem 2.1 after swapping the two polynomials. -/ -theorem compatible_iff_theorem21RootCountBranches_symm - (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]} - (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) : - Compatible f g ↔ theorem21RootCountBranches g f := - ⟨theorem21RootCountBranches_symm_of_compatible h hf hg hsgn, - compatible_of_theorem21RootCountBranches_symm h hf hg hsgn⟩ - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/XSub/CubicCubic/Endpoints.lean b/RealRooted/LiuOppositeSigns/XSub/CubicCubic/Endpoints.lean index 27c8ce6f0..e1fb87718 100644 --- a/RealRooted/LiuOppositeSigns/XSub/CubicCubic/Endpoints.lean +++ b/RealRooted/LiuOppositeSigns/XSub/CubicCubic/Endpoints.lean @@ -158,27 +158,5 @@ theorem positiveSplitSameDegreeTranslatedXSubRightFamily_of_right_natDegree_le_t positiveSplitSameDegreeTranslatedXSubRightFamily_of_right_natDegree_le_three_of_monic xSubCubicCubicSplits hpair hfnn hgnn hdeg hgdeg -/-- Pack the endpoint cases through degree three as a predicate-restricted -same-degree sign-normalized x-subtraction target, modulo the normalized monic -cubic/cubic arithmetic leaf. -/ -theorem - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_three_of_monic - (hmono : xSubCubicCubicSplitsStatement) : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n ≤ 3) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact - positiveSplitSameDegreeTranslatedXSubRightFamily_of_right_natDegree_le_three_of_monic - hmono hpair hfnn hgnn hdeg hgdeg - -/-- Pack the endpoint cases through degree three as a predicate-restricted -same-degree sign-normalized x-subtraction target. -/ -theorem - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_three : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n ≤ 3) := - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_three_of_monic - xSubCubicCubicSplits - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/LeftSuccessor.lean b/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/LeftSuccessor.lean index c5c15751c..a5d0d9a50 100644 --- a/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/LeftSuccessor.lean +++ b/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/LeftSuccessor.lean @@ -239,9 +239,12 @@ theorem PositiveSplitRootCountPair.xSub_splits_of_left_successor_nonneg /-- Unrestricted positive-split left-successor translated x-subtraction family. -/ -theorem positiveSplitLeftSuccDegreeTranslatedXSubRightFamily : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement := by - intro f g r hpair hfnn hgnn hdeg μ hμ +theorem positiveSplitLeftSuccDegreeTranslatedXSubRightFamily {f g : ℝ[X]} (r : ℝ) + (hpair : PositiveSplitRootCountPair f g) + (hfnn : HasNonnegCoeffs (f.comp (X + C r))) + (hgnn : HasNonnegCoeffs (g.comp (X + C r))) + (hdeg : f.natDegree = g.natDegree + 1) (μ : ℝ) (hμ : 0 < μ) : + (X * f.comp (X + C r) - C μ * g.comp (X + C r)).Splits := by let p := f.comp (X + C r) let q := g.comp (X + C r) have hpair_shift : PositiveSplitRootCountPair p q := by simpa [p, q] using hpair.comp_X_add_C r @@ -251,15 +254,5 @@ theorem positiveSplitLeftSuccDegreeTranslatedXSubRightFamily : hpair_shift.xSub_splits_of_left_successor_nonneg hfnn hgnn hdeg_shift hμ -/-- The proved left-successor x-subtraction family gives every predicate -restriction. -/ -theorem positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate - {P : ℕ → Prop} : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement P := - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement_of_imp - (fun _ _ => trivial) - (positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_true_of_xSub - positiveSplitLeftSuccDegreeTranslatedXSubRightFamily) - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/RightSuccessor.lean b/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/RightSuccessor.lean index eebdfa5c7..ab49d3343 100644 --- a/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/RightSuccessor.lean +++ b/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/RightSuccessor.lean @@ -377,9 +377,12 @@ theorem PositiveSplitRootCountPair.xSub_splits_of_right_successor_nonneg /-- Unrestricted positive-split right-successor translated x-subtraction family. -/ -theorem positiveSplitRightSuccDegreeTranslatedXSubRightFamily : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement := by - intro f g r hpair hfnn hgnn hdeg μ hμ +theorem positiveSplitRightSuccDegreeTranslatedXSubRightFamily {f g : ℝ[X]} (r : ℝ) + (hpair : PositiveSplitRootCountPair f g) + (hfnn : HasNonnegCoeffs (f.comp (X + C r))) + (hgnn : HasNonnegCoeffs (g.comp (X + C r))) + (hdeg : g.natDegree = f.natDegree + 1) (μ : ℝ) (hμ : 0 < μ) : + (X * f.comp (X + C r) - C μ * g.comp (X + C r)).Splits := by let p := f.comp (X + C r) let q := g.comp (X + C r) have hpair_shift : PositiveSplitRootCountPair p q := by simpa [p, q] using hpair.comp_X_add_C r @@ -389,15 +392,5 @@ theorem positiveSplitRightSuccDegreeTranslatedXSubRightFamily : hpair_shift.xSub_splits_of_right_successor_nonneg hfnn hgnn hdeg_shift hμ -/-- The proved right-successor x-subtraction family gives every predicate -restriction. -/ -theorem positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate - {P : ℕ → Prop} : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement P := - positiveSplitTranslatedXSubRightFamilyPredicateRelationStatement_of_imp - (fun _ _ => trivial) - (positiveSplitTranslatedXSubRightFamilyPredicateRelation_true_of_relation - positiveSplitRightSuccDegreeTranslatedXSubRightFamily) - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/SameDegree.lean b/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/SameDegree.lean index 5ad1ad843..6daaccf37 100644 --- a/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/SameDegree.lean +++ b/RealRooted/LiuOppositeSigns/XSub/IntervalRootCount/SameDegree.lean @@ -221,9 +221,12 @@ theorem PositiveSplitRootCountPair.xSub_splits_of_same_degree_nonneg exact hmain q.natDegree rfl hpair hp_nonneg hq_nonneg hdeg μ hμ /-- Same-degree translated x-subtraction family. -/ -theorem positiveSplitSameDegreeTranslatedXSubRightFamily : - positiveSplitSameDegreeTranslatedXSubRightFamilyStatement := by - intro f g r hpair hfnn hgnn hdeg μ hμ +theorem positiveSplitSameDegreeTranslatedXSubRightFamily {f g : ℝ[X]} (r : ℝ) + (hpair : PositiveSplitRootCountPair f g) + (hfnn : HasNonnegCoeffs (f.comp (X + C r))) + (hgnn : HasNonnegCoeffs (g.comp (X + C r))) + (hdeg : f.natDegree = g.natDegree) (μ : ℝ) (hμ : 0 < μ) : + (X * f.comp (X + C r) - C μ * g.comp (X + C r)).Splits := by let p := f.comp (X + C r) let q := g.comp (X + C r) have hpair_shift : PositiveSplitRootCountPair p q := by simpa [p, q] using hpair.comp_X_add_C r @@ -232,15 +235,5 @@ theorem positiveSplitSameDegreeTranslatedXSubRightFamily : simpa [p, q] using hpair_shift.xSub_splits_of_same_degree_nonneg hfnn hgnn hdeg_shift hμ -/-- Same-degree translated x-subtraction family packaged with an arbitrary -right-degree predicate. -/ -theorem positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate - (P : ℕ → Prop) : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement P := - positiveSplitTranslatedXSubRightFamilyPredicateRelationStatement_of_imp - (fun _ _ => trivial) - (positiveSplitTranslatedXSubRightFamilyPredicateRelation_true_of_relation - positiveSplitSameDegreeTranslatedXSubRightFamily) - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/XSub/LeftSucc.lean b/RealRooted/LiuOppositeSigns/XSub/LeftSucc.lean index e179eb128..ed7565cfc 100644 --- a/RealRooted/LiuOppositeSigns/XSub/LeftSucc.lean +++ b/RealRooted/LiuOppositeSigns/XSub/LeftSucc.lean @@ -6,9 +6,9 @@ import RealRooted.SameDegreeQuadraticRootCount /-! # Liu left-successor x-subtraction base cases -This module contains the left-successor positive-split x-subtraction target -interface and the degree-zero right-endpoint terminal used by the two-degree -factor-return branch. +This module contains low-degree right-endpoint cases of the left-successor +positive-split x-subtraction pencil used by the two-degree factor-return +branch. -/ open Polynomial Filter @@ -16,65 +16,6 @@ open Polynomial Filter namespace RealRooted namespace LiuOppositeSigns -/-- Positive-split left-successor subtraction-family target. After a shift -that makes the two endpoints coefficientwise nonnegative, the one-sided pencil -`X * f - μ g`, `μ > 0`, should be real-rooted. This is the honest -two-degree Liu factor-return leaf left after the false all-combinations route -is removed. -/ -def positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement : Prop := - ∀ ⦃f g : ℝ[X]⦄ (r : ℝ), - PositiveSplitRootCountPair f g → - HasNonnegCoeffs (f.comp (X + C r)) → - HasNonnegCoeffs (g.comp (X + C r)) → - f.natDegree = g.natDegree + 1 → - ∀ μ : ℝ, 0 < μ → - (X * f.comp (X + C r) - C μ * g.comp (X + C r)).Splits - -/-- Predicate-restricted form of the positive-split left-successor -subtraction-family target. The predicate records endpoint restrictions on -`g.natDegree`. -/ -def positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (P : ℕ → Prop) : Prop := - ∀ ⦃f g : ℝ[X]⦄ (r : ℝ), - PositiveSplitRootCountPair f g → - HasNonnegCoeffs (f.comp (X + C r)) → - HasNonnegCoeffs (g.comp (X + C r)) → - f.natDegree = g.natDegree + 1 → - P g.natDegree → - ∀ μ : ℝ, 0 < μ → - (X * f.comp (X + C r) - C μ * g.comp (X + C r)).Splits - -/-- Predicate-restricted positive-split x-subtraction targets transport along -endpoint predicate implications. -/ -theorem positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement_of_imp - {P Q : ℕ → Prop} (hPQ : ∀ n, P n → Q n) - (hQ : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - Q) : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - P := by - intro f g r hpair hfnn hgnn hdeg hgdeg μ hμ - exact hQ r hpair hfnn hgnn hdeg (hPQ _ hgdeg) μ hμ - -/-- The unrestricted positive-split x-sub family is the `P := True` case of -the predicate-restricted target. -/ -theorem positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_true_of_xSub - (hsub : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement) : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun _ => True) := by - intro f g r hpair hfnn hgnn hdeg _ μ hμ - exact hsub r hpair hfnn hgnn hdeg μ hμ - -/-- A `P := True` positive-split x-sub family gives the unrestricted target. -/ -theorem positiveSplitLeftSuccDegreeTranslatedXSubRightFamily_of_predicate_true - (hsub : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun _ => True)) : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyStatement := by - intro f g r hpair hfnn hgnn hdeg μ hμ - exact hsub r hpair hfnn hgnn hdeg trivial μ hμ - /-- Quadratic terminal case for the x-subtraction pencil: a degree-one positive-leading left endpoint and degree-zero positive-leading right endpoint give a splitting polynomial `X * p - μ q` for every `μ > 0`. -/ diff --git a/RealRooted/LiuOppositeSigns/XSub/LeftSuccDegreeThree.lean b/RealRooted/LiuOppositeSigns/XSub/LeftSuccDegreeThree.lean index ef346455b..ff1bc0884 100644 --- a/RealRooted/LiuOppositeSigns/XSub/LeftSuccDegreeThree.lean +++ b/RealRooted/LiuOppositeSigns/XSub/LeftSuccDegreeThree.lean @@ -153,48 +153,5 @@ theorem positiveSplitLeftSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_ positiveSplitLeftSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_le_three_of_monic xSubQuarticCubicSplits hpair hfnn hgnn hdeg hgdeg -/-- Pack the degree-three-right endpoint terminal as a predicate-restricted -positive-split x-sub family, modulo the normalized monic quartic/cubic -arithmetic leaf. -/ -theorem - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_three_of_monic - (hmono : xSubQuarticCubicSplitsStatement) : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n = 3) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact - positiveSplitLeftSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_three_of_monic - hmono hpair hfnn hgnn hdeg hgdeg - -/-- Pack the degree-three-right endpoint terminal as a predicate-restricted -positive-split x-sub family. -/ -theorem - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_three : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n = 3) := - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_three_of_monic - xSubQuarticCubicSplits - -/-- Pack endpoint cases through degree three as a predicate-restricted -positive-split x-sub family, modulo the normalized monic quartic/cubic -arithmetic leaf. -/ -theorem - positiveSplitLeftSuccXSubFamilyPredicate_of_right_natDegree_le_three_of_monic - (hmono : xSubQuarticCubicSplitsStatement) : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n ≤ 3) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact - positiveSplitLeftSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_le_three_of_monic - hmono hpair hfnn hgnn hdeg hgdeg - -/-- Pack endpoint cases through degree three as a predicate-restricted -positive-split x-sub family. -/ -theorem positiveSplitLeftSuccXSubFamilyPredicate_of_right_natDegree_le_three : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n ≤ 3) := - positiveSplitLeftSuccXSubFamilyPredicate_of_right_natDegree_le_three_of_monic - xSubQuarticCubicSplits - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/XSub/LeftSuccDegreeTwo.lean b/RealRooted/LiuOppositeSigns/XSub/LeftSuccDegreeTwo.lean index da40820e6..cd3d5e3f8 100644 --- a/RealRooted/LiuOppositeSigns/XSub/LeftSuccDegreeTwo.lean +++ b/RealRooted/LiuOppositeSigns/XSub/LeftSuccDegreeTwo.lean @@ -148,70 +148,5 @@ theorem positiveSplitLeftSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_ exact positiveSplitLeftSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_two hpair hfnn hgnn hdeg htwo -/-- Pack the low-degree-right endpoint terminal as a predicate-restricted -positive-split x-sub family. -/ -theorem - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_one : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n ≤ 1) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact positiveSplitLeftSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_le_one - hpair hfnn hgnn hdeg hgdeg - -/-- Pack the constant-right endpoint terminal as a predicate-restricted -positive-split x-sub family. -/ -theorem - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_zero : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n = 0) := by - refine positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement_of_imp - (Q := fun n => n ≤ 1) ?_ - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_one - intro n hn - simp [hn] - -/-- Pack the degree-one-right endpoint terminal as a predicate-restricted -positive-split x-sub family. -/ -theorem - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_one : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n = 1) := by - refine positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement_of_imp - (Q := fun n => n ≤ 1) ?_ - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_one - intro n hn - simp [hn] - -/-- Pack the degree-two-right endpoint terminal as a predicate-restricted -positive-split x-sub family, modulo the normalized monic arithmetic leaf. -/ -theorem - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_two_of_monic - (hmono : xSubCubicQuadraticSplitsStatement) : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n = 2) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact - positiveSplitLeftSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_two_of_monic - hmono hpair hfnn hgnn hdeg hgdeg - -/-- Pack the degree-two-right endpoint terminal as a predicate-restricted -positive-split x-sub family. -/ -theorem - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_two : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n = 2) := - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_two_of_monic - xSubCubicQuadraticSplits - -/-- Pack the endpoint cases through degree two as a predicate-restricted -positive-split x-sub family. -/ -theorem - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_two : - positiveSplitLeftSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n ≤ 2) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact positiveSplitLeftSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_le_two - hpair hfnn hgnn hdeg hgdeg - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/XSub/LinearQuadratic.lean b/RealRooted/LiuOppositeSigns/XSub/LinearQuadratic.lean index 8d48d598d..0fc8bf80c 100644 --- a/RealRooted/LiuOppositeSigns/XSub/LinearQuadratic.lean +++ b/RealRooted/LiuOppositeSigns/XSub/LinearQuadratic.lean @@ -263,15 +263,5 @@ theorem positiveSplitRightSuccDegreeTranslatedXSubRightFamily_of_right_natDegree exact positiveSplitRightSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_two hpair hfnn hgnn hdeg htwo -/-- Pack the endpoint cases through degree two as a predicate-restricted -right-successor positive-split x-sub family. -/ -theorem - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_two : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n ≤ 2) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact positiveSplitRightSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_le_two - hpair hfnn hgnn hdeg hgdeg - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/XSub/QuadraticCubic.lean b/RealRooted/LiuOppositeSigns/XSub/QuadraticCubic.lean index d41c3a15c..c9c8e0743 100644 --- a/RealRooted/LiuOppositeSigns/XSub/QuadraticCubic.lean +++ b/RealRooted/LiuOppositeSigns/XSub/QuadraticCubic.lean @@ -1442,27 +1442,5 @@ theorem positiveSplitRightSuccDegreeTranslatedXSubRightFamily_of_right_natDegree positiveSplitRightSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_le_three_of_monic xSubQuadraticCubicSplits hpair hfnn hgnn hdeg hgdeg -/-- Pack the endpoint cases through degree three as a predicate-restricted -right-successor positive-split x-sub family. -/ -theorem - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_le_three : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n ≤ 3) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact positiveSplitRightSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_le_three - hpair hfnn hgnn hdeg hgdeg - -/-- Compatibility alias for the shorter historical degree-three predicate -name. -/ -theorem - positiveSplitRightSuccXSubFamilyPredicate_of_right_natDegree_le_three_of_monic - (hmono : xSubQuadraticCubicSplitsStatement) : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n ≤ 3) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact - positiveSplitRightSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_le_three_of_monic - hmono hpair hfnn hgnn hdeg hgdeg - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/LiuOppositeSigns/XSub/SameDegree.lean b/RealRooted/LiuOppositeSigns/XSub/SameDegree.lean index 868ea950f..2d822496a 100644 --- a/RealRooted/LiuOppositeSigns/XSub/SameDegree.lean +++ b/RealRooted/LiuOppositeSigns/XSub/SameDegree.lean @@ -4,9 +4,9 @@ import RealRooted.QuadraticRoot /-! # Liu same-degree and right-successor x-subtraction base cases -This module contains the generic positive-split translated x-subtraction -interface for the same-degree and right-successor branches, together with the -constant and linear endpoint cases. +This module contains the constant and linear endpoint cases of the +positive-split translated x-subtraction pencils for the same-degree and +right-successor branches. -/ open Polynomial Filter @@ -14,87 +14,6 @@ open Polynomial Filter namespace RealRooted namespace LiuOppositeSigns -/-- Positive-split x-subtraction target for an arbitrary endpoint degree -relation. This is the common statement shape behind the same-, right-successor, -and left-successor translated half-pencil leaves. -/ -def positiveSplitTranslatedXSubRightFamilyRelationStatement - (R : ℕ → ℕ → Prop) : Prop := - ∀ ⦃f g : ℝ[X]⦄ (r : ℝ), - PositiveSplitRootCountPair f g → - HasNonnegCoeffs (f.comp (X + C r)) → - HasNonnegCoeffs (g.comp (X + C r)) → - R f.natDegree g.natDegree → - ∀ μ : ℝ, 0 < μ → - (X * f.comp (X + C r) - C μ * g.comp (X + C r)).Splits - -/-- Predicate-restricted positive-split x-subtraction target for an arbitrary -endpoint degree relation. The predicate records endpoint restrictions on -`g.natDegree`. -/ -def positiveSplitTranslatedXSubRightFamilyPredicateRelationStatement - (R : ℕ → ℕ → Prop) (P : ℕ → Prop) : Prop := - ∀ ⦃f g : ℝ[X]⦄ (r : ℝ), - PositiveSplitRootCountPair f g → - HasNonnegCoeffs (f.comp (X + C r)) → - HasNonnegCoeffs (g.comp (X + C r)) → - R f.natDegree g.natDegree → - P g.natDegree → - ∀ μ : ℝ, 0 < μ → - (X * f.comp (X + C r) - C μ * g.comp (X + C r)).Splits - -/-- Predicate-restricted relation x-subtraction targets transport along -endpoint predicate implications. -/ -theorem positiveSplitTranslatedXSubRightFamilyPredicateRelationStatement_of_imp - {R : ℕ → ℕ → Prop} {P Q : ℕ → Prop} (hPQ : ∀ n, P n → Q n) - (hQ : - positiveSplitTranslatedXSubRightFamilyPredicateRelationStatement R Q) : - positiveSplitTranslatedXSubRightFamilyPredicateRelationStatement R P := by - intro f g r hpair hfnn hgnn hdeg hgdeg μ hμ - exact hQ r hpair hfnn hgnn hdeg (hPQ _ hgdeg) μ hμ - -/-- The unrestricted relation x-subtraction target is the `P := True` case of -the predicate-restricted target. -/ -theorem positiveSplitTranslatedXSubRightFamilyPredicateRelation_true_of_relation - {R : ℕ → ℕ → Prop} - (hsub : positiveSplitTranslatedXSubRightFamilyRelationStatement R) : - positiveSplitTranslatedXSubRightFamilyPredicateRelationStatement R - (fun _ => True) := by - intro f g r hpair hfnn hgnn hdeg _ μ hμ - exact hsub r hpair hfnn hgnn hdeg μ hμ - -/-- A `P := True` relation x-subtraction target gives the unrestricted -relation target. -/ -theorem positiveSplitTranslatedXSubRightFamilyRelation_of_predicate_true - {R : ℕ → ℕ → Prop} - (hsub : - positiveSplitTranslatedXSubRightFamilyPredicateRelationStatement R - (fun _ => True)) : - positiveSplitTranslatedXSubRightFamilyRelationStatement R := by - intro f g r hpair hfnn hgnn hdeg μ hμ - exact hsub r hpair hfnn hgnn hdeg trivial μ hμ - -/-- Same-degree positive-split subtraction-family target. -/ -def positiveSplitSameDegreeTranslatedXSubRightFamilyStatement : Prop := - positiveSplitTranslatedXSubRightFamilyRelationStatement - (fun m n => m = n) - -/-- Predicate-restricted same-degree positive-split subtraction-family target. -/ -def positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement - (P : ℕ → Prop) : Prop := - positiveSplitTranslatedXSubRightFamilyPredicateRelationStatement - (fun m n => m = n) P - -/-- Right-successor positive-split subtraction-family target. -/ -def positiveSplitRightSuccDegreeTranslatedXSubRightFamilyStatement : Prop := - positiveSplitTranslatedXSubRightFamilyRelationStatement - (fun m n => n = m + 1) - -/-- Predicate-restricted right-successor positive-split subtraction-family -target. -/ -def positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (P : ℕ → Prop) : Prop := - positiveSplitTranslatedXSubRightFamilyPredicateRelationStatement - (fun m n => n = m + 1) P - /-- Degree guardrail for the translated x-subtraction endpoint: in the left-successor case, `g.comp (X + C r)` and `X * f.comp (X + C r)` differ by two degrees, so this endpoint cannot be proved by a direct `StrictInterl` witness. -/ @@ -239,36 +158,5 @@ theorem positiveSplitRightSuccDegreeTranslatedXSubRightFamily_of_right_natDegree exact splits_X_mul_sub_C_mul_of_left_natDegree_zero_right_natDegree_le_one hFdeg hGdeg μ -/-- Pack the degree-zero right endpoint terminal as a predicate-restricted -same-degree sign-normalized x-subtraction target. -/ -theorem - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_zero : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n = 0) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact positiveSplitSameDegreeTranslatedXSubRightFamily_of_right_natDegree_zero - hpair hfnn hgnn hdeg hgdeg - -/-- Pack the degree-one right endpoint terminal as a predicate-restricted -same-degree sign-normalized x-subtraction target. -/ -theorem - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_one : - positiveSplitSameDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n = 1) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact positiveSplitSameDegreeTranslatedXSubRightFamily_of_right_natDegree_one - hpair hfnn hgnn hdeg hgdeg - -/-- Pack the degree-one right endpoint terminal as a predicate-restricted -right-successor sign-normalized x-subtraction target. -/ -theorem - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicate_of_right_natDegree_one : - positiveSplitRightSuccDegreeTranslatedXSubRightFamilyPredicateStatement - (fun n => n = 1) := by - intro f g r hpair hfnn hgnn hdeg hgdeg - exact positiveSplitRightSuccDegreeTranslatedXSubRightFamily_of_right_natDegree_one - hpair hfnn hgnn hdeg hgdeg - - end LiuOppositeSigns end RealRooted diff --git a/RealRooted/Production.lean b/RealRooted/Production.lean index da35ec8d0..b630644cf 100644 --- a/RealRooted/Production.lean +++ b/RealRooted/Production.lean @@ -538,17 +538,11 @@ import RealRooted.LinearPowerFamily import RealRooted.LiuOppositeSigns import RealRooted.LiuOppositeSigns.BoundedIntervalContinuity import RealRooted.LiuOppositeSigns.CommonInterleaverConsequences -import RealRooted.LiuOppositeSigns.Corollary22 import RealRooted.LiuOppositeSigns.DeletionBranches import RealRooted.LiuOppositeSigns.DerivativeShiftRegularization import RealRooted.LiuOppositeSigns.DerivativeShiftSequenceRegularization import RealRooted.LiuOppositeSigns.FactorReturnAssembly -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.DegreeCaseAssembly -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.LeftDegreeCases -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.PredicateDegreeCases -import RealRooted.LiuOppositeSigns.FactorReturnAssembly.RightDegreeCases import RealRooted.LiuOppositeSigns.FactorReturnLeft -import RealRooted.LiuOppositeSigns.FactorReturnStatements import RealRooted.LiuOppositeSigns.FactorReturnTwoDegree import RealRooted.LiuOppositeSigns.ForwardCubicLinear import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.Average @@ -571,7 +565,6 @@ import RealRooted.LiuOppositeSigns.RootCount import RealRooted.LiuOppositeSigns.RootCountClosure import RealRooted.LiuOppositeSigns.RootCountRelStability import RealRooted.LiuOppositeSigns.RootDeletion -import RealRooted.LiuOppositeSigns.Theorem21Assembly import RealRooted.LiuOppositeSigns.Theorem21Statements import RealRooted.LiuOppositeSigns.Theorem21Statements.CommonRootDeletion import RealRooted.LiuOppositeSigns.Theorem21Statements.Interfaces