Source and edition
Tim Button and the Open Logic Project contributors, The Open Logic Text, Arithmetization chapter. Open Logic Project.
The teaching unit is available under CC BY4.0. Its cut definition, order and union argument, and the square-root cut calculation, adapt the human source. The Cauchy-sequence approach also informs the unit. GPT-6 Astra (OpenAI), Ultra, in Codex supplied the detailed field and order verification, bisection estimates, comparison and uniqueness proofs, and worked solutions. That instance self-checked its additions; no independent AI or human review is claimed.
Supplied terms · Native cut source · Native square-root cut passage · Editable teaching unit · Read the lesson
Sources
- Tim Button and Open Logic contributors: cuts.tex
- Tim Button and Open Logic contributors: cauchy.tex
- Tim Button and Open Logic contributors: checking-details.tex
Edition and prerequisites
Native source revision 1e960beff9ed7835bf3e3f1335e21af3439cd107. Native passages retain the project’s macros and are not standalone compilable documents. The teaching proofs are fully supplied in the editable lesson. The unit starts with rational arithmetic, induction, recursion and elementary set constructions; it does not claim to prove those starting inputs.