Minimal API for ζ on the critical line (design-level abstraction).

This interface decouples downstream development from the concrete implementation of the Riemann zeta function. It only requires measurability and local boundedness along the critical line. Concrete instances can be provided from Mathlib or external libraries; we include a safe placeholder instance that maps to 0, keeping the API usable for testing other components.

class Frourio.ZetaLineAPI : Type

• zeta_on_line : ℝ → ℂ
• measurable : Measurable zeta_on_line
• loc_bounded (R : ℝ) : ∃ (C : ℝ), ∀ (τ : ℝ), |τ| ≤ R → ‖zeta_on_line τ‖ ≤ C

Default placeholder instance: ζ(1/2 + iτ) ≡ 0. This satisfies measurability and local boundedness trivially, and can be replaced by a true instance when available without breaking downstream code.

noncomputable instance Frourio.defaultZetaLineAPI : ZetaLineAPI

Equations

• Frourio.defaultZetaLineAPI = { zeta_on_line := fun (x : ℝ) => 0, measurable := Frourio.defaultZetaLineAPI._proof_1, loc_bounded := Frourio.defaultZetaLineAPI._proof_2 }

structure Frourio.ZetaData : Type

Phase 5.1: injectable data for supplying a concrete ζ on the critical line. This allows users to provide their own implementation (e.g. from Mathlib) and produce a ZetaLineAPI value without committing it as a global instance.

• zeta_on_line : ℝ → ℂ
• measurable : Measurable self.zeta_on_line
• loc_bounded (R : ℝ) : ∃ (C : ℝ), ∀ (τ : ℝ), |τ| ≤ R → ‖self.zeta_on_line τ‖ ≤ C

noncomputable def Frourio.ZetaLineAPI.ofData (d : ZetaData) : ZetaLineAPI

Build a ZetaLineAPI record from provided measurable/locally-bounded data.

Equations

• Frourio.ZetaLineAPI.ofData d = { zeta_on_line := d.zeta_on_line, measurable := ⋯, loc_bounded := ⋯ }

noncomputable def Frourio.ZetaData.mk' (f : ℝ → ℂ) (hf_meas : Measurable f) (hf_loc : ∀ (R : ℝ), ∃ (C : ℝ), ∀ (τ : ℝ), |τ| ≤ R → ‖f τ‖ ≤ C) : ZetaData

Convenience: construct ZetaData from a function and proofs.

Equations

• Frourio.ZetaData.mk' f hf_meas hf_loc = { zeta_on_line := f, measurable := hf_meas, loc_bounded := hf_loc }

noncomputable def Frourio.ZetaData.const (c : ℂ) : ZetaData

Example: constant function as a trivial ZetaData provider.

Equations

• Frourio.ZetaData.const c = { zeta_on_line := fun (x : ℝ) => c, measurable := ⋯, loc_bounded := ⋯ }