The challenge-signature mapping degree (proper-map-degree, file 1 of 3)

Unit: proper-map-degree (docs/design/proper-map-degree.md §3.1). Root-level wrapper of RS.degree (Jacobian/MappingDegree/Degree.lean) matching the EXACT signature the challenge file (docs/Jacobian_challenge.lean:147) demands.

• _root_.ContMDiff.degree (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) : ℕ — the degree of a holomorphic map between compact Riemann surfaces; 0 for constant maps, else RS.degree f.
• ContMDiff.degree_eq, ContMDiff.degree_of_forall_eq, ContMDiff.degree_comp — restated corollaries in wrapper form (statement bank, API parity with RS.degree/RS.degree_comp).

Deviation from the design doc (proper-map-degree.md §3.1): the design's sketch declared variable {f : X → Y} (implicit). The challenge file's own preamble (docs/Jacobian_challenge.lean:104, variable (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)) declares f explicit — confirmed load-bearing by its own call site pushforward_pullback's RHS (ContMDiff.degree f hf) • P, which applies f positionally. To match "the exact challenge signature" this file declares f explicit throughout; hf.degree (dot notation) still works since f is fully determined by unification against hf's type.

noncomputable def ContMDiff.degree {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] (f : X → Y) (_hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) : ℕ

The degree of a holomorphic map between compact Riemann surfaces (challenge signature, docs/Jacobian_challenge.lean:147). Equal to 0 for constant maps (RS.degree_of_forall_eq), otherwise the usual mapping degree (RS.degree). One-line wrapper — RS.degree already has the right junk-0 convention definitionally, no case split needed. [Nonempty Y] (needed by RS.degree) is discharged for free by ConnectedSpace.toNonempty (Mathlib.Topology.Connected.Basic:636).

Equations

• ContMDiff.degree f _hf = RS.degree f

@[simp]

theorem ContMDiff.degree_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) : degree f hf = RS.degree f

theorem ContMDiff.degree_of_forall_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] {c : Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ fun (x : X) => c) : degree (fun (x : X) => c) hf = 0

Restated junk convention in wrapper form (RS.degree_of_forall_eq, unfolded).

theorem ContMDiff.degree_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {Z : Type u_3} [TopologicalSpace Z] [T2Space Z] [ConnectedSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Z] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g) (hneG : ¬∃ (c : Z), ∀ (y : Y), g y = c) (hneF : ¬∃ (c : Y), ∀ (x : X), f x = c) : degree (g ∘ f) ⋯ = degree g hg * degree f hf

Functoriality, restated in wrapper form (statement bank; no critical consumer identified, kept for API parity with RS.degree_comp).