Move the read-write law and exactness to the language

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
 

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]]).

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