Formalize Carathéodory's and Loewner's conjectures

[Paul-Lez]

This PR does the following:

• formalize the smooth and real-analytic Loewner conjectures using the winding number of the trace-free Hessian;
• formalize smooth and real-analytic Carathéodory conjectures for parametrized convex two-spheres;
• formulate Carathéodory umbilics through proportional first and second fundamental forms, with reusable equivalence lemmas;
• record that the smooth Loewner conjecture implies the smooth Carathéodory conjecture.

The classical formulations follow Ghomi’s Problems 8.1 and 8.2, with the analytic results sourced to Titus.

The complete sorry-free counterexample proof is in the dependent draft PR #5070. That PR proves both smooth statements false, pins their formal_proof metadata to a kernel-checked commit, and includes the full informal proof.