Residue-trace compatibility (form-trace-tower, file 3/6)

Unit: form-trace-tower (docs/design/form-trace-tower.md §2 D4, §4.3, §5 P-main). THE central theorem: Miranda Lemma 3.2 globalized, Res_y(Tr ω) = Σ_{x ∈ F⁻¹y} Res_x(ω).

Deviation from the design, forced by PairForm.lean's finding: the design's own proof plan (§5 P-main step 2–3) invokes resAtX_eq_of_mem_source with the ADAPTED target chart (S.A i).e' in place of chartAt ℂ y₀ — exactly the FALSE general two-chart invariance documented in PairForm.lean's module docstring. Tracing through what actually makes the classical theorem true: AdaptedChartsAt's existence proof (Jacobian/LocalMultiplicity/AdaptedCharts.lean, exists_adaptedChartsAt) always builds its target chart as chartAt ℂ (F x) shifted by an ADDITIVE CONSTANT (e' := (chartAt ℂ (F x) ≫ₕ (Homeomorph.subRight _)) ≫ₕ ofSet _) — a TRANSLATION, whose derivative is the honest CONSTANT 1 (not just at one point but identically), which is exactly the case where changing the target chart costs nothing (no 1/λ-type correction, unlike a general — e.g. scaled — target chart). This translation property is a fact about the concrete construction, not exposed as a field of the abstract AdaptedChartsAt/ FiberStack structures (an adversarial witness could rescale the target chart, which WOULD introduce a genuine correction — see PairForm.lean). Since resAtP1_trace_eq_sum takes an arbitrary S : FiberStack F y₀ as an explicit parameter, this calibration is recorded as an EXPLICIT hypothesis hcal (satisfied by any stack built via exists_fiberStack/ exists_adaptedChartsAt, per direct inspection of their construction) rather than assumed away.

• resAtP1 (D4), resAtP1_eq_resAtX_id.
• resAtP1_trace_eq_sum — THE main theorem (task item 3), with the hcal calibration hypothesis.
• trace_const_mul_pullback, trace_pullback_eq_degree_smul — the projection-formula facts (task item 5, §4.6), NOT gated on the calibration issue at all (pure value/finsum identities).

noncomputable def RS.FormTrace.resAtP1 (R : OnePoint ℂ → ℂ) (y₀ : OnePoint ℂ) : ℂ

Residue at y₀ : ℙ¹ of a function R : ℙ¹ → ℂ, viewed as the coefficient of R·dz.

Equations

• RS.FormTrace.resAtP1 R y₀ = RS.resAt (R ∘ ↑(chartAt ℂ y₀).symm) (↑(chartAt ℂ y₀) y₀)

theorem RS.FormTrace.resAtP1_def (R : OnePoint ℂ → ℂ) (y₀ : OnePoint ℂ) : resAtP1 R y₀ = resAt (R ∘ ↑(chartAt ℂ y₀).symm) (↑(chartAt ℂ y₀) y₀)

theorem RS.FormTrace.resAtP1_eq_resAtX_id (R : OnePoint ℂ → ℂ) (y₀ : OnePoint ℂ) : resAtP1 R y₀ = resAtX id R y₀

Compat: meromorphy is preserved by a translation of the base point

The per-fibre-point identification, under the calibration hypothesis

THE main theorem

theorem RS.FormTrace.resAtP1_trace_eq_sum {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {F : X → OnePoint ℂ} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : OnePoint ℂ), ∀ (x : X), F x = c) {h : X → ℂ} (hh : MeromorphicOnX h Set.univ) {y₀ : OnePoint ℂ} (S : FiberStack F y₀) (hcal : ∀ (i : Fin S.n), ∀ y ∈ (S.A i).e'.source, ↑(S.A i).e' y = ↑(chartAt ℂ y₀) y - ↑(chartAt ℂ y₀) y₀) : resAtP1 (MTrace.trace F h) y₀ = ∑ i : Fin S.n, resAtX F h (S.pt i)

THE main theorem (Miranda Lemma 3.2, globalized over an arbitrary fibre via FiberStack). See the module docstring for the calibration hypothesis hcal, needed because the general two-chart resAtX invariance the design's own proof plan relied on is false (PairForm.lean); hcal is satisfied by any stack produced by exists_fiberStack (per direct inspection of exists_adaptedChartsAt's construction, which always builds a translate of chartAt on the target side).

Projection-formula facts (task item 5, §4.6) — forward-looking, non-blocking exports for

a future jacobian-functoriality unit. Pure VALUE identities (no residues, no chart issue).

theorem RS.FormTrace.trace_const_mul_pullback {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {F : X → OnePoint ℂ} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : OnePoint ℂ), ∀ (x : X), F x = c) {g : OnePoint ℂ → ℂ} (h : X → ℂ) : (MTrace.trace F fun (x : X) => g (F x) * h x) = fun (y : OnePoint ℂ) => g y * MTrace.trace F h y

Miranda Problem VIII.3.D (Tr is ℳ(Y)-linear against pullbacks), value form: TRUE unconditionally over every y — this one goes through mtrace's naive-fibre-sum characterization trace_eq_finsum' directly (no traceZk/branch-point subtlety, since F x = y for every x in the fibre regardless of ramification).

theorem RS.FormTrace.trace_pullback_eq_degree_smul_of_regular {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {F : X → OnePoint ℂ} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : OnePoint ℂ), ∀ (x : X), F x = c) (g : OnePoint ℂ → ℂ) {y₀ : OnePoint ℂ} (hy₀ : IsRegularValue F y₀) : MTrace.trace F (fun (x : X) => g (F x)) y₀ = ↑(degree F) * g y₀

Miranda Problem VIII.3.D's g := 1/degree specialization, Tr(F^*g) = deg·g — restricted to regular values (deviation from the design's unconditional claim, a genuine gap found the same way as PairForm.lean's: at a BRANCH value, traceZk's own junk convention at w = 0 (traceZk h k 0 = h 0, NOT k · h 0 — see PlanarTrace.lean's traceZk_comp_pow, explicitly caveated "genuinely false at w = 0") makes trace F (fun x => g (F x)) compute the NAIVE fibre CARDINALITY, not the multiplicity-weighted degree F, at a branch point — e.g. F := (·^2), g := 1: trace F (fun _ => 1) 0 = 1 (a single preimage 0) but degree F = 2. Provable, and still useful, at REGULAR values, where every fibre point has multiplicity 1 so the naive cardinality IS the degree.