Density.lean — the reusable "dense ⟹ everywhere" closing lemma (jacobian-functoriality §5)

Unit: jacobian-functoriality. RS.Form1.eq_of_eqOn_dense ("Lemma A"): two Form1s whose coeffAts agree on a dense set of the manifold are equal. Used downstream by Trace.lean's compat, the projection formula, and the comp-functoriality laws.

Design deviation (recorded, not silently dropped): the design sketch proposed routing this through a standalone Form1.continuous_coeffAt : Continuous (fun x => coeffAt x η). That statement needs genuine tangent-bundle continuity theory (continuity of mfderiv (chartAt ℂ x) as its base point x varies, not at a fixed point) that does not reduce to anything already built in this project. This is avoided entirely: fix an arbitrary reference chart e₀ at x₀. For x in e₀'s source, coeffAt x η = deriv (⇑e₀ ∘ ⇑(chartAt ℂ x).symm) (chartAt ℂ x x) * coeffIn e₀ η (e₀ x) (RS.coeffAt_eq_deriv_mul_coeffIn, a pure algebraic identity via RS.coeffIn_trans, no continuity-in-x needed). Since this transition factor is the same nonzero number for η and η' (RS.analyticAt_transition's nonvanishing-derivative half), the hypothesis coeffAt x η = coeffAt x η' cancels it, reducing the comparison to coeffIn e₀ η vs. coeffIn e₀ η' — two fixed-chart functions, continuous on e₀.target by Form1.continuousOn_coeffIn (already built, no gap) — agreeing on a dense subset of e₀.target (image of the dense hypothesis set), hence equal there by a direct filter/uniqueness-of-limits argument (tendsto_nhds_unique_of_eventuallyEq).

theorem RS.coeffAt_eq_deriv_mul_coeffIn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) {e₀ : OpenPartialHomeomorph X ℂ} (he₀ : e₀ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {x : X} (hx : x ∈ e₀.source) : coeffAt x η = deriv (↑e₀ ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x) * coeffIn e₀ η (↑e₀ x)

The preferred-chart coefficient, read against a fixed reference chart e₀ valid at x: a pure chain-rule identity (RS.coeffIn_trans applied between e₀ and chartAt ℂ x), no continuity-in-x involved.

theorem RS.deriv_transition_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {e₀ : OpenPartialHomeomorph X ℂ} (he₀ : e₀ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {x : X} (hx : x ∈ e₀.source) : deriv (↑e₀ ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x) ≠ 0

The chart-transition factor above never vanishes (a chart composed with its own inverse is the identity; RS.analyticAt_transition's nonvanishing-derivative half).

theorem RS.ContinuousOn.eqOn_of_subset_closure {f g : ℂ → ℂ} {U : Set ℂ} (hUo : IsOpen U) (hf : ContinuousOn f U) (hg : ContinuousOn g U) {T : Set ℂ} (hTU : U ⊆ closure T) (heq : Set.EqOn f g T) : Set.EqOn f g U

Two continuous-on-U planar functions agreeing on a subset T whose closure covers U agree on all of U (elementary filter/uniqueness-of-limits argument; the standard "dense ⟹ everywhere" fact specialized to an open domain, avoiding the need for global Continuous).

theorem RS.target_subset_closure_image_inter {X : Type u_1} [TopologicalSpace X] {e₀ : OpenPartialHomeomorph X ℂ} {s : Set X} (hs : Dense s) : e₀.target ⊆ closure (↑e₀ '' (s ∩ e₀.source))

Density transports along a chart: if s is dense in X, then every point of e₀.target is in the closure of e₀ '' (s ∩ e₀.source).

theorem RS.Form1.eq_of_eqOn_dense {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η η' : Form1 X} {s : Set X} (hs : Dense s) (h : Set.EqOn (fun (x : X) => coeffAt x η) (fun (x : X) => coeffAt x η') s) : η = η'

Lemma A. Two holomorphic 1-forms whose coeffAts agree on a dense set (in particular, on the cofinite complement of a finite set, e.g. a branch/critical locus) are equal.