1 Introduction

1.1 The unifying perspective

This paper unifies six standalone research papers, each addressing one of six open problems flagged at the end of the synthesis paper of our prior series, the Univalent Correspondence. The prior series was a six-paper survey of how the natural number 58 is described from six foundational perspectives — naive (Paper I), set-theoretic (Paper II), universal-property (Paper III), Yoneda (Paper IV), HoTT (Paper V), and categorical/structural (Paper VI) — culminating in a synthesis (Paper VII) that demonstrated, under the univalence axiom, that the four formal descriptions III–VI literally name the same object. The prior synthesis ended by listing six concrete open problems whose resolution would extend that picture from the natural numbers to the structures of contemporary analytic mathematics. The present paper unifies, under a single perspective, the six standalone papers that take up those problems.

The single perspective is the one identified by the prior synthesis as the principal open problem: the absence of a HoTT-native formulation of analytic number theory, and in particular the absence of a HoTT-native object $\zeta :{\mathbb{C}}_c\to {\mathbb{C}}_c$ together with a HoTT-native proposition $\zeta (s)=0$ that one could conjecturally inhabit. We organise all six papers as steps toward that goal. Some of them are direct prerequisites (Part II provides a cubical Cauchy-real construction on which any analytic-NT programme must rest); some address infrastructural prerequisites of the prerequisites (Part IV ensures that the $(\infty ,1)$-categorical natural-numbers object behaves correctly inside the ambient $\infty$-topos); some open up parallel apparatus that may ultimately be necessary (Part I’s coalgebraic transcendentals and Part V’s directed univalence); some clarify the foundational landscape against which everything is assembled (Part III’s comparison of ETCS, IZF, FOLDS). Part VI is the centerpiece: it stitches the others into a roadmap.

1.2 Why the unifying perspective is meaningful

It is tempting to dismiss the proposed unification as nominal: a series of papers about disparate things, retrofitted under a common heading. We argue the contrary. The six topics are not independent: each invokes the apparatus of the others, often in essential ways. To make a HoTT-native $\zeta$ we need

• HoTT-native real numbers (Part II) and the complex numbers built from them;

• primitive recursion / iteration on $\mathbb{N}$, hence an NNO whose universal property is correctly stated in the $(\infty ,1)$-categorical context where holomorphic functions live (Part IV);

• a constructive analysis library that respects the inductive / coinductive duality (Part I), since power series and Dirichlet series are inductively-defined limits of coinductively-presented streams of partial sums;

• a foundational frame in which the relation “$\zeta$ depends only on the structure of ${\mathbb{C}}_c$ as a topological field” is automatic, not a separate metatheorem (Part III);

• a synthetic notion of category and functor strong enough to express Galois actions, automorphic representations, and the entire Tannakian frame around $L$-functions, hence directed univalence (Part V);

• finally, a coordinator paper that takes all of the above and produces an actual roadmap to the goal (Part VI).

Removing any one of the six components leaves a perceptible gap in the chain. We will spell out, in 2, the single mathematical artifact in which all six contributions live, namely the ambient $(\infty ,1)$-topos with directed-univalent structure presheaves and a Riemann-zeta object as a synthetic distribution; and we shall trace the precise way in which each of the six papers contributes a piece of the construction.

1.3 Relation to the prior series

The prior series was about the natural numbers and their identity. It established that the natural numbers, viewed from any of the four formal perspectives III–VI, are the same object, which was the central claim of the prior synthesis. The present series extends that programme along two axes.

From $\mathbb{N}$ to ${\mathbb{R}}_c,{\mathbb{C}}_c,\zeta$. The prior series developed the infrastructure (NNOs, HoTT, univalence, structuralism) but applied it mostly to discrete objects (natural numbers, finite groups, ${\pi }_1(S^1)$). The principal continuous object whose HoTT presentation it discussed was the Cauchy reals ${\mathbb{R}}_c$, but only as a HIIT in Book HoTT, and only for the purpose of defining $\pi$ and $e$ as centres of contractible subtypes (Paper V §8). The present series goes further: a complete coalgebraic dual for transcendentals (Part I), a cubical formalisation of the HIIT itself (Part II), and the analytic objects — complex numbers, holomorphic functions, Dirichlet series, $L$-functions — needed to write down $\zeta$ (Part VI).

From 1-categorical to $(\infty ,1)$-categorical. The prior series worked mostly in 1-categorical universe, citing Lurie and Riehl–Shulman where necessary but not developing the higher-categorical theory. The present series tightens the higher-categorical frame: contractibility of the type of $(\infty ,1)$-categorical NNOs (Part IV), directed univalence of the universe of discrete types (Part V), and a complete recasting of the Riemann zeta function as an internal object of an $(\infty ,1)$-topos (Part VI §4–5).

The two extensions interact: the analytic side requires the higher categorical, because holomorphic functions, Galois actions, and automorphic forms all live naturally in $(\infty ,1)$-toposes. This is what makes the unification non-trivial. We summarise the relation in 1.

1.4 Organisation of this paper

2 fixes notation and gives the unified mathematical framework. [sec:partI,sec:partII,sec:partIII,sec:partIV,sec:partV,sec:partVI] treat each of the six component papers in turn, devoting roughly two pages to each: a half-page recap, the principal theorems, and the connection to the others. 9 extracts the five cross-cutting themes. 10 reformulates Part VI’s six sub-problems as compositional gates, showing how the apparatus from Parts I–V combine to make each sub-problem well-posed. 12 concludes with the outstanding open questions for the next round of the programme.

2 The Unified Framework

2.1 Ambient setting

Throughout we work inside an elementary $(\infty ,1)$-topos $\mathcal{E}$ in the sense of Rasekh . By Shulman’s theorem , $\mathcal{E}$ admits an interpretation of homotopy type theory with the univalence axiom; we view that interpretation as the internal language. We will alternate between external talk (objects of $\mathcal{E}$, morphisms in $\mathcal{E}$) and internal talk (types $A:\mathcal{U}$, terms $a:A$, identity types $a{=}_{A}b$, equivalences $A\simeq B$). Where the distinction matters we shall flag it.

The universe $\mathcal{U}:{\mathcal{U}}^{\prime }$ is univalent: for $A,B:\mathcal{U}$, $$\begin{array}{c}\mathsf{idtoeqv}:(A{=}_{\mathcal{U}}B)\to (A\simeq B)\end{array}$$ is an equivalence (Paper V ). When we want a directed-univalent universe we shall write $\mathcal{S}$ for the universe of discrete types in the sense of Riehl–Shulman simplicial type theory , in which there is a definable map $\mathsf{funtohom}:{\mathrm{Hom}}_{\mathcal{S}}(A,B)\to (A\to B)$ that is an equivalence after Gratzer–Weinberger–Buchholtz ; see Part V (7 below).

2.2 The unified triple

1 is the central object of this paper. Each of Parts I–VI contributes either a component, a justification, or a structural property of the triple. Specifically:

• Part I: provides the coalgebraic dual presentation of ${\mathbb{C}}_c$ used to make sense of $\zeta$ as the limit of a stream of partial sums.

• Part II: provides the cubical formalisation of ${\mathbb{R}}_c$, hence of ${\mathbb{C}}_c={\mathbb{R}}_c\times {\mathbb{R}}_c$.

• Part III: certifies that the HoTT-internal definition of $\zeta$ is invariant under the choice between ETCS, IZF, FOLDS, and HoTT via the univalence boundary.

• Part IV: certifies that the NNO needed for the Dirichlet sum ${\sum }_{n\ge 1}{n}^{-s}$ in the $(\infty ,1)$-categorical universe is contractibly unique.

• Part V: certifies that automorphic representations, which are directed objects, can be expressed using $\mathsf{dua}$.

• Part VI: assembles the triple and posits the six sub-problems whose collective resolution gives a HoTT-native proof of, say, $\zeta (2)={\pi }^2/6$ and a HoTT-native statement of the Riemann hypothesis.

2.3 Notation and types

We write $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$ for the standard discrete types of natural numbers, integers, and rationals. We write ${\mathbb{R}}_c$ for the Cauchy reals as a HIIT (Paper V §11.3 / Booij , formalised in Part II) and ${\mathbb{C}}_c:={\mathbb{R}}_c\times {\mathbb{R}}_c$ with the standard field structure. We write $\mathsf{Aut}(A)$ for the type of self-equivalences of $A$, and $\mathsf{isContr}(A)$ for the proposition that $A$ is contractible.

3 Part I: Coalgebraic Transcendentals

3.1 Recap

Part I  addresses the open problem flagged at the end of the prior synthesis (§8 item 1): a final-coalgebra characterisation of $\pi$ and $e$ that avoids the inductive HIIT route. The prior synthesis (Paper V §8) defined $\pi$ and $e$ as centres of contractible subtypes of the inductive Cauchy reals. Part I provides the dual description: $\pi$ is the unique element of an explicit final coalgebra modulo carry-bisimulation, distinguished by a categorical predicate that does not invoke the inductive presentation.

3.2 Principal theorems

The predicates $P_{\pi },P_e$ are stated coalgebraically: $P_{\pi }$ asserts that the stream is the unique fixed point of the BBP digit-extraction coendomorphism, and $P_e$ asserts that the stream is the bisimulation class of the unique fixed point of the spigot algorithm of .

3.3 Connection to the unified triple

Part I gives the coalgebraic half of the inductive–coinductive duality. In the unified framework the relevance is direct: the Dirichlet series $\sum n^{-s}$ is most naturally presented as a stream of partial sums, and convergence is a coinductive property. 3 provides the prototype: a transcendental real expressed as the unique element of a final coalgebra picked out by a coinductive predicate. The same recipe will apply to $\zeta (2k)$ (rational multiples of ${\pi }^{2k}$) once Part VI’s machinery is in place.

3.4 Cross-references

Part I cites Part II for the cubical Cauchy-real construction whose existence it presupposes, and Part VI for the analytic context in which its transcendentals are deployed. Within the prior series, Part I extends Paper III §5 (coinductive presentation of $\mathbb{R}$), Theorem 5.2 (streams as final coalgebra), and Paper V §8 (inductive presentation of $\pi ,e$).

4 Part II: Cubical HIITs and the Cauchy Reals

4.1 Recap

Part II  addresses the open problem (Synthesis §8 item 6) of giving a clean cubical-Agda formalisation of the HIIT Cauchy reals. The prior series (Paper V §5.4 / Booij ) constructed ${\mathbb{R}}_c$ as a HIIT in Book HoTT; the present part transports the construction to cubical Agda  where univalence is constructive.

4.2 Principal theorems

4.3 Connection to the unified triple

Part II provides the foundational object on which Part VI builds. In the unified framework: ${\mathcal{U}}_{\mathrm{cu}}$ is the cubical universe whose existence is asserted by Cubical Agda, and ${\mathbb{R}}_c\in {\mathcal{U}}_{\mathrm{cu}}$ is the HIIT just constructed. Hence $${\mathbb{C}}_c:={\mathbb{R}}_c\times {\mathbb{R}}_c\in {\mathcal{U}}_{\mathrm{cu}}.$$ It is in ${\mathbb{C}}_c$ that the zeta function lives.

4.4 Cross-references

Part II provides the carrier on which all of Part I’s coalgebraic constructions ultimately rest (since $[0,1]$ is a quotient of digit streams that must equal a sub-HIIT of ${\mathbb{R}}_c$), and the carrier on which Part VI’s $\zeta$ is built.

5 Part III: ETCS, IZF, FOLDS

5.1 Recap

Part III  addresses the open problem (Synthesis §8 item 3) of comparing three structural foundations against each other and against HoTT. ETCS (Lawvere 1964 ) replaces ZFC by an axiomatisation of the category of sets; IZF (Friedman ) keeps membership but rejects excluded middle; FOLDS (Makkai 1995 ) is a logic in which only equivalence-invariant properties are expressible.

5.2 Principal theorems

5.3 Connection to the unified triple

Part III certifies that the unified triple $({\mathcal{U}}_{\mathrm{cu}},\zeta ,\mathsf{ua})$ is foundationally robust in a precise sense: under any of ETCS, IZF, FOLDS, or HoTT, the construction of $\zeta$ from ${\mathbb{R}}_c$ and ${\mathbb{C}}_c$ produces an isomorphic object (modulo the respective notion of equivalence). Without this, one might worry that $\zeta$ as defined inside HoTT is parochial. The univalence-boundary theorem says: HoTT goes a strict step further than the other three by making structure-preservation a theorem rather than a metatheorem.

5.4 Cross-references

Part III sits orthogonally to Parts I, II, IV: it does not contribute machinery to $\zeta$ but certifies the construction across foundations. It connects to Paper II of the prior series (which mentioned ETCS, IZF as alternatives but did not develop them) and to Paper VI (which developed Lawvere theories within an ETCS-friendly frame).

6 Part IV: $(\infty ,1)$-NNOs

6.1 Recap

Part IV  addresses the open problem (Synthesis §8 item 4) of the higher-categorical structure of NNO. The prior series proved contractibility of the type of NNOs in HoTT (Paper V Theorem 4.4). The $(\infty ,1)$-categorical analogue, in elementary $(\infty ,1)$-toposes, is more delicate: Rasekh  showed that every elementary $(\infty ,1)$-topos has a NNO, by constructing it from the loop space of $S^1=K(\mathbb{Z},1)$.

6.2 Principal theorems

6.3 Connection to the unified triple

Part IV ensures that the iteration / primitive recursion needed to define the Dirichlet sum $${\zeta }_{\mathrm{Dir}}(s):=\sum _{n\ge 1}{n}^{-s}$$ is correctly stated in the $(\infty ,1)$-context. Without contractibility, two distinct presentations of $\mathbb{N}$ in $\mathcal{E}$ might give two non-equivalent definitions of $\zeta$ via two non-equivalent enumerations of the natural numbers; contractibility prevents this.

6.4 Cross-references

Part IV uses Part II’s cubical machinery to formalise contractibility within Cubical Agda, and feeds Part VI’s $\zeta$. It extends Paper III §3 (NNO universal property), Paper V Theorem 4.4 (contractibility in HoTT), and Paper VI Theorem 4.1 (initial in $\mathrm{Mod}(T_{\mathrm{succ}})$).

7 Part V: Directed Univalence

7.1 Recap

Part V  addresses the open problem (Synthesis §8 item 5) of a complete directed univalence principle. Riehl–Shulman simplicial type theory  introduced a directed interval; Gratzer–Weinberger–Buchholtz  proved directed univalence for the universe $\mathcal{S}$ of discrete types. Part V surveys the state of the art and outlines a path to directed univalence for arbitrary types.

7.2 Principal theorems

7.3 Connection to the unified triple

Part V provides the synthetic apparatus for category theory and functor theory inside HoTT: with directed univalence, functors become directed maps in the universe, and natural transformations become directed 2-cells. This is essential for Part VI’s treatment of automorphic representations (which are functors $\mathrm{GL}(n,\mathbb{A})\to {\mathbb{C}}_c^{\ast }$ with extra coherence) and for the categorical Langlands correspondence. In the unified triple, ${\mathsf{ua}}_{?}=\mathsf{dua}$ is the case relevant to Langlands.

7.4 Cross-references

Part V extends Paper V §8.3 (directed HoTT paragraph) and Synthesis §7.2 (synthetic $\infty$-categories). It feeds Part VI §4–5 (Langlands).

8 Part VI: Langlands and the $\zeta (s)=0$ Roadmap

8.1 Recap

Part VI  is the centerpiece. It addresses the principal open problem (Synthesis §7.3, §8 item 2): a HoTT-native formulation of analytic number theory with $\zeta$ a HoTT-native object and $\zeta (s)=0$ a HoTT-native proposition. Part VI does not solve this problem; it formulates it precisely and offers a roadmap.

8.2 Principal contributions

1. A prerequisite chain: HoTT-native real numbers ${\mathbb{R}}_c$ $\Rightarrow$ HoTT-native complex numbers ${\mathbb{C}}_c$ via univalent algebraic closure $\Rightarrow$ HoTT-native holomorphic functions $\Rightarrow$ HoTT-native Dirichlet series.

2. Three candidate definitions of $\zeta$: as an HIIT, as the analytic limit of an Euler product, and as the unique solution to a meromorphic-continuation universal property.

3. A worked example $\zeta (2)={\pi }^2/6$ at the level of definitions.

4. A geometric Langlands $(\infty ,1)$-topos formulation, plus Clausen–Scholze condensed mathematics, plus Loeffler–Stoll Lean / Mathlib comparison.

5. Six concrete sub-problems for HoTT-native $\zeta$, with effort estimates.

6. A formal HoTT statement of the Riemann hypothesis.

8.3 The six sub-problems

We will reproduce these in 10. They are:

1. HoTT-native ${\mathbb{C}}_c$ with full algebraic-closure axiom.

2. HoTT-native holomorphic functions.

3. HoTT-native Dirichlet series machinery.

4. HoTT-native analytic continuation.

5. HoTT-native functional equation.

6. HoTT-native formal RH statement.

The dependency graph is a chain $1\to 2\to 3\to 4\to 5\to 6$ with a shortcut from 1 to 3.

8.4 Connection to the unified triple

Part VI is the place at which the triple $({\mathcal{U}}_{\mathrm{cu}},\zeta ,{\mathsf{ua}}_{?})$ is finally assembled. Each sub-problem invokes one of the preceding parts:

• Sub-problem 1 (${\mathbb{C}}_c$): uses Part II.

• Sub-problem 2 (holomorphic functions): uses Part II for the carrier and Part III for the foundational independence of the definition.

• Sub-problem 3 (Dirichlet series): uses Part I for the coalgebraic formulation as a stream of partial sums, Part II for convergence, and Part IV for the indexing $\mathbb{N}$.

• Sub-problem 4 (analytic continuation): uses Parts I–IV.

• Sub-problem 5 (functional equation): uses Parts I–IV plus Part V for the cohesive / directed reformulation.

• Sub-problem 6 (formal RH): uses Parts I–V.

9 Cross-Cutting Themes

9.1 Theme 1: Inductive–coinductive duality (Parts I, II)

The reals ${\mathbb{R}}_c$ admit two presentations: inductively, as a HIIT of Cauchy sequences modulo a path-constructor (Paper V §5.4; Part II); and coinductively, as a final coalgebra of digit streams modulo carry-bisimulation (Paper III §5; Part I). These are equal by univalence applied to the universal property of the Cauchy completion (Paper III Theorem 4.1) but differ computationally.

13 is the unifying theorem of Parts I and II. In 10 we use it to argue that the convergence of the Dirichlet sum $\sum n^{-s}$ for $\Re (s)>1$ is naturally a coinductive fact about partial-sum streams, while the analytic continuation to $\mathbb{C}\setminus \{1\}$ is naturally an inductive fact about holomorphic-extension functors.

9.2 Theme 2: Structural vs. material foundations (Part III)

The contrast between membership-based foundations (ZFC, IZF) and structure-based foundations (ETCS, FOLDS, HoTT) is the subject of Part III. Within HoTT, structure becomes material in a precise sense: the type ${\Sigma }_{X:\mathcal{U}}F(X)$ of $F$-structures is itself a type, and equivalence of structures is internalised as identity by univalence.

This is not vacuous. In ZFC, “the natural numbers” is not a single object: there are von Neumann naturals, Zermelo naturals, and infinitely many other encodings, all with different junk theorems (Paper II §4–6). In HoTT, “the natural numbers” is a single type $\mathbb{N}:\mathcal{U}$, and the type of NNO structures is contractible (Paper V Theorem 4.4 / Part IV). Univalence is the principle that makes the category-theoretic “up to isomorphism” literally an identity.

9.3 Theme 3: Coherence and contractibility (Part IV)

The bridge from 1-categorical universal properties (“unique up to isomorphism”) to $(\infty ,1)$-categorical ones (“unique up to contractible space of choices”) is the contractibility theorem of Part IV. The 1-categorical statement says: any two NNOs are uniquely isomorphic. The $(\infty ,1)$-categorical statement says: the space of NNOs is contractible, i.e. uniquely isomorphic in a way that is itself unique up to a unique 2-isomorphism, etc.

This principle is what makes the prior synthesis’s theorem (“Identity of perspectives” Theorem 5.2) lift from natural numbers to arbitrary essentially algebraic structures, including the analytic objects of Part VI.

9.4 Theme 4: Symmetric vs. directed univalence (Parts II, V)

Symmetric univalence (Paper V Theorem 4.2; Part II) gives an equivalence $(A{=}_{\mathcal{U}}B)\simeq (A\simeq B)$. Directed univalence (Riehl–Shulman; Part V) gives an equivalence ${\mathrm{Hom}}_{\mathcal{S}}(A,B)\simeq (A\to B)$ in the universe of discrete types.

For the analytic-NT programme, this principle has a concrete consequence: statements about $\zeta$ as a function live in the symmetric universe (Part II), while statements about automorphic representations and Langlands functoriality live in the directed universe (Part V).

9.5 Theme 5: The $\zeta$-prerequisite chain (Part VI)

The five themes above coalesce in Part VI. The following diagram summarises the dependencies.

1 encodes the central claim of this synthesis: the six component papers are not independent investigations but a single five-prerequisite construction whose target is the HoTT-native $\zeta$.

10 The $\zeta (s)=0$ Roadmap as Compositional Gates

10.1 Reformulation

We reformulate Part VI’s six sub-problems as compositional gates: each sub-problem invokes exactly the apparatus assembled in the preceding parts.

10.2 Gate 1: HoTT-native ${\mathbb{C}}_c$ with algebraic closure

Apparatus required. Part II (cubical ${\mathbb{R}}_c$). Part III (foundation-independence of the construction). Part IV (universal property at the $(\infty ,1)$-level).

Status. Partial; algebraic closure not yet formalised.

10.3 Gate 2: HoTT-native holomorphic functions

Apparatus required. Gate 1; Part I for stream-presentation of power series; Part II for the analytic limit construction.

Status. Possible by direct constructive analysis. Estimated effort: $\sim 5000$ lines.

10.4 Gate 3: HoTT-native Dirichlet series

Apparatus required. Gates 1, 2; Part I (coalgebraic streams of partial sums); Part IV (NNO indexing). Note the natural use of 13: convergence is coinductive over the partial-sum stream, while the algebra structure is inductive on the underlying sequences.

Status. Companion Haskell code provides a finite-precision prototype; HoTT formalisation pending.

10.5 Gate 4: HoTT-native analytic continuation

Apparatus required. Gates 1–3; Part III for foundational robustness of analytic continuation across ETCS / IZF / FOLDS / HoTT. This is the key technical bottleneck. Constructive analytic continuation is delicate; the classical identity theorem uses excluded middle, which must be replaced by a constructive density argument.

Status. Open; bottleneck.

10.6 Gate 5: HoTT-native functional equation

Apparatus required. Gates 1–4; Part V (directed reasoning for duality), Part I (coalgebraic identity for the gamma function).

Status. Requires Gates 1–4 first.

10.7 Gate 6: HoTT-native RH statement

The HoTT statement is, in the notation of Part VI: $$\mathrm{RH}:=\prod _{s:{\mathbb{C}}_c}(\zeta (s)=0)\to \mathsf{IsNonTrivial}(s)\to (\Re (s){=}_{{\mathbb{R}}_c}1/2).$$

Apparatus required. Gates 1–4; Part III for the foundation- independent reading; Part V for the connection to Langlands functoriality.

Status. Doable now (modulo Gates 1–4); the statement, not the proof.

10.8 Composition diagram

10.9 Estimated effort

Following Part VI, the total effort is estimated at $\sim 15,000$ lines of Cubical Agda, $8$–$12$ graduate-student-years. Comparable to the total effort behind Loeffler–Stoll  plus its Mathlib dependencies.

10.10 Worked example: $\zeta (2)$ as a HoTT-native fact

To make the gate structure concrete, consider the special value $\zeta (2)={\pi }^2/6$. A HoTT-native proof of this identity would proceed as follows.

1. By Gate 3, the Dirichlet sum ${\sum }_{n=1}^{\infty }1/n^2$ converges in ${\mathbb{C}}_c$. The convergence is a coinductive fact about the partial-sum stream $S_N:={\sum }_{n=1}^{N}1/n^2$, which is bisimilar (in the sense of Part I) to a Cauchy stream of approximations to ${\pi }^2/6$.

2. By Part I (3), $\pi$ is the centre of a contractible coalgebraic subtype, hence ${\pi }^2/6$ is.

3. By Part II’s universal property, the Cauchy reals are unique up to canonical equivalence, so the limit of $S_N$ in ${\mathbb{R}}_c$ is well-defined and is equal to ${\pi }^2/6$.

4. The classical Euler proof, transported via the foundation- independence of Part III, gives the equality. Specifically: the function $\sin (\pi z)/(\pi z)$ admits a product expansion ${\prod }_{n\ge 1}(1-z^2/n^2)$, whose coefficient of $z^2$ on both sides yields $\zeta (2)={\pi }^2/6$. The product expansion is a coinductive identity in the sense that the partial products $P_N(z):={\prod }_{n=1}^N(1-z^2/n^2)$ form a stream ${(P_N)}_{N\in \mathbb{N}}$ of holomorphic functions whose coefficient streams converge coordinatewise; the equality of the coefficient of $z^2$ between the two sides is then a bisimulation between coefficient streams in the sense of Part I, and the Weierstrass-product machinery  provides the uniform-convergence bound that promotes the coordinatewise coalgebraic identity to an identity of holomorphic functions in ${\mathbb{C}}_c$.

The above is a specification of a proof, not the proof itself. Fully formalising it inside Cubical Agda is the subject of the gates’ implementation.

10.11 Worked example: the functional equation

Riemann’s functional equation $$\zeta (s)=2^s{\pi }^{s-1}\sin (\pi s/2)\Gamma (1-s)\zeta (1-s)$$ is the principal organising identity for $\zeta$. In the unified framework it is Gate 5. We sketch the route in HoTT.

The classical proof uses the Mellin transform: the integral ${\int }_0^{\infty }{x}^{s-1}f(x)dx$ for suitable $f$, with $f$ a theta function. The HoTT-native version requires:

• $\Gamma$ as a HoTT-native object: by Gates 2–3, $\Gamma$ is definable as the analytic continuation of ${\int }_0^{\infty }{x}^{s-1}{e}^{-x}dx$ for $\Re (s)>0$;

• theta functions $\theta (\tau )$: defined as Dirichlet-type series indexed by $\mathbb{Z}$, hence available once Gates 2–4 are in place;

• the Mellin pairing $⟨\theta ,\zeta ⟩$: definable as a synthetic integral over the directed half-line $(0,\infty )$, whose definition requires Part V’s directed structure for the orientation;

• the modular invariance $\theta (\tau )={(-i\tau )}^{-1/2}\theta (-1/\tau )$: a synthetic statement in cohesive HoTT , using the cohesive shape modality to pass between $\mathbb{Z}$-equivariant and ${\mathrm{SL}}_2(\mathbb{Z})$-equivariant cohomology.

The functional equation falls out of the modular invariance of $\theta$ via the Mellin pairing; the HoTT-native version requires the synthetic apparatus of Parts II, IV, V.

10.12 Worked example: the Riemann hypothesis as a HoTT proposition

The HoTT-internal RH proposition is, in the notation of Part VI: $$\mathrm{RH}:=\prod _{s:{\mathbb{C}}_c}(\zeta (s){=}_{{\mathbb{C}}_c}0)\to \mathsf{IsNonTrivial}(s)\to (\Re (s){=}_{{\mathbb{R}}_c}1/2).$$

Three remarks on this proposition.

Remark 1: Propositionality. $\mathrm{RH}$ is an $(-1)$-truncated type because each of the constituent identities $\Re (s)=1/2$ is a path in an h-set. Hence “$\mathrm{RH}$ has two distinct proofs” is empty; either $\mathrm{RH}$ is inhabited, or it is not.

Remark 2: Decidability. $\mathrm{RH}$ is not decidable in HoTT: there is no algorithm $\mathrm{RH}\vee \neg \mathrm{RH}$. This is consistent with constructivity, since $\mathrm{RH}$ is a $\Pi$-statement over an uncountable type. Under classical logic (LEM), $\mathrm{RH}\vee \neg \mathrm{RH}$ is inhabited; this is a consequence of LEM, not a constructive theorem.

Remark 3: Modal status. $\mathrm{RH}$ admits a modal-logical analysis. Inside cohesive HoTT, with cohesion modalities $♯,♭$ , one can ask whether $\mathrm{RH}$ is $♭$-stable (true in the discrete shadow) or $♯$-stable (true in the codiscrete shadow). The answer is not known.

11 Discussion

11.1 What HoTT contributes vs. what HoTT requires

A fair question, posed by reviewers of Part VI, is: what does HoTT actually contribute to analytic number theory, beyond a more elaborate language? The answer has three parts.

(1) Foundation-independence is internalised. In ZFC, the statement “$\zeta (2)={\pi }^2/6$” depends, at least nominally, on the chosen encoding of $\mathbb{C}$. In HoTT, by univalence and the structure-identity principle (Part III), the statement is invariant under all isomorphisms of ${\mathbb{C}}_c$. This is not a sociological convention but a theorem.

(2) Coherences are automatic. Classical proofs of identities like the functional equation involve a long chain of intermediate identities, each requiring its own proof of well-definedness on equivalence classes. In HoTT, by univalence and contractibility (Part IV), these intermediate identities are automatic: paths in the universe transport along functorial constructions.

(3) Computation comes for free. In Cubical Agda (Part II), the construction of $\zeta$ would be executable: one could ask the proof assistant to compute $\zeta (2)$ to $k$ decimal places, and the construction of the proof of $\zeta (2)={\pi }^2/6$ would yield, as a byproduct, an algorithm computing ${\pi }^2/6$ to $k$ decimal places, by Type II Turing computability of the cubical reals.

The cost is also threefold:

• Constructive analytic continuation is much harder than the classical version (Gate 4).

• Some classical theorems (e.g. the prime-number theorem with the classical contour-shift proof) require LEM and do not transport directly.

• The infrastructure — HIIT machinery (Part II), $(\infty ,1)$-NNO (Part IV), directed univalence (Part V) — is itself a research-level investment.

11.2 Lean Mathlib vs. Cubical Agda

The Loeffler–Stoll formalization  is in Lean 4 / Mathlib, which uses classical foundations. Their formalisation is $\sim 3300$ lines for analytic continuation and the functional equation. Our estimate (Part VI, repeated in 10) is $\sim 15000$ lines for the equivalent work in Cubical Agda. The factor-of-five overhead reflects:

• additional structural lemmas that are free in Mathlib’s classical setting (e.g. propositional extensionality);

• HIIT path-constructor reasoning;

• constructive analogues of identity-theorem-style classical arguments;

• the cubical machinery itself (transport, composition, Glue types).

Whether this overhead is worth paying is a separate question; we have argued in (1)–(3) above that it is.

11.3 The role of cohesive / differential HoTT

Several gates — holomorphic functions (Gate 2), the modular invariance underlying the functional equation (Gate 5) — have a natural cohesive flavour. Cohesive HoTT  adjoins to the universe a triple of modalities $(♭,♯,\mathsf{S})$ that encode, respectively, the discrete, the codiscrete, and the shape (cohesive shape) of a cohesive space. Holomorphicity is then a $♭$-modal condition; modular invariance is a $♯$-modal condition. The full development of analytic number theory in cohesive HoTT is a long-term programme; we view Part VI’s roadmap as the first step.

11.4 The role of computer-checked proofs

The estimates in 10 assume Cubical Agda as the implementation platform. Other platforms are possible: Lean 4 with a HoTT layer (in development), Coq with the UniMath library, or rzk for the directed-univalent fragment. Whether the cubical flavour or the rzk flavour is better suited to the directed parts (Gate 5, Part V) is an empirical question whose answer awaits experimentation. A pragmatic strategy might combine the two: cubical Agda for the symmetric-univalent fragment and rzk for the directed fragment, glued via an interface based on the universe of discrete types.

11.5 What success would look like

A successful execution of the programme outlined here would yield:

1. a Cubical Agda library defining $\zeta :{\mathbb{C}}_c\to {\mathbb{C}}_c$ with the Euler product, the functional equation, and the formal RH statement;

2. a proof of $\zeta (2)={\pi }^2/6$ formally verified by the computer;

3. a proof of the non-vanishing of $\zeta$ on $\Re (s)=1$, hence a HoTT-native proof of the prime number theorem;

4. the formal RH proposition $\mathrm{RH}:\mathsf{Prop}$, in a form that could in principle be inhabited by a proof if one were ever found.

The last item bears emphasis: HoTT does not promise a proof of RH. It promises a statement of RH that is foundationally robust, structurally clean, and decoupled from the choice of set-theoretic model. That, in itself, is a nontrivial contribution.

12 Open Questions

We close with the outstanding open questions for the next round of the programme. These are not the gates of 10, which are “mechanical” in the sense that we know how they would proceed; they are the genuinely conceptual questions still to be resolved.

12.1 Open question 1: Coalgebraic $\zeta (2k)$

12.2 Open question 2: Cubical formalisation of analytic continuation

12.3 Open question 3: Directed univalence for non-discrete types

This is the open problem that Part V isolates as the crux for synthetic representation theory.

12.4 Open question 4: Foundational comparison theorem

This is the conceptual content of Part III lifted to ${\mathbb{C}}_c$.

12.5 Open question 5: $\infty$-toposes for analytic Langlands

12.6 Open question 6: Riemann hypothesis as HoTT proposition

13 Conclusion

This synthesis paper has unified six independent investigations into a single research programme directed at a HoTT-native formulation of analytic number theory. Five cross-cutting themes ([prin:dual,prin:strucMaterial,prin:coherence,prin:dualUniv], plus the $\zeta$-prerequisite chain of 10) tie the parts together, and Part VI’s six sub-problems are reformulated in 10 as compositional gates inheriting exactly the apparatus of the preceding parts. The Riemann hypothesis appears, in this picture, not as a single statement to be proved, but as a single proposition to be stated: the construction of the proposition is itself a multi-year, multi-person research programme, and we have set out, in 2 and 12, the gates that the programme must traverse.

The prior series established that the natural numbers are foundationally one object, viewed from many perspectives. The present series extends this picture from the natural numbers to the analytic objects of contemporary mathematics: the reals, the complex numbers, holomorphic functions, $L$-functions, and ultimately $\zeta$ itself. The unifying perspective is the same throughout: under univalence, equivalent presentations are literally equal, and the structure-identity principle becomes internalised at every level. What was the central claim of the prior synthesis for $\mathbb{N}$ becomes, in the present synthesis, a roadmap for $\zeta$.

We have argued that the unification is not nominal but structural: each of the six papers contributes essential apparatus to the $\zeta$-roadmap, and removing any one of them leaves a perceptible gap. Whether the roadmap can be completed in the next decade is an empirical question about how much effort the community puts in. Whether $\mathrm{RH}$ is provable inside the HoTT framework is a deep mathematical question that is not, on present evidence, more or less likely to receive a positive answer than the classical question. What HoTT contributes is not a new approach to the Riemann hypothesis; it contributes a new language in which the question can be stated, a language in which the structural symmetries of the problem become visible, and a foundation in which questions of foundational independence become provable rather than philosophically debatable.