Distinct ordered analytic branches

For a finite family of real analytic germs, suppose every pair coinciding at the central parameter agrees as germs. Selecting one label for each distinct central value produces analytic functions on a common open neighborhood, strictly ordered at every parameter there, with exactly the same range as the original family. Thus repeated root labels can be removed without losing analyticity or any roots. The selection is fixed throughout the neighborhood; it is not a pointwise sorting operation. Zero branches and empty families are allowed.

The collision hypothesis is essential: the germs x ↦ x and x ↦ -x coincide at zero but their distinct-value count changes there. For polynomial root branches, persistence of collisions must be established before applying the ordering theorem.

References

S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Section 4.

theorem TauCeti.exists_analyticOnNhd_strictMono_range_eq {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Finite ι] {f : ι → E → ℝ} {x₀ : E} (hf : ∀ (i : ι), AnalyticAt ℝ (f i) x₀) (heq : ∀ (i j : ι), f i x₀ = f j x₀ → f i =ᶠ[nhds x₀] f j) : ∃ (k : ℕ) (e : Fin k ↪ ι) (U : Set E), IsOpen U ∧ x₀ ∈ U ∧ (∀ (i : Fin k), AnalyticOnNhd ℝ (f (e i)) U) ∧ ∀ x ∈ U, (StrictMono fun (i : Fin k) => f (e i) x) ∧ (Set.range fun (i : Fin k) => f (e i) x) = Set.range fun (i : ι) => f i x

Remove repeated labels from a finite real analytic family with persistent central collisions. On one open neighborhood the selected original functions are analytic, strictly increasing in their index, and enumerate exactly the original range. The embedding selects labels once and for all, so further identities of the original branches remain available.