# Decisions

One record per choice that shapes this repository. Each follows the [decision record](https://github.com/Tewf/reader-ergonomics/blob/2e5b6f0c3e67d2dc8195a63cf882d46170e79a5a/shapes/decision-record.md) of reader-ergonomics: the
decision in one sentence under its title, then its status, context, decision and consequences.

**Shape:** [topic](https://github.com/Tewf/reader-ergonomics-topic/blob/092ae2fc2e07226b695e219e3eb14b40286faa25/shapes/topic.md), as every folder here.

## Contents

| Record | Summary |
|---|---|
| [0001 A repository of its own](0001-a-repository-of-its-own.md) | the AI-augmented strand left the topic with its history, and pins a topic release |
| [0002 Call it a blueprint](0002-call-it-a-blueprint.md) | the field's word for a graph of claims each checked by Lean, made topic-shaped |
| [0003 Euclid's theorem as the first proof](0003-euclids-theorem-as-the-first-proof.md) | three claims, one topic each, under one theorem topic |
| [0004 Lean on Mathlib](0004-lean-on-mathlib.md) | a Lake project at the root, on Mathlib at the tag whose toolchain it takes |
| [0005 Three checks, each its own CI step](0005-three-checks-each-its-own-ci-step.md) | the topic check, the link check and the build, in that order |
| [0006 A challenge file holds the audited statements](0006-a-challenge-file-holds-the-audited-statements.md) | the statements apart from the proofs, held to each proof by a text check and by Lean |
| [0007 The audit has two columns](0007-the-audit-has-two-columns.md) | the maintainer audits the prose against the source; the Lean statement against the prose waits for a reader of Lean |
| [0008 Which findings became principles](0008-which-findings-became-principles.md) | five principles from the review's four conditions and the link check, one claim shape, the rest left findings |

## See also

[The front page](../README.md).