ContourIntegration: pin (or defer) HW Prop 2.2/2.3 — not in AINTLIB, would be new mathematics

[CBirkbeck]

With the Thm 3.3 summit chain complete on the TauCeti side (summits built against #70,
awaiting its merge), the only remaining ContourIntegration items are the two Layer-1
narrative milestones from README.md that are not pinned in Suggested.lean:

• HW Prop 2.3 (the real bounded-integrand formula n₀(Λ) = (1/2π)∫(xẏ−yẋ)/(x²+y²) with
  the ½·k_Λ·|Λ̇| crossing value): not formalized in AINTLIB at all — the whole source
  development is complex-PV-based; no curvature notion exists there. Porting is impossible;
  building it is greenfield (real integrand, boundedness, C^{1,1}/C² regularity split,
  signed-curvature limit).
• HW Prop 2.2's decomposition sum (n_{z₀}(Λ) = n(Λ̃) + Σ αℓ/2π): AINTLIB has the
  per-crossing pieces (crossing angle, finiteness, per-crossing L/2πi winding
  contributions) but never assembles the sum; the model-sector Λ̃ construction and the
  aggregation theorem don't exist in the source either.

Since the roadmap gates new mathematics on pinned targets, and the README's "migrate from
AINTLIB" framing doesn't hold for these two, a decision is needed:

1. Pin them in Suggested.lean as explicit targets (I can draft signatures — TauCeti's
   merged per-window machinery already contains most of a native Prop 2.2 proof), or
2. Defer/drop them from the ContourIntegration scope (the valence formula's actual
   consumer is Thm 3.3 + the winding values, both done; Prop 2.3 is a computational
   convenience, not a dependency of any pinned target).

Happy to go either way — flagging rather than building, per the roadmap contract.

🤖 Generated with Claude Code

[CBirkbeck]

As offered — a concrete signature draft, should you choose to pin. The decomposition
(Prop 2.2) is statable without constructing the indented curve Λ̃ (the genuinely new
part AINTLIB also never built) by phrasing it as integrality of the residual: the winding
number is an integer plus the crossing-angle sum over the (finite) crossing set,

/-- HW Prop 2.2, residual form: about any point, the generalized winding number of a closed
piecewise-C¹ immersion differs from `(2π)⁻¹ · Σ` of its crossing angles by an integer. -/
theorem windingNumber_sub_crossingAngle_sum_mem_integers
    {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (hγ_imm : IsPwC1ImmersionOn γ a b)
    (hclosed : γ a = γ b) (hγa : γ a ≠ z₀)
    (crossings : Finset ℝ)
    (h_mem : ∀ t ∈ crossings, t ∈ Set.Ioo a b ∧ γ t = z₀)
    (h_complete : ∀ t ∈ Set.Icc a b, γ t = z₀ → t ∈ crossings) :
    ∃ n : ℤ, windingNumber γ a b z₀
      = n + (2 * Real.pi)⁻¹ * ∑ t ∈ crossings, crossingAngle γ t

This captures the paper's content (winding = integer + Σ αℓ/2π), uses only merged TauCeti
objects (crossingAngle exists in RegularityConditions.lean), and most of its proof is
already merged (the per-window argument limits of the crossing machinery). Prop 2.3's real
curvature formula I'd propose deferring: it's greenfield (no AINTLIB source), needs a
curvature notion Mathlib lacks, and nothing pinned consumes it.

🤖 Generated with Claude Code