Calibrated fiber stacks (residue-theorem, general-X reduction support)

Unit: residue-theorem (docs/design/residue-theorem.md §6 route, primary per the orchestrator addendum). Jacobian/FormTrace/ResidueTraceCompat.lean's main theorem resAtP1_trace_eq_sum takes an explicit calibration hypothesis hcal: the stack's adapted TARGET charts must be translates of chartAt ℂ y₀. That hypothesis is satisfied by the concrete construction of RS.exists_adaptedChartsAt (whose target chart is literally (chartAt ℂ (F x) ≫ₕ subRight …) ≫ₕ ofSet …) but is NOT exposed by the abstract existential.

This file re-runs the two existence proofs (exists_adaptedChartsAt, exists_fiberStack — Jacobian/LocalMultiplicity/AdaptedCharts.lean and Jacobian/MappingDegree/LocalStructure.lean, copied with attribution per CONVENTIONS.md's Compat discipline; residue-theorem may not edit those units' files) with the single extra conclusion ∀ y, A.e' y = chartAt ℂ (F x) y - chartAt ℂ (F x) (F x) threaded through:

• RS.exists_adaptedChartsAt_translated — adapted charts whose target chart is, as a raw function, the recentered preferred chart at F x.
• RS.exists_fiberStack_translated — a FiberStack all of whose target charts are the recentered chartAt ℂ y₀; this discharges resAtP1_trace_eq_sum's hcal verbatim.

theorem RS.exists_adaptedChartsAt_translated {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) {U : Set X} (hU : U ∈ nhds x) : ∃ (A : AdaptedChartsAt F x (multiplicity F x)), A.e.source ⊆ U ∧ ∀ (y : Y), ↑A.e' y = ↑(chartAt ℂ (F x)) y - ↑(chartAt ℂ (F x)) (F x)

RS.exists_adaptedChartsAt, strengthened with the (construction-inherent) conclusion that the adapted target chart is, as a raw function on all of Y, the recentered preferred chart at F x. Proof copied from Jacobian/LocalMultiplicity/AdaptedCharts.lean (the extra conclusion is rfl for that construction).

Calibrated fiber stacks (standing surface hypotheses)

theorem RS.exists_fiberStack_translated {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) (y₀ : Y) : ∃ (S : FiberStack F y₀), ∀ (i : Fin S.n) (y : Y), ↑(S.A i).e' y = ↑(chartAt ℂ y₀) y - ↑(chartAt ℂ y₀) y₀

RS.exists_fiberStack, strengthened: a stack of adapted charts over y₀ all of whose target charts are, as raw functions, the recentered chartAt ℂ y₀ — exactly resAtP1_trace_eq_sum's calibration hypothesis hcal. Proof copied from Jacobian/MappingDegree/LocalStructure.lean, seeded with exists_adaptedChartsAt_translated.