The arc self-pairing of the logarithmic-derivative integrand

The reflection t ↦ 4 - t carries the unit-circle arc of the boundary contour to its own reversal through the inversion S. Composed with the S-transformation law of the logarithmic derivative of a weight-k form, the reflected integrand logDeriv g (γ (4 - t)) · γ' (4 - t) pairs with the direct one up to the weight term -k · γ' / γ — so the two halves of the arc integral collapse to -k times the integral of γ' / γ, whose integrand is π/6 · i on the open arc and hence almost everywhere: the arc contributes -k/12 to the (2πi)⁻¹-normalized valence contour, the term that lands as k/12 on the divisor side of the valence formula.

Main declarations

• TauCeti.ModularForm.logDeriv_comp_ofComplex_fdBoundary_arc_add_four_sub_eq_neg: the direct and reflected arc contour integrands sum to the negated weight term.
• TauCeti.ModularForm.intervalIntegral_deriv_smul_logDeriv_comp_ofComplex_fdBoundary_arc: the arc contour integral of the form's logarithmic derivative evaluates to -(k * (π/6 * I)), the arc's -k/12 contribution to the normalized valence contour.

The same pairing survives ε-excision, which is what the principal-value assembly needs: when the form vanishes at a point on the arc the unexcised integrand is not interval-integrable there, so the boundary integral is assembled from an excised integrand. Excision is compatible with the reflection whenever the excision set consists of unit-modulus points closed under the inversion z ↦ -1/z.

• TauCeti.ModularForm.excised_logDeriv_comp_ofComplex_fdBoundary_arc_add_four_sub_eq_neg: the excised pointwise pairing — at an excised parameter both terms vanish, at a retained one the direct and reflected excised integrands sum to the excised weight term.
• two_mul_intervalIntegral_excised_deriv_smul_logDeriv_comp_ofComplex_fdBoundary_arc (in TauCeti.ModularForm, unqualified here only to stay inside the line limit) — the excised arc integral is -k/2 times the excised integral of the contour's own logarithmic derivative.

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/ValenceFormula/PVChain/ArcContribution.lean) this file ports onto the current Mathlib pin.

theorem TauCeti.ModularForm.logDeriv_comp_ofComplex_fdBoundary_arc_add_four_sub_eq_neg {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {H t : ℝ} (ht : t ∈ Set.Ioo 1 3) (hd : DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) (hne : (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) ≠ 0) : deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) + deriv (fdBoundary H) (4 - t) • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H (4 - t)) = -(↑k * logDeriv (fdBoundary H) t)

On the open arc, the direct and reflected logarithmic-derivative contour integrands sum to the negated weight term -k · logDeriv γ.

theorem TauCeti.ModularForm.intervalIntegrable_deriv_smul_logDeriv_comp_ofComplex_fdBoundarySegment3 {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {H : ℝ} (hd : ∀ t ∈ Set.Ioo 1 2, DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) (hne : ∀ t ∈ Set.Ioo 1 2, (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) ≠ 0) (hint : IntervalIntegrable (fun (t : ℝ) => deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 1 2) : IntervalIntegrable (fun (t : ℝ) => deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 2 3

The reflected-half integrability: interval integrability of the arc contour integrand on [2, 3] follows from integrability on [1, 2] through the pairing, which writes the second half as a reflected constant-minus-first-half integrand.

theorem TauCeti.ModularForm.intervalIntegral_deriv_smul_logDeriv_comp_ofComplex_fdBoundary_arc {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {H : ℝ} (hd : ∀ t ∈ Set.Ioo 1 2, DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) (hne : ∀ t ∈ Set.Ioo 1 2, (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) ≠ 0) (hint : IntervalIntegrable (fun (t : ℝ) => deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 1 2) : ∫ (t : ℝ) in 1..3, deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) = -(↑k * (↑(Real.pi / 6) * Complex.I))

The arc contour integral of a slash-invariant form's logarithmic derivative is -(k * (π/6 * I)) — the arc's -k/12 contribution to the (2πi)⁻¹-normalized valence contour. The two halves of the arc pair through the S-transformation under the substitution t ↦ 4 - t, leaving -k times the constant arc integral of the contour's own logarithmic derivative.

theorem TauCeti.ModularForm.excised_logDeriv_comp_ofComplex_fdBoundary_arc_add_four_sub_eq_neg {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {H : ℝ} {S : Finset ℂ} {ε t : ℝ} (ht : t ∈ Set.Ioo 1 3) (hnorm : ∀ s ∈ S, ‖s‖ = 1) (hinv : ∀ s ∈ S, -1 / s ∈ S) (hd : (¬∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε) → DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) (hne : (¬∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε) → (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) ≠ 0) : ((if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) + if ∃ s ∈ S, ‖fdBoundary H (4 - t) - s‖ ≤ ε then 0 else deriv (fdBoundary H) (4 - t) • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H (4 - t))) = if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else -(↑k * logDeriv (fdBoundary H) t)

The arc pairing under excision. At an excised parameter both terms vanish; at a retained one the direct and reflected excised integrands sum to the excised weight term, exactly as in TauCeti.ModularForm.logDeriv_comp_ofComplex_fdBoundary_arc_add_four_sub_eq_neg.

Regularity is asked only where the integrand is retained: at an excised parameter the form may vanish or fail to be differentiable, which is the point of excising it.

theorem TauCeti.ModularForm.intervalIntegrable_excised_const {H ε : ℝ} {S : Finset ℂ} (c : ℂ) (a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else c) MeasureTheory.volume a b

An excised constant is interval-integrable. It is measurable, because the excision set is, and bounded by the constant's norm.

theorem TauCeti.ModularForm.intervalIntegrable_excised_deriv_smul_logDeriv_comp_ofComplex_fdBoundarySegment3 {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {H : ℝ} {S : Finset ℂ} {ε : ℝ} (hnorm : ∀ s ∈ S, ‖s‖ = 1) (hinv : ∀ s ∈ S, -1 / s ∈ S) (hd : ∀ t ∈ Set.Ioo 1 2, (¬∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε) → DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) (hne : ∀ t ∈ Set.Ioo 1 2, (¬∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε) → (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) ≠ 0) (hint : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 1 2) : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 2 3

Integrability on the second arc half, excised. The reflection t ↦ 4 - t exchanges the two halves of the arc, and the excised pointwise pairing identity rewrites the integrand on [2, 3] as the excised weight minus the reflected integrand on [1, 2] — both integrable. This is the excised counterpart of intervalIntegrable_deriv_smul_logDeriv_comp_ofComplex_fdBoundarySegment3.

theorem TauCeti.ModularForm.two_mul_intervalIntegral_excised_deriv_smul_logDeriv_comp_ofComplex_fdBoundary_arc {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {H : ℝ} {S : Finset ℂ} {ε : ℝ} (hnorm : ∀ s ∈ S, ‖s‖ = 1) (hinv : ∀ s ∈ S, -1 / s ∈ S) (hd : ∀ t ∈ Set.Ioo 1 2, (¬∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε) → DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) (hne : ∀ t ∈ Set.Ioo 1 2, (¬∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε) → (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) ≠ 0) (hint : IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) MeasureTheory.volume 1 2) : (2 * ∫ (t : ℝ) in 1..3, if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) = -↑k * ∫ (t : ℝ) in 1..3, if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else logDeriv (fdBoundary H) t

The excised arc integral collapses to the weight term. Integrating the pointwise pairing over [1, 3], where the reflection t ↦ 4 - t maps the interval to itself, the excised arc integral is -k/2 times the excised integral of the contour's own logarithmic derivative.

The statement is for one fixed ε and one fixed excision set S; it asserts nothing about a limit. Its intended use is as the ε-uniform input to the principal-value assembly, which supplies the extra hypotheses that identify a principal value — that S captures every zero of the form on the arc, and the convergence of the excised right-hand side as the excision shrinks. Neither is assumed here, and neither follows from this statement alone.

The excised form is what the assembly needs because where the form vanishes on the arc the unexcised integrand is not interval-integrable. Only when the form is zero-free on the arc does this specialize to the untruncated TauCeti.ModularForm.intervalIntegral_deriv_smul_logDeriv_comp_ofComplex_fdBoundary_arc.