Arc Contribution to the PV Chain

Proves that the ε-truncated arc integral of f'/f along the FD boundary tends to -(2πik/12) as ε → 0⁺.

The proof uses S-symmetry: the modular S-transformation z ↦ -1/z is an isometry on the unit circle, and the logDeriv functional equation gives F(4-t) + F(t) = -k·(iπ/6)·indicator(t) pointwise. Integrating and using the change of variables t ↦ 4-t yields 2·I(ε) = -k·(iπ/6)·m(ε), where m(ε) → 2.

Main Results

• arc_cpv_contribution_tendsto — Tendsto for sArcOfS S-only truncation
• arc_cpv_eventually_eq_union — bridge from sArcOfS S ∪ sVertOfS S to sArcOfS S
• tendsto_pvIntegral_arc_bridge — final bridge for Assembly.lean

LogDeriv S-transformation

theorem logDeriv_modform_S_transform {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (z : ℂ) (hz : 0 < z.im) (hz_ne : z ≠ 0) (hgz : modularFormCompOfComplex f z ≠ 0) : logDeriv (modularFormCompOfComplex f) z = logDeriv (modularFormCompOfComplex f) (-1 / z) / z ^ 2 - ↑k / z

S-isometry on unit circle

theorem S_isometry_unit_circle (z w : ℂ) (hz : ‖z‖ = 1) (hw : ‖w‖ = 1) : ‖-1 / z - -1 / w‖ = ‖z - w‖

Arc S-reversal

theorem fdBoundary_arc_S_reverse (H t : ℝ) (ht : t ∈ Set.Ioo 1 3) : fdBoundaryH H (4 - t) = -1 / fdBoundaryH H t

Arc indicator symmetry

Integrability of CPV integrand on arc

Arc preimage subsingleton

S-symmetry identity for arc CPV integral

theorem arc_cpv_integral_S_identity {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (S : Finset UpperHalfPlane) (H ε : ℝ) (hε : 0 < ε) (h_oncurve : ∀ t ∈ Set.Ioo 1 3, modularFormCompOfComplex f (fdBoundaryH H t) = 0 → fdBoundaryH H t ∈ ↑(sArcOfS S)) : ∫ (t : ℝ) in 1..3, cauchyPrincipalValueIntegrandOn (sArcOfS S) (logDeriv (modularFormCompOfComplex f)) (fdBoundaryH H) ε t = -(↑k * (↑Real.pi / 12 * Complex.I)) * ↑(∫ (t : ℝ) in 1..3, if ∃ s ∈ sArcOfS S, ‖fdBoundaryH H t - s‖ ≤ ε then 0 else 1)

Non-excluded measure tends to 2

theorem arc_non_excluded_measure_tendsto (S : Finset UpperHalfPlane) (H : ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in 1..3, if ∃ s ∈ sArcOfS S, ‖fdBoundaryH H t - s‖ ≤ ε then 0 else 1) (nhdsWithin 0 (Set.Ioi 0)) (nhds 2)

Arc CPV contribution tends to -(2πik/12)

theorem arc_cpv_contribution_tendsto {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (S : Finset UpperHalfPlane) (H : ℝ) (h_oncurve : ∀ t ∈ Set.Ioo 1 3, modularFormCompOfComplex f (fdBoundaryH H t) = 0 → fdBoundaryH H t ∈ ↑(sArcOfS S)) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in 1..3, cauchyPrincipalValueIntegrandOn (sArcOfS S) (logDeriv (modularFormCompOfComplex f)) (fdBoundaryH H) ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-(2 * ↑Real.pi * Complex.I * ↑k / 12)))

Bridge: sArcOfS S ∪ sVertOfS S → sArcOfS S on arc interval

theorem arc_cpv_eventually_eq_union (S : Finset UpperHalfPlane) (H : ℝ) (g : ℂ → ℂ) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∫ (t : ℝ) in 1..3, cauchyPrincipalValueIntegrandOn (sArcOfS S ∪ sVertOfS S) g (fdBoundaryH H) ε t = ∫ (t : ℝ) in 1..3, cauchyPrincipalValueIntegrandOn (sArcOfS S) g (fdBoundaryH H) ε t

Final bridge for Assembly.lean

theorem tendsto_pvIntegral_arc_bridge {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (S : Finset UpperHalfPlane) {H : ℝ} (_hH : √3 / 2 < H) (h_oncurve_arc : ∀ t ∈ Set.Ioo 1 3, modularFormCompOfComplex f (fdBoundaryH H t) = 0 → fdBoundaryH H t ∈ ↑(sArcOfS S)) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in 1..3, pvIntegrand f (fdBoundaryH H) (sArcOfS S ∪ sVertOfS S) ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-(2 * ↑Real.pi * Complex.I * (↑k / 12))))