[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents Laterally, across Integers, rings, finite-dimensional Clifford rings $\mathrm{Cl}_{p, q}(\mathbb{Z})$ Commutative rings, $R$-algebras, finite-dimensional $R$-Clifford algebras $\mathrm{Cl}_{p, q}(R)$ Rational number field, rational algebras, finite-dimensional rational Clifford algebras $\mathrm{Cl}_{p, q}(\mathbb{Q})$ Real number fields, real algebras, finite-dimensional real Clifford algebras $\mathrm{Cl}_{p, q}(\mathbb{R})$ \section{Ordered commutative ring} ... \section{Ordered field} An ordered field is an ordered commutative ring such that every element which is greater than or less than zero is invertible. \section{Euclidean field} A Euclidean field is an ordered field where the square function, restricted to the non-negative elements, has a retract. Every Euclidean field has an absolute value function given by $\vert x \vert \coloneqq \sqrt{x^2}$ and a pseudolattice structure given by $\min(x, y) = \frac{x + y - \vert y - x \vert}{2}$, $\max(x, y) = \frac{x + y + \vert y - x \vert}{2}$ \section{Archimedean Euclidean field} $$\mathrm{isLimitOf}(a, l) \coloneqq \forall \epsilon:\mathbb{Q}_+.\exists N:\mathbb{N}.\forall n:\mathbb{N}.(n \geq N) \implies (a(n) - l \lt \epsilon \wedge -\epsilon \lt a(n) - l)$$ $$\mathrm{seqHaus}:\forall a:\mathbb{N} \to F.\mathrm{isProp}\left(\sum_{l:F} \mathrm{isLimitOf}(a, l)\right)$$ Prove that the type of limits of a sequence $a:\mathbb{N} \to F$ is a proposition. \section{Real number field} A real number field is a sequentially Cauchy complete Archimedean ordered Euclidean field. \section{Exponential function} $$\frac{\Gamma \vdash \mathbb{R} \; \mathrm{type} \quad \Gamma \vdash \mathrm{isRealNumberField}(\mathbb{R})}{\Gamma, x:\mathbb{R} \vdash \exp(x):\mathbb{R}}$$ $$\frac{\Gamma \vdash \mathbb{R} \; \mathrm{type} \quad \Gamma \vdash \mathrm{isRealNumberField}(\mathbb{R})}{\Gamma, x:\mathbb{R} \vdash \delta_\exp(x):\forall \epsilon:\mathbb{Q}_+.\exists N:\mathbb{N}.\forall n:\mathbb{N}.(n \geq N) \implies \left(\left(1 + \frac{x}{n}\right)^{n} - \exp(x) \lt \epsilon \wedge -\epsilon \lt \left(1 + \frac{x}{n}\right)^{n} - \exp(x)\right)}$$ or $$\frac{\Gamma \vdash \mathbb{R} \; \mathrm{type} \quad \Gamma \vdash \mathrm{isRealNumberField}(\mathbb{R})}{\Gamma, x:\mathbb{R} \vdash \delta_\exp(x):\forall \epsilon:\mathbb{Q}_+.\exists N:\mathbb{N}.\forall n:\mathbb{N}.(n \geq N) \implies \left(\sum_{i = 0}^{n} \frac{x^i}{i!} - \exp(x) \lt \epsilon \wedge -\epsilon \lt \sum_{i = 0}^{n} \frac{x^i}{i!} - \exp(x)\right)}$$ \section{Quadratic closures} A field is **quadratically closed** if every non-degenerate monic quadratic function is the product of two monic affine functions. Quadratic closure: Every non-degenerate monic quadratic function is the product of two monic affine functions. \section{Test} Literal basic stuff about high school algebra: * What is a variable? * What are free and bound variables? * What is substitution of terms for variables? \section{Variables} A variable is a symbol $x$ which represents an arbitrary instantiation of a type $T$. Variables are thus types and written as $x:T$. Variables are usually found in the context, as $\Gamma, x:T, \Delta \vdash \mathcal{J}$ for arbitrary judgment $\mathcal{J}$. \section{Free and bound variables} \section{Substitution} \section{Change of bound variables} category: redirected to nlab