Bridge functor axiom
The Bridge functor axiom (III.D71) is the first of three custom axioms in TauLib beyond Mathlib's trusted base. It asserts the existence of a structure-preserving functor between τ-admissible spectral data and the orthodox classical formulations (Riemann zeta, Dirichlet/Hecke L-functions). Spectral-purity results in the τ-internal world translate to classical statements on the τ-admissible sub-domain. The axiom is finite-checked but not constructively proved: every finite (n, k) bound has been verified, but the universal extension is the conjectural step.
τ-Definition
The Bridge functor axiom (III.D71) is the first of three custom axioms in TauLib beyond Mathlib's trusted base. It asserts the existence of a structure-preserving functor between τ-admissible spectral data and the orthodox classical formulations (Riemann zeta, Dirichlet/Hecke L-functions). Spectral-purity results in the τ-internal world translate to classical statements on the τ-admissible sub-domain. The axiom is finite-checked but not constructively proved: every finite (n, k) bound has been verified, but the universal extension is the conjectural step.
Categorical invariant. A functor B : τ-Spec → Class-Spec preserving spectral purity, asserted to exist universally on τ-admissible inputs; the universal claim is the axiom, the finite envelope check is provable.
Primary registry anchor:
III.D71
τ-Derivation Chain
-
I.K0— Universe Postulate -
II.T40— Central theorem at rank (3, 15) — τ-internal categorical anchor -
III.T18— Spectral correspondence theorem — within τ, spectral data and admissible classical data correspond at finite (n, k) -
III.D71— Bridge functor axiom — universal extension of the spectral correspondence to all τ-admissible inputs (this entry)
Lean modules referenced:
TauLib.BookIII.Bridge.BridgeAxiom
Mathematical content
There exists a structure-preserving functor B : τ-Spec → Class-Spec from τ-admissible spectral data to classical formulations (Riemann zeta, Dirichlet L-functions, Hecke L-functions). B preserves spectral-purity results: every τ-internal spectral-purity theorem translates to a classical statement on the τ-admissible sub-domain.
What is finite-checked. For all τ-admissible spectral data up to a stated finite (n, k) bound (currently k ≤ 15), the functor's structure-preserving behaviour and the spectral-purity translation have been verified via native_decide. The trichotomy (III.T18) classifications match for all bounded configurations.
What is axiomatized. The universal extension: the functor B exists and preserves spectral purity for all τ-admissible data, not just the finite-check window.
What closes the gap. A constructive proof of the functor's existence for unbounded (n, k), or a rigorous obstruction argument that the finite-check must extend. Active research.
Load-bearing for. The Master Schema (III.T23) — the bridge between τ-internal Riemann Hypothesis results and the classical Clay statement — depends on this axiom. Classical-RH claims are marked Partial on the site, not internally addressed. The τ-internal Critical Line Theorem (III.T19) is preserved under retraction; the classical bridge falls.
Lean Coverage
Status: Formalized
Module: TauLib.BookIII.Bridge.BridgeAxiom
Lean kind: axiom
Lean symbol: Tau.BookIII.Bridge.bridgeFunctorExists