Toward RH : HoTT-Prop

Synthesis Paper

SYNTHESISMeta

Toward RH : HoTT-Prop — Synthesis of Volume III

This synthesis paper unifies the six research papers of Volume III of the Toward RH : HoTT-Prop programme. The honest result: one cleanly engineered new theorem (OQ1) and five well-formulated open programmes.

Read PaperPDF

Open Questions — Priority Order

OQ1Highest

Coalgebraic ζ(2k): Bisimulation-closed predicates for ζ(2k) ∈ ℚ·π^{2k}

We construct, for each k ≥ 1, an explicit coinductively defined streaming witness in the digit-stream final coalgebra whose underlying real value is ζ(2k)/2, packaged as a contractible HoTT-internal type.

ReadPDF

OQ2High

A Cubical Library for Analytic Continuation: Identity and Monodromy Theorems Constructively

Specifies and partially formalises a Cubical Agda library for constructive analytic continuation, targeting Gates 2 and 4 of the Volume II RH roadmap.

ReadPDF

OQ4Medium

A Foundational Comparison Theorem for ζ in HoTT and ZFC

Addresses whether first-order statements about ζ provable in HoTT for the HoTT-native structure are equivalent to those provable in classical ZFC for the standard structure.

ReadPDF

OQ3Research-Grade

Directed Univalence Beyond the Discrete: Extending GWB 2024 to (∞,1)-Categorical Types

The directed univalence theorem of GWB 2024 holds for discrete types. The natural strengthening to all (∞,1)-categorical types is the principal open problem in directed type theory.

ReadPDF

OQ5Research-Grade

An (∞,1)-Topos for Analytic Langlands: Automorphic Representations and Condensed Mathematics

A programmatic investigation of which elementary (∞,1)-topos most naturally hosts automorphic representations of GL(n, A_Q) and how it relates to the Clausen–Scholze condensed setting.

ReadPDF

OQ6Speculative

RH as a HoTT Proposition: Decidability and Constructive Certification

Studies the logical structure of the Riemann Hypothesis as a HoTT proposition RH : Prop. We ask: independently of provability, is RH decidable? Four interlocking questions answered.

ReadPDF

Honest Verdict — Lean Proof Matrix

Generated by codex gpt-5.5 at xhigh reasoning effort. Each theorem returns one of valid, invalid, or incomplete.

The 3 valid results in OQ4 are definitional identities in a finite-shadow toy model — not the full directed-univalence claim. The dominant blocker is lake build failure during Mathlib clone — an infrastructure issue, not a proof issue.

Part of the multi-volume HoTT Foundations of Mathematics programme