Prove Liu cross-owned gaps by bounded continuity

[PerAlexandersson]

Summary

• add fixed-degree reflection helpers for inverse roots and positive half-line root counts;
• prove affine-pencil root-count constancy on bounded intervals even when natDegree drops;
• prove Liu's CrossOwnedNotOddGaps input by following the direct or reciprocal pencil from the root-free endpoint polynomial;
• avoid the equal-degree cancellation-parameter inequalities that are not part of Liu's source proof.

Source route

This follows Liu, Polynomials with real zeros and compatible sequences, Theorem 2.1: parity supplies a positive crossing in a bounded merged-root gap, while continuity preserves the number of roots when the gap endpoints remain root-free. Fixed-degree reflection handles a root escaping to infinity at leading-term cancellation.

Validation

• Axle checked the reflection endpoint identity, translation adapters, degree-bound plumbing, and assembled bounded-interval proof in isolated Lean 4.31.0 harnesses.
• A read-only independent audit found the odd-gap argument sound with no missing hypotheses.
• Comparator CI is authoritative for the rebased branch and is pending.

[PerAlexandersson]

Continuation 113 pushes e90d393d, repairing the next independent failure from the last completed Lean Action run.

RootOrderBridge.lean timed out at the context-sensitive simp_all proving the successor-length reverse-index helper inside count_le_two_of_succRootCrossing; the second theorem-level timeout was cascading. The helper now performs an explicit getD/reverse calculation with two local lia index facts.

Axle 4.31 accepted the isolated exact helper (request 097c7814-e840-480c-8dc1-15ef60e0cb6c). No local Lake build was run. Nearby linter-only unused simp arguments are reserved for continuation 114's required cleanup pass.

[PerAlexandersson]

Mandatory cleanup continuation 114 pushes 2f263fc1.

The two successor-degree sorted-list length facts in count_le_two_of_succRootCrossing now use direct simpa [sM] using hM / simpa [sN] using hN proofs. This removes eight lines of duplicated context-wide subst/simp_all plumbing and all six archived unused-simp warnings there, without changing theorem statements or mathematics.

Axle 4.31 checked the exact isolated pair without warnings (request 27ebbc09-c642-4be2-9414-5ff59a6a9627). No local Lake build was run. Continuation 115 returns to proof/CI repair.

[PerAlexandersson]

Continuation 115 pushes b8f32466, repairing the archived DerivativeShiftSequence.lean unknown-name cascade.

TDeriv, HasSimpleRoots, and the associated derivative-shift lemmas are imported correctly but declared in namespace RealRooted; this file entered namespace Polynomial without opening RealRooted. Adding open RealRooted preserves the intended Polynomial.applyTDerivList API while making all imported names visible. No theorem body or mathematics changed.

Three obsolete comparator runs for prior heads were canceled; the current-head workflow was not touched. No local Lake build was run, so the restarted GitHub build remains authoritative.

[PerAlexandersson]

Continuation 116 pushes 7da47c41, repairing the archived DerivativeShiftRootMatching.lean failures.

A local equality now explicitly identifies the root-continuity family p + C nu * (-p.derivative) with TDeriv nu p. Splitting, natural-degree, and root-count transport use that equality instead of relying on simp to normalize subtraction and multiplication by a negated polynomial. The final Multiset.Rel.mono callback now also accepts Mathlib's source/target membership arguments.

Axle 4.31 checked both exact shapes (request c39ba2b5-12ed-48d3-8990-d7fccae724ba). No local Lake build was run. Continuation 117 is the mandatory cleanup cycle.

[PerAlexandersson]

Mandatory cleanup continuation 117 pushes 0a49c235.

The two list inductions in DerivativeShiftSequence.lean duplicated three-line tail-positivity proofs using intro and simp. Both now use the direct membership weakening List.mem_cons_of_mem, deleting four lines and removing tactic automation without changing statements, induction structure, or mathematics.

Axle 4.31 accepted the exact standalone function without warnings (request 40437d12-de7f-4106-9c6a-147ede341443). No local Lake build was run. Continuation 118 returns to proof/CI repair.

[PerAlexandersson]

Comparator run 30794802855 exposed four merge-build failures. The first dependency repair is pushed in b0536886: Rel.comp now preserves the actual tail relations after destructuring, and rel_uncross_min_cons handles the current cons_eq_cons unequal-head branch explicitly. Axle request ab966cc5-6a9e-46f8-9385-1276928bc0df checked both full proofs. The next comparator run will determine which downstream RootOrderBridge/DerivativeShiftSequence/Obreschkoff errors remain independently.

[PerAlexandersson]

Mandatory cleanup pass pushed in 98082647. The repaired Rel.comp induction now discharges the two multiset equalities directly with rfl patterns, removing two temporary names and two subst commands while retaining distinct tail-hypothesis names. This preserves the shadowing fix and adds no API. Axle request: ec73d1d0-3bf5-4d81-9f8a-11d185093b27.

[PerAlexandersson]

Comparator repair 198878a is pushed.

• Gives Multiset.strongInductionOn its explicit dependent motive.
• Replaces the timed-out successor reverse-index grind with the exact substitution j = d - 1 - i.
• Transports derivative-shift multiplicity explicitly across the induction equality.
• Moves the compatibility-dependent constant-endpoint and Corollary 2.2 block out of upstream ObreschkoffConverse and into LiuOppositeSignsTheorem, avoiding the existing Compatibility.Basic -> AffineFamily -> ObreschkoffConverse import cycle.

Axle requests 7364289a-dc6a-46c7-93e8-7aa1057017f9 and 159c0982-d4d3-4176-ac9a-f0b954045913 checked the isolated eliminator and full index conversion. No local Lake build was run; the restarted comparator is authoritative.

[PerAlexandersson]

Scheduled cleanup continuation 145 repairs all three independent compile failures from comparator run 30798983908 in commit bcb80a8: dependent strongInductionOn now uses apply rather than refine, the derivative-shift triangle inequality uses current abs_add_le (Axle 4.31 request 0abc328f-92ed-4428-ad0d-be044f62a25d), and the bounded-continuity theorem is restored to its LiuOppositeSigns owner namespace without adding imports.

[PerAlexandersson]

Pushed 4cd3e0c7 to repair CI run 30803211498. The failure was confined to RealRooted.Mathlib.Data.Multiset.Rel: two list-to-multiset coercions needed simplification, and the final branch needed sorted-tail equalities derived from the cases equations before applying List.Forall₂.cons. All downstream Liu modules had built in that run. Awaiting the new GitHub CI run.

[PerAlexandersson]

Pushed 93b0bb8a to repair comparator run 30806290935. The only failure was RealRooted.Mathlib.Data.Multiset.Rel: Multiset.sort_cons now needs explicit element/multiset/relation arguments. Both tail reconstructions were updated, and the same run’s unnecessary-simpa warning was removed. All downstream Liu modules built in the failed run. Axle request: 3f3913a3-0576-41cf-99b3-b593e6d7471c.

[PerAlexandersson]

Pushed $(git rev-parse --short HEAD) for build 30809143688 / comparator 30809147296. RootMatchingSort now opens the owning Liu/polynomial namespaces and rewrites both nested abs_lt goals; RootCountRelStability opens the namespace owning its root-count declarations; derivative-shift regularization now uses current abs_add_le with ring_nf under abs. Axle requests: 3e345189-7186-4b75-8415-cc3497096a08 and 32112950-6a45-46fc-a8ee-291453a626b5. No local Lake build was run; GitHub CI is restarting.

[PerAlexandersson]

Pushed b1e9e07 for comparator 30818990414. The residual failure was namespace placement only: roots_sort_ge_eq_cons is now declared in LiuOppositeSigns.IsLargestRoot, exactly where receiver-style field notation searches. The theorem statement and proof are unchanged. Axle request: f48b36cf-788e-4631-ab0f-4095baf68186. No local Lake build was run; GitHub CI is restarting.

[PerAlexandersson]

Pushed faaf41e4 to repair the current RootCountClosure.lean comparator failure. The Liu closure argument is unchanged. The patch adds the owning successor-degree and statement imports, centralizes the bounded List.Forall₂ to getD conversion, eta-expands the non-root count bound, transports crossings across the already-proved degree equalities, and calls the generic largest-root perturbation lemma through its actual root namespace. No local Lake build was run; fresh comparator CI is authoritative.