diff --git a/docs/reference/BELOCH-CONSTRUCTIONS.md b/docs/reference/BELOCH-CONSTRUCTIONS.md index 0c04a7ec..8a73f219 100644 --- a/docs/reference/BELOCH-CONSTRUCTIONS.md +++ b/docs/reference/BELOCH-CONSTRUCTIONS.md @@ -336,7 +336,7 @@ fold (map --ac onto --bd) (toward .b) (moving .c) The bisector of two rational lines is irrational in general, slope $\sqrt2 - 1$ for $y = 0$ and $y = x$; equality, parallelism and the paper -tests stay exact (`SPECIFICATION.md` §6). +tests stay exact ([[reference/beloch#exactness]]). ## Axiom 6, a point onto a line through a point diff --git a/docs/reference/BELOCH.md b/docs/reference/BELOCH.md index e4335781..1574d2e4 100644 --- a/docs/reference/BELOCH.md +++ b/docs/reference/BELOCH.md @@ -162,11 +162,13 @@ does not load files yet, so these two rules wait for the import ## Reads and writes -One law organizes the surface syntax (`SPECIFICATION.md` §4.10): an +One law organizes the surface syntax ([[decision/0011]]): an operation that changes the state is a keyword verb, sequenced in program order; an operation that only computes something from the current state is an operator, a bracket, or a construction, and may appear anywhere a value -is needed. +is needed. Finding where two creases cross and describing a line cost the +folder nothing; making a crease costs a fold, and the notation keeps the +two apart. In the terms of the model, the writes are the partial functions from states to states ([[reference/model#def-write|def-write]]), and the reads are functions from @@ -182,7 +184,7 @@ A point is named with `.`, a line or a crease with `--` ([[reference/beloch-names#names]]): the corners of the sheet are points, and so is every meet and every free point; a construction yields a line, and a write yields a crease. Every value is exact, whatever construction made it -(`SPECIFICATION.md` §6). +(Exactness, below). **Writes.** The operations of the model's section on operations, named by the verbs `mark`, `fold`, `unfold`, `reverse`, `flatten` and `flip`. Each is a @@ -276,3 +278,27 @@ segments are collinear ([[decision/0014]]) and is an error once a fold has bent A line stands nowhere a crease is wanted: it has no material until a `mark` scores it. The check needs no geometry, so a program's sorts can be verified before it is evaluated. + +## Exactness + +Every geometric decision is exact. An implementation decides each +predicate, equality of points and of lines, parallelism, incidence, +orientation and whether a point lies on the paper, as over the real +numbers: no tolerance, no sampling. The decisions are what a reader of the +output sees, since they fix which vertices are one, which layer a face +lies in and what lies on the paper, so two implementations that agree on +the predicates of a program write the same FOLD graph. + +The rule binds the decisions and leaves the representation of numbers +free. Exact arithmetic over the real algebraic numbers is one way to meet +it ([[decision/0012]], [[decision/0013]]); interval arithmetic with an exact +fallback where an interval leaves a predicate open is another. The +constructions bound how irrational a coordinate gets: axioms 1 to 4 keep +rational inputs rational, axiom 5 brings square roots, extensions of +degree 2 over the field so far [@hull2020, §3.2], and axiom 7 brings cube +roots, while axioms 1 to 6 stay in the tower of square roots +([[reference/beloch-constructions#axiom-numbering]]). + +The output is the one inexact step: the coordinates in a FOLD file are +decimals, rounded at serialization alone, and no decision is taken on a +rounded value ([[reference/fold]]). diff --git a/docs/reference/SPECIFICATION.md b/docs/reference/SPECIFICATION.md index 2286b233..53f47c84 100644 --- a/docs/reference/SPECIFICATION.md +++ b/docs/reference/SPECIFICATION.md @@ -84,93 +84,6 @@ selectors `.[] --[] #[]`), the one write was the keyword `through`); --- -## 4. Operations - -### 4.10 The read/write law — constructions read, `mark`/`fold`/`flatten` write *(since v0.20-dev; completed v0.21-dev; `collapse` renamed `flatten` v0.23-dev)* - -One law governs the surface syntax: **an operation that mutates paper state — -scores a crease, folds, and thereby re-segments existing references (ADR 0014) -— is a keyword verb, sequenced in program order; an operation that only reads -the current state, or only describes a geometric line without touching the -paper, is a pure read, and is an operator, bracket, or construction.** Keywords are -commits to the versioned sheet; reads are checkout queries against it, or (for -constructions) descriptions not yet committed. The physical asymmetry the law -encodes: *finding* where two creases cross is free, *describing* a line is -free, *making* a crease costs a fold, so the notation looks different for the -two. - -The **reads** are: - -- the symbols/brackets — meet `*` and `.[l+]`, join `--[c+]`, flap `#[c+]`, - filter `&`, drop `\`, union `[…]` — which **select existing geometry** and - error on no-match: meet `*`/`.[]` names an existing crossing, and the join - `--[.a .b]` (or its `.a * .b` sugar) resolves to a **real** crease or paper - edge through the two points, never conjuring a "sight-line." -- the **constructions** — `map … onto …`, `through … …`, `perp … through …` - (`BELOCH-CONSTRUCTIONS.md`) — which compute a line without touching the paper. `--l = map - .a onto .b` binds a value; on its own it scores nothing. *(since v0.21-dev)* - `through` (Huzita axiom 1) joins this side too: it used to be the sole - write, but it is no reflection, only a description — "the line through two - points" is exactly as inert as any other construction until a disposition verb - acts on it. - -The **writes** are the disposition keyword verbs (`BELOCH-WRITES.md`, `BELOCH-WRITES.md`): - -- **`mark`** — crease a construction (or an inline line) flat: subdivides the - sheet, emits FOLD `F`. -- **`fold`** — crease a construction (or an existing material crease) and fold it: - subdivides *and* moves layers, emits FOLD `M`/`V`. -- **`flatten`** — fold several existing material creases sharing one vertex - straight to the flat end state, optionally deriving the one crease - flat-foldability forces when the given ray set is odd (`BELOCH-WRITES.md`). - -`@` is retired entirely: it is no longer a marker anywhere in the grammar — -the verb itself (`mark`/`fold`/`flatten`) carries the write, completing the -notation cutover begun in v0.20-dev. - -Point-locating landmark constructions (a bisector foot, a reference apex) are -currently scored as full `mark (through …) as …` creases, an interim that adds -real geometry and moves the golden. The short-reference alternative is the -partial mark `mark (…) (at .p)` (`BELOCH-WRITES.md`), whose mid-face extent lays a non-subdividing -record instead of a full crease. - ---- - -## 6. Exactness *(since v0.0)* - -All coordinates and line coefficients are **real numbers**; a line is -`a·x + b·y = c`. - -**Geometric decisions MUST be exact.** A conforming implementation MUST decide -every geometric predicate — equality of points and lines, parallelism, -incidence, orientation, point-in-polygon — as if computed over the exact reals. -No epsilon, no tolerance, no sampling. These decisions are **observable**: they -fix vertex identity, layer membership, and on-paper tests, and therefore the -emitted crease pattern and folded form (§7). Two implementations that agree on a -program's predicates emit the same FOLD graph. - -The requirement is on the **decisions, not the number representation**. Exact -arithmetic over the algebraic reals is one sufficient strategy; an -exact-geometric-computation approach in the style of CGAL — interval arithmetic -with an exact fallback only when an interval is inconclusive — is equally -conforming. The spec constrains *what must be decided correctly*, never *how*. - -**Algebraic degree** *(informational).* The constructions bound how irrational a -coordinate can become, which tells an implementation what field its decisions -must cover: - -- Axioms 1–4 over rational inputs stay **rational** — no roots arise. -- Axiom 5 (angle bisector) introduces **square roots**: degree-≤2 extensions of - the base field [[hull2020]](#ref-hull2020) §3.2. -- Axiom 7 (the cubic Beloch fold) introduces **cube roots**; axioms 1–6 stay in - the quadratic tower. - -**Serialization is the only inexact step.** `vertices_coords` in the FOLD output -(§7) is rendered to JSON decimal; non-terminating reals are rounded *in the -output only*. No internal decision is ever taken on a truncated value. - ---- - ## 7. Output: the FOLD contract *(since v0.0; dual-frame since v0.7-dev; multi-frame since v0.16-dev)* `beloch fold FILE.bel` emits a [FOLD](https://github.com/edemaine/fold) file