---
title: "Milestones"
module: Milestones
lang: en
site: "Bedrock"
description: "The book's proved endpoint results, with routes leading to each theorem."
stage: "Preview"
reading_order: 1
canonical: https://bedrock.institute/en/index.html
html: index.html#milestones
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Milestones.lagda.md
prerequisites: []
routes: []
translations: [https://bedrock.institute/zh/index.md, https://bedrock.institute/ja/index.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Milestones

This page gathers the book's proved endpoint results and offers a concise entrance to the routes that lead to them. Each entry states a theorem in ordinary mathematical language, then imports the exact Agda declaration that proves it.

```agda
{-# OPTIONS --cubical --safe --guardedness #-}

module Milestones where
```

**Theorem 1.** Under the excluded-middle assumption, the host-level `V` is a model of ZF.

```agda
open import V.Model public using ( V⊨ZF )
```

**Theorem 2.** Under the host-level axiom-of-choice assumption, the host-level `V` is a model of ZFC.

```agda
open import V.Model public using ( V⊨ZFC )
```

**Theorem 3.** Under the excluded-middle assumption, the constructible universe `L` is a model of ZFC.

```agda
open import L.Model public using ( L⊨ZFC )
```

**Theorem 4.** Under the same excluded-middle assumption, the constructible universe `L` satisfies the generalized continuum hypothesis internally.

```agda
open import L.GCH.Theorem public using ( L⊨GCH )
```